7a5ae2c2af56aa9e84d0c19dc144f2a2962a77a4
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").
175 --------------
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:
181     # 12/0;;
182     Exception: Division_by_zero.
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:
188     # type 'a option = None | Some of 'a;;
189     # None;;
190     - : 'a option = None
191     # Some 3;;
192     - : int option = Some 3
194 So if a division is normal, we return some number, but if the divisor is
195 zero, we return None. As a mnemonic aid, we'll append a `'` to the end of our new divide function.
197 <pre>
198 let div' (x:int) (y:int) =
199   match y with 0 -> None |
200                _ -> Some (x / y);;
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>
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:
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));;
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>
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.
243 I prefer to line up the `match` alternatives by using OCaml's
244 built-in tuple type:
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>
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:
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);;
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>
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.
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). To continue our mnemonic association, we'll put a `'` after the name "bind" as well.
282 <pre>
283 let bind' (x: int option) (f: int -> (int option)) =
284   match x with None -> None |
285                Some n -> f n;;
287 let add' (x: int option) (y: int option)  =
288   bind' x (fun x -> bind' y (fun y -> Some (x + y)));;
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)));;
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>
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.
310 The definition of `div'` shows exactly what extra needs to be said in
311 order to trigger the no-division-by-zero presupposition.
313 For linguists: this is a complete theory of a particularly simply form
314 of presupposition projection (every predicate is a hole).