6 OCAML has type inference: the system can often infer what the type of
7 an expression must be, based on the type of other known expressions.
9 For instance, if we type
13 The system replies with
15 val f : int -> int = <fun>
17 Since `+` is only defined on integers, it has type
20 - : int -> int -> int = <fun>
22 The parentheses are there to turn off the trick that allows the two
23 arguments of `+` to surround it in infix (for linguists, SOV) argument
29 In general, tuples with one element are identical to their one
35 though OCAML, like many systems, refuses to try to prove whether two
36 functional objects may be identical:
39 Exception: Invalid_argument "equal: functional value".
44 Booleans in OCAML, and simple pattern matching
45 ----------------------------------------------
47 Where we would write `true 1 2` in our pure lambda calculus and expect
48 it to evaluate to `1`, in OCAML boolean types are not functions
49 (equivalently, are functions that take zero arguments). Selection is
50 accomplished as follows:
52 # if true then 1 else 2;;
55 The types of the `then` clause and of the `else` clause must be the
58 The `if` construction can be re-expressed by means of the following
59 pattern-matching expression:
61 match <bool expression> with true -> <expression1> | false -> <expression2>
65 # match true with true -> 1 | false -> 2;;
70 # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
76 All functions in OCAML take exactly one argument. Even this one:
82 Here's how to tell that `f` has been curry'd:
85 - : int -> int = <fun>
87 After we've given our `f` one argument, it returns a function that is
88 still waiting for another argument.
90 There is a special type in OCAML called `unit`. There is exactly one
91 object in this type, written `()`. So
96 Just as you can define functions that take constants for arguments
102 you can also define functions that take the unit as its argument, thus
105 val f : unit -> int = <fun>
107 Then the only argument you can possibly apply `f` to that is of the
108 correct type is the unit:
113 Let's have some fn: think of `rec` as our `Y` combinator. Then
115 # let rec f n = if (0 = n) then 1 else (n * (f (n - 1)));;
116 val f : int -> int = <fun>
120 We can't define a function that is exactly analogous to our ω.
121 We could try `let rec omega x = x x;;` what happens? However, we can
124 # let rec omega x = omega x;;
126 By the way, what's the type of this function?
127 If you then apply this omega to an argument,
131 the interpreter goes into an infinite loop, and you have to control-C
134 Oh, one more thing: lambda expressions look like this:
138 # (fun x -> x) true;;
141 (But `(fun x -> x x)` still won't work.)
143 So we can try our usual tricks:
145 # (fun x -> true) omega;;
148 OCAML declined to try to evaluate the argument before applying the
149 functor. But remember that `omega` is a function too, so we can
150 reverse the order of the arguments:
152 # omega (fun x -> true);;
156 Now consider the following variations in behavior:
158 # let test = omega omega;;
159 [Infinite loop, need to control c out]
161 # let test () = omega omega;;
162 val test : unit -> 'a = <fun>
165 - : unit -> 'a = <fun>
168 [Infinite loop, need to control c out]
170 We can use functions that take arguments of type unit to control
171 execution. In Scheme parlance, functions on the unit type are called
172 *thunks* (which I've always assumed was a blend of "think" and "chunk").
177 We will return to the Curry-Howard correspondence a number of times
178 during this course. It expresses a deep connection between logic,
179 types, and computation. Today we'll discuss how the simply-typed
180 lambda calculus corresponds to intuitionistic logic. This naturally
181 give rise to the question of what sort of computation classical logic
182 corresponds to---as we'll see later, the answer involves continuations.
184 So at this point we have the simply-typed lambda calculus: a set of
185 ground types, a set of functional types, and some typing rules, given
188 If a variable `x` has type σ and term `M` has type τ, then
189 the abstract `\xM` has type σ `-->` τ.
191 If a term `M` has type σ `-->` &tau, and a term `N` has type
192 σ, then the application `MN` has type τ.
194 These rules are clearly obverses of one another: the functional types
195 that abstract builds up are taken apart by application.
197 The next step in making sense out of the Curry-Howard corresponence is
198 to present a logic. It will be a part of intuitionistic logic. We'll
199 start with the implicational fragment (that is, the part of
200 intuitionistic logic that only involves axioms and implications):
208 Exchange: Γ, A, B, Δ |- C
209 ---------------------------
210 $Gamma;, B, A, Δ |- C
212 Contraction: Γ, A, A |- B
216 Weakening: Γ |- B
222 --> I: Γ, A |- B
226 --> E: Γ |- A --> B Γ |- A
227 -----------------------------------------
231 `A`, `B`, etc. are variables over formulas.
232 Γ, Δ, etc. are variables over (possibly empty) sequences
233 of formulas. `Γ |- A` is a sequent, and is interpreted as
234 claiming that if each of the formulas in Γ is true, then `A`
237 This logic allows derivations of theorems like the following:
246 ----------------- --> I
250 Should remind you of simple types. (What was `A --> B --> A` the type
253 The easy way to grasp the Curry-Howard correspondence is to *label*
254 the proofs. Since we wish to establish a correspondence between this
255 logic and the lambda calculus, the labels will all be terms from the
256 simply-typed lambda calculus. Here are the labeling rules:
264 Exchange: Γ, x:A, y:B, Δ |- R:C
265 --------------------------------------
266 Γ, y:B, x:A, Δ |- R:C
268 Contraction: Γ, x:A, x:A |- R:B
269 --------------------------
272 Weakening: Γ |- R:B
273 ---------------------
274 Γ, x:A |- R:B [x chosen fresh]
278 --> I: Γ, x:A |- R:B
279 -------------------------
280 Γ |- \xM:A --> B
282 --> E: Γ |- f:(A --> B) Γ |- x:A
283 ---------------------------------------------
287 In these labeling rules, if a sequence Γ in a premise contains
288 labeled formulas, those labels remain unchanged in the conclusion.
290 Using these labeling rules, we can label the proof
296 ---------------- Weak
298 ------------------------- --> I
299 x:A |- (\y.x):(B --> A)
300 ---------------------------- --> I
301 |- (\x y. x):A --> B --> A
304 We have derived the *K* combinator, and typed it at the same time!
306 [To do: add pairs and destructors; unit and negation...]
308 Excercise: construct a proof whose labeling is the combinator S.