X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week6.mdwn;fp=week6.mdwn;h=1839455a6542b7df4b9339222295d6f871b14358;hp=0000000000000000000000000000000000000000;hb=80ad862c64373ac07b6e33236a47a50e98583d62;hpb=55c4880bbefdb5860acfd968f726a4dc48430445 diff --git a/week6.mdwn b/week6.mdwn new file mode 100644 index 00000000..1839455a --- /dev/null +++ b/week6.mdwn @@ -0,0 +1,172 @@ +[[!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` and expect it to evaluate to `1`, in +OCAML boolean types are not functions (equivalently, are functions +that take zero arguments). Choices are made 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 +---- + +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;; + - : book = 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 differences: + + # 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"). +