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 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:
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;;
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.
198 let div' (x:int) (y:int) =
199 match y with 0 -> None |
203 val div' : int -> int -> int option = fun
205 - : int option = Some 4
207 - : int option = None
208 # div' (div' 12 3) 2;;
212 Error: This expression has type int option
213 but an expression was expected of type int
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:
223 let div' (x:int option) (y:int option) =
224 match y with None -> None |
226 Some n -> (match x with None -> None |
227 Some m -> Some (m / n));;
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
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
247 let div' (x:int option) (y:int option) =
248 match (x, y) with (None, _) -> None |
250 (_, Some 0) -> None |
251 (Some m, Some n) -> Some (m / n);;
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:
260 let add' (x:int option) (y:int option) =
261 match (x, y) with (None, _) -> None |
263 (Some m, Some n) -> Some (m + n);;
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
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.
283 let bind' (x: int option) (f: int -> (int option)) =
284 match x with None -> None |
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)));;
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
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
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).