9.4 The Curry-Howard Correspondence

< Free Open Study >

The "→" type constructor comes with typing rules of two kinds:

an introduction rule (T-ABS) describing how elements of the type can be created, and
an elimination rule (T-APP) describing how elements of the type can be used.

When an introduction form (λ) is an immediate subterm of an elimination form (application), the result is a redex—an opportunity for computation.

The terminology of introduction and elimination forms is frequently useful in discussing type systems. When we come to more complex systems later in the book, we'll see a similar pattern of linked introduction and elimination rules for each type constructor we consider.

9.4.1 Exercise [⋆]

Which of the rules for the type Bool in Figure 8-1 are introduction rules and which are elimination rules? What about the rules for Nat in Figure 8-2?

The introduction/elimination terminology arises from a connection between type theory and logic known as the Curry-Howard correspondence or Curry-Howard isomorphism (Curry and Feys, 1958; Howard, 1980). Briefly, the idea is that, in constructive logics, a proof of a proposition P consists of concrete evidence for P.^[4] What Curry and Howard noticed was that such evidence has a strongly computational feel. For example, a proof of a proposition P ⊃ Q can be viewed as a mechanical procedure that, given a proof of P, constructs a proof of Q—or, if you like, a proof of Q abstracted on a proof of P. Similarly, a proof of P ∧ Q consists of a proof of P together with a proof of Q. This observation gives rise to the following correspondence:

LOGIC	PROGRAMMING LANGUAGES

propositions	types
proposition P ⊃ Q	type P→Q
proposition P ∧ Q	type P × Q (see §11.6)
proof of proposition P	term t of type P
proposition P is provable	type P is inhabited (by some term)

On this view, a term of the simply typed lambda-calculus is a proof of a logical proposition corresponding to its type. Computation—reduction of lambda-terms—corresponds to the logical operation of proof simplification by cut elimination. The Curry-Howard correspondence is also called the propositions as types analogy. Thorough discussions of this correspondence can be found in many places, including Girard, Lafont, and Taylor (1989), Gallier (1993), Sφrensen and Urzyczyn (1998), Pfenning (2001), Goubault-Larrecq and Mackie (1997), and Simmons (2000).

The beauty of the Curry-Howard correspondence is that it is not limited to a particular type system and one related logic—on the contrary, it can be extended to a huge variety of type systems and logics. For example, System F (Chapter 23), whose parametric polymorphism involves quantification over types, corresponds precisely to a second-order constructive logic, which permits quantification over propositions. System F_ω (Chapter 30) corresponds to a higher-order logic. Indeed, the correspondence has often been exploited to transfer new developments between the fields. Thus, Girard's linear logic (1987) gives rise to the idea of linear type systems (Wadler, 1990, Wadler, 1991, Turner, Wadler, and Mossin, 1995, Hodas, 1992, Mackie, 1994, Chirimar, Gunter, and Riecke, 1996, Kobayashi, Pierce, and Turner, 1996, and many others), while modal logics have been used to help design frameworks for partial evaluation and run-time code generation (see Davies and Pfenning, 1996, Wickline, Lee, Pfenning, and Davies, 1998, and other sources cited there).

^[4]The characteristic difference between classical and constructive logics is the omission from the latter of proof rules like the law of the excluded middle, which says that, for every proposition Q, either Q holds or ¬Q does. To prove Q V ¬Q in a constructive logic, we must provide evidence either for Q or for ¬Q.

< Free Open Study >