[[!toc]] Types, OCAML ------------ OCAML has type inference: the system can often infer what the type of an expression must be, based on the type of other known expressions. For instance, if we type # let f x = x + 3;; The system replies with val f : int -> int = Since `+` is only defined on integers, it has type # (+);; - : int -> int -> int = The parentheses are there to turn off the trick that allows the two arguments of `+` to surround it in infix (for linguists, SOV) argument order. That is, # 3 + 4 = (+) 3 4;; - : bool = true In general, tuples with one element are identical to their one element: # (3) = 3;; - : bool = true though OCAML, like many systems, refuses to try to prove whether two functional objects may be identical: # (f) = f;; Exception: Invalid_argument "equal: functional value". Oh well. Booleans in OCAML, and simple pattern matching ---------------------------------------------- Where we would write `true 1 2` in our pure lambda calculus and expect it to evaluate to `1`, in OCAML boolean types are not functions (equivalently, are functions that take zero arguments). Selection is accomplished as follows: # if true then 1 else 2;; - : int = 1 The types of the `then` clause and of the `else` clause must be the same. The `if` construction can be re-expressed by means of the following pattern-matching expression: match with true -> | false -> That is, # match true with true -> 1 | false -> 2;; - : int = 1 Compare with # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;; - : int = 9 Unit and thunks --------------- All functions in OCAML take exactly one argument. Even this one: # let f x y = x + y;; # f 2 3;; - : int = 5 Here's how to tell that `f` has been curry'd: # f 2;; - : int -> int = After we've given our `f` one argument, it returns a function that is still waiting for another argument. There is a special type in OCAML called `unit`. There is exactly one object in this type, written `()`. So # ();; - : unit = () Just as you can define functions that take constants for arguments # let f 2 = 3;; # f 2;; - : int = 3;; you can also define functions that take the unit as its argument, thus # let f () = 3;; val f : unit -> int = Then the only argument you can possibly apply `f` to that is of the correct type is the unit: # f ();; - : int = 3 Let's have some fn: think of `rec` as our `Y` combinator. Then # let rec f n = if (0 = n) then 1 else (n * (f (n - 1)));; val f : int -> int = # f 5;; - : int = 120 We can't define a function that is exactly analogous to our ω. We could try `let rec omega x = x x;;` what happens? However, we can do this: # let rec omega x = omega x;; By the way, what's the type of this function? If you then apply this omega to an argument, # omega 3;; the interpreter goes into an infinite loop, and you have to control-C to break the loop. Oh, one more thing: lambda expressions look like this: # (fun x -> x);; - : 'a -> 'a = # (fun x -> x) true;; - : bool = true (But `(fun x -> x x)` still won't work.) So we can try our usual tricks: # (fun x -> true) omega;; - : bool = true OCAML declined to try to evaluate the argument before applying the functor. But remember that `omega` is a function too, so we can reverse the order of the arguments: # omega (fun x -> true);; Infinite loop. Now consider the following variations in behavior: # let test = omega omega;; [Infinite loop, need to control c out] # let test () = omega omega;; val test : unit -> 'a = # test;; - : unit -> 'a = # test ();; [Infinite loop, need to control c out] We can use functions that take arguments of type unit to control execution. In Scheme parlance, functions on the unit type are called *thunks* (which I've always assumed was a blend of "think" and "chunk").