f26285f3b9cb92768b509c3e93768166a3729a6a
1 [[!toc]]
3 Types, OCAML
4 ------------
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
11     # let f x = x + 3;;
13 The system replies with
15     val f : int -> int = <fun>
17 Since `+` is only defined on integers, it has type
19      # (+);;
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
24 order. That is,
26     # 3 + 4 = (+) 3 4;;
27     - : bool = true
29 In general, tuples with one element are identical to their one
30 element:
32     # (3) = 3;;
33     - : bool = true
35 though OCAML, like many systems, refuses to try to prove whether two
36 functional objects may be identical:
38     # (f) = f;;
39     Exception: Invalid_argument "equal: functional value".
41 Oh well.
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;;
53     - : int = 1
55 The types of the `then` clause and of the `else` clause must be the
56 same.
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>
63 That is,
65     # match true with true -> 1 | false -> 2;;
66     - : int = 1
68 Compare with
70     # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
71     - : int = 9
73 Unit and thunks
74 ---------------
76 All functions in OCAML take exactly one argument.  Even this one:
78     # let f x y = x + y;;
79     # f 2 3;;
80     - : int = 5
82 Here's how to tell that `f` has been curry'd:
84     # f 2;;
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
93     # ();;
94     - : unit = ()
96 Just as you can define functions that take constants for arguments
98     # let f 2 = 3;;
99     # f 2;;
100     - : int = 3;;
102 you can also define functions that take the unit as its argument, thus
104     # let f () = 3;;
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:
110     # f ();;
111     - : int = 3
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>
117     # f 5;;
118     - : int = 120
120 We can't define a function that is exactly analogous to our &omega;.
121 We could try `let rec omega x = x x;;` what happens?  However, we can
122 do this:
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,
129     # omega 3;;
131 the interpreter goes into an infinite loop, and you have to control-C
132 to break the loop.
134 Oh, one more thing: lambda expressions look like this:
136     # (fun x -> x);;
137     - : 'a -> 'a = <fun>
138     # (fun x -> x) true;;
139     - : bool = true
141 (But `(fun x -> x x)` still won't work.)
143 So we can try our usual tricks:
145     # (fun x -> true) omega;;
146     - : bool = true
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);;
154 Infinite loop.
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>
164     # test;;
165     - : unit -> 'a = <fun>
167     # test ();;
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").
174 Curry-Howard, take 1
175 --------------------
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
186 roughly as follows:
188 If a variable `x` has type &sigma; and term `M` has type &tau;, then
189 the abstract `\xM` has type &sigma; `-->` &tau;.
191 If a term `M` has type &sigma; `-->` &tau;, and a term `N` has type
192 &sigma;, then the application `MN` has type &tau;.
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):
202 <pre>
203 Axiom: ---------
204         A |- A
206 Structural Rules:
208           &Gamma;, A, B, &Delta; |- C
209 Exchange: ---------------------------
210           &Gamma;, B, A, &Delta; |- C
212              &Gamma;, A, A |- B
213 Contraction: -------------------
214              &Gamma;, A |- B
216            &Gamma; |- B
217 Weakening: -----------------
218            &Gamma;, A |- B
220 Logical Rules:
222          &Gamma;, A |- B
223 --> I:   -------------------
224          &Gamma; |- A --> B
226          &Gamma; |- A --> B         &Gamma; |- A
227 --> E:   -----------------------------------
228          &Gamma; |- B
229 </pre>
231 `A`, `B`, etc. are variables over formulas.
232 &Gamma;, &Delta;, etc. are variables over (possibly empty) sequences
233 of formulas.  &Gamma; `|- A` is a sequent, and is interpreted as
234 claiming that if each of the formulas in &Gamma; is true, then `A`
235 must also be true.
237 This logic allows derivations of theorems like the following:
239 <pre>
240 -------  Id
241 A |- A
242 ---------- Weak
243 A, B |- A
244 ------------- --> I
245 A |- B --> A
246 ----------------- --> I
247 |- A --> B --> A
248 </pre>
250 Should remind you of simple types.  (What was `A --> B --> A` the type
251 of again?)
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:
258 <pre>
259 Axiom: -----------
260        x:A |- x:A
262 Structural Rules:
264           &Gamma;, x:A, y:B, &Delta; |- R:C
265 Exchange: -------------------------------
266           &Gamma;, y:B, x:A, &Delta; |- R:C
268              &Gamma;, x:A, x:A |- R:B
269 Contraction: --------------------------
270              &Gamma;, x:A |- R:B
272            &Gamma; |- R:B
273 Weakening: ---------------------
274            &Gamma;, x:A |- R:B     [x chosen fresh]
276 Logical Rules:
278          &Gamma;, x:A |- R:B
279 --> I:   -------------------------
280          &Gamma; |- \xM:A --> B
282          &Gamma; |- f:(A --> B)      &Gamma; |- x:A
283 --> E:   -------------------------------------
284          &Gamma; |- (fx):B
285 </pre>
287 In these labeling rules, if a sequence &Gamma; in a premise contains
288 labeled formulas, those labels remain unchanged in the conclusion.
290 What is means for a variable `x` to be chosen *fresh* is that
291 `x` must be distinct from any other variable in any of the labels
292 used in the proof.
294 Using these labeling rules, we can label the proof
295 just given:
297 <pre>
298 ------------  Id
299 x:A |- x:A
300 ---------------- Weak
301 x:A, y:B |- x:A
302 ------------------------- --> I
303 x:A |- (\y.x):(B --> A)
304 ---------------------------- --> I
305 |- (\x y. x):A --> B --> A
306 </pre>
308 We have derived the *K* combinator, and typed it at the same time!
310 Need a proof that involves application, and a proof with cut that will
311 show beta reduction, so "normal" proof.
313 [To do: add pairs and destructors; unit and negation...]
315 Excercise: construct a proof whose labeling is the combinator S.