ass5: omega->blackhole
[lambda.git] / week6.mdwn
1 [[!toc]]
2
3 Types, OCaml
4 ------------
5
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.
8
9 For instance, if we type 
10
11     # let f x = x + 3;;
12
13 The system replies with 
14
15     val f : int -> int = <fun>
16
17 Since `+` is only defined on integers, it has type
18
19      # (+);;
20      - : int -> int -> int = <fun>
21
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,
25
26     # 3 + 4 = (+) 3 4;;
27     - : bool = true
28
29 In general, tuples with one element are identical to their one
30 element:
31
32     # (3) = 3;;
33     - : bool = true
34
35 though OCaml, like many systems, refuses to try to prove whether two
36 functional objects may be identical:
37
38     # (f) = f;;
39     Exception: Invalid_argument "equal: functional value".
40
41 Oh well.
42
43
44 Booleans in OCaml, and simple pattern matching
45 ----------------------------------------------
46
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:
51
52     # if true then 1 else 2;;
53     - : int = 1
54
55 The types of the `then` clause and of the `else` clause must be the
56 same.
57
58 The `if` construction can be re-expressed by means of the following
59 pattern-matching expression:
60
61     match <bool expression> with true -> <expression1> | false -> <expression2>
62
63 That is,
64
65     # match true with true -> 1 | false -> 2;;
66     - : int = 1
67
68 Compare with 
69
70     # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
71     - : int = 9
72
73 Unit and thunks
74 ---------------
75
76 All functions in OCaml take exactly one argument.  Even this one:
77
78     # let f x y = x + y;;
79     # f 2 3;;
80     - : int = 5
81
82 Here's how to tell that `f` has been curry'd:
83
84     # f 2;;
85     - : int -> int = <fun>
86
87 After we've given our `f` one argument, it returns a function that is
88 still waiting for another argument.
89
90 There is a special type in OCaml called `unit`.  There is exactly one
91 object in this type, written `()`.  So
92
93     # ();;
94     - : unit = ()
95
96 Just as you can define functions that take constants for arguments
97
98     # let f 2 = 3;;
99     # f 2;;
100     - : int = 3;;
101
102 you can also define functions that take the unit as its argument, thus
103
104     # let f () = 3;;
105     val f : unit -> int = <fun>
106
107 Then the only argument you can possibly apply `f` to that is of the
108 correct type is the unit:
109
110     # f ();;
111     - : int = 3
112
113 Let's have some fn: think of `rec` as our `Y` combinator.  Then
114
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
119
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:
123
124     # let rec omega x = omega x;;
125
126 By the way, what's the type of this function?
127 If you then apply this omega to an argument,
128
129     # omega 3;;
130
131 the interpreter goes into an infinite loop, and you have to control-C
132 to break the loop.
133
134 Oh, one more thing: lambda expressions look like this:
135
136     # (fun x -> x);;
137     - : 'a -> 'a = <fun>
138     # (fun x -> x) true;;
139     - : bool = true
140
141 (But `(fun x -> x x)` still won't work.)
142
143 So we can try our usual tricks:
144
145     # (fun x -> true) omega;;
146     - : bool = true
147
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:
151
152     # omega (fun x -> true);;
153
154 Infinite loop.
155
156 Now consider the following variations in behavior:
157
158     # let test = omega omega;;
159     [Infinite loop, need to control c out]
160
161     # let test () = omega omega;;
162     val test : unit -> 'a = <fun>
163
164     # test;;
165     - : unit -> 'a = <fun>
166
167     # test ();;
168     [Infinite loop, need to control c out]
169
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").
173
174 Towards Monads
175 --------------
176
177 So the integer division operation presupposes that its second argument
178 (the divisor) is not zero, upon pain of presupposition failure.
179 Here's what my OCaml interpreter says:
180
181     # 12/0;;
182     Exception: Division_by_zero.
183
184 So we want to explicitly allow for the possibility that 
185 division will return something other than a number.
186 We'll use OCaml's option type, which works like this:
187
188     # type 'a option = None | Some of 'a;;
189     # None;;
190     - : 'a option = None
191     # Some 3;;
192     - : int option = Some 3
193
194 So if a division is normal, we return some number, but if the divisor is
195 zero, we return None:
196
197 <pre>
198 let div (x:int) (y:int) = 
199   match y with 0 -> None |
200                _ -> Some (x / y);;
201
202 (*
203 val div : int -> int -> int option = fun
204 # div 12 3;;
205 - : int option = Some 4
206 # div 12 0;;
207 - : int option = None
208 # div (div 12 3) 2;;
209 Characters 4-14:
210   div (div 12 3) 2;;
211       ^^^^^^^^^^
212 Error: This expression has type int option
213        but an expression was expected of type int
214 *)
215 </pre>
216
217 This starts off well: dividing 12 by 3, no problem; dividing 12 by 0,
218 just the behavior we were hoping for.  But we want to be able to use
219 the output of the safe-division function as input for further division
220 operations.  So we have to jack up the types of the inputs:
221
222 <pre>
223 let div (x:int option) (y:int option) = 
224   match y with None -> None |
225                Some 0 -> None |
226                Some n -> (match x with None -> None |
227                                        Some m -> Some (m / n));;
228
229 (*
230 val div : int option -> int option -> int option = <fun>
231 # div (Some 12) (Some 4);;
232 - : int option = Some 3
233 # div (Some 12) (Some 0);;
234 - : int option = None
235 # div (div (Some 12) (Some 0)) (Some 4);;
236 - : int option = None
237 *)
238 </pre>
239
240 Beautiful, just what we need: now we can try to divide by anything we
241 want, without fear that we're going to trigger any system errors.
242
243 I prefer to line up the `match` alternatives by using OCaml's 
244 built-in tuple type:
245
246 <pre>
247 let div (x:int option) (y:int option) = 
248   match (x, y) with (None, _) -> None |
249                     (_, None) -> None |
250                     (_, Some 0) -> None |
251                     (Some m, Some n) -> Some (m / n);;
252 </pre>
253
254 So far so good.  But what if we want to combine division with 
255 other arithmetic operations?  We need to make those other operations 
256 aware of the possibility that one of their arguments will trigger a
257 presupposition failure:
258
259 <pre>
260 let add (x:int option) (y:int option) = 
261   match (x, y) with (None, _) -> None |
262                     (_, None) -> None |
263                     (Some m, Some n) -> Some (m + n);;
264
265 (*
266 val add : int option -> int option -> int option = <fun>
267 # add (Some 12) (Some 4);;
268 - : int option = Some 16
269 # add (div (Some 12) (Some 0)) (Some 4);;
270 - : int option = None
271 *)
272 </pre>
273
274 This works, but is somewhat disappointing: the `add` operation
275 doesn't trigger any presupposition of its own, so it is a shame that
276 it needs to be adjusted because someone else might make trouble.
277
278 But we can automate the adjustment.  The standard way in OCaml,
279 Haskell, etc., is to define a `bind` operator (the name `bind` is not
280 well chosen to resonate with linguists, but what can you do):
281
282 <pre>
283 let bind (x: int option) (f: int -> (int option)) = 
284   match x with None -> None | 
285                Some n -> f n;;
286
287 let add (x: int option) (y: int option)  =
288   bind x (fun x -> bind y (fun y -> Some (x + y)));;
289
290 let div (x: int option) (y: int option) =
291   bind x (fun x -> bind y (fun y -> if (0 = y) then None else Some (x / y)));;
292
293 (*
294 #  div (div (Some 12) (Some 2)) (Some 4);;
295 - : int option = Some 1
296 #  div (div (Some 12) (Some 0)) (Some 4);;
297 - : int option = None
298 # add (div (Some 12) (Some 0)) (Some 4);;
299 - : int option = None
300 *)
301 </pre>
302
303 Compare the new definitions of `add` and `div` closely: the definition
304 for `add` shows what it looks like to equip an ordinary operation to
305 survive in dangerous presupposition-filled world.  Note that the new
306 definition of `add` does not need to test whether its arguments are
307 None objects or real numbers---those details are hidden inside of the
308 `bind` function.
309
310 The definition of `div` shows exactly what extra needs to be said in
311 order to trigger the no-division-by-zero presupposition.
312
313 For linguists: this is a complete theory of a particularly simply form
314 of presupposition projection (every predicate is a hole).