X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week6.mdwn;h=2a4586a01c9b36c546e3aeacbb599a14c3e581d8;hp=e244af75eaf6a74feebf26a26c96c07c9537e8f0;hb=HEAD;hpb=93d67277339f0aed8184a14bbc35ec5060a0c031 diff --git a/week6.mdwn b/week6.mdwn deleted file mode 100644 index e244af75..00000000 --- a/week6.mdwn +++ /dev/null @@ -1,272 +0,0 @@ -[[!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. - -[Note: There is a limited way you can compare functions, using the -`==` operator instead of the `=` operator. Later when we discuss mutation, -we'll discuss the difference between these two equality operations. -Scheme has a similar pair, which they name `eq?` and `equal?`. In Python, -these are `is` and `==` respectively. It's unfortunate that OCaml uses `==` for the opposite operation that Python and many other languages use it for. In any case, OCaml will understand `(f) == f` even though it doesn't understand -`(f) = f`. However, don't expect it to figure out in general when two functions -are identical. (That question is not Turing computable.) - - # (f) == (fun x -> x + 3);; - - : bool = false - -Here OCaml says (correctly) that the two functions don't stand in the `==` relation, which basically means they're not represented in the same chunk of memory. However as the programmer can see, the functions are extensionally equivalent. The meaning of `==` is rather weird.] - - - -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, they're functions that take zero arguments). Instead, 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 - -Now why would that be useful? - -Let's have some fun: 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? - -[Note: if you want to learn more OCaml, you might come back here someday and try: - - # let id x = x;; - val id : 'a -> 'a = - # let unwrap (`Wrap a) = a;; - val unwrap : [< `Wrap of 'a ] -> 'a = - # let omega ((`Wrap x) as y) = x y;; - val omega : [< `Wrap of [> `Wrap of 'a ] -> 'b as 'a ] -> 'b = - # unwrap (omega (`Wrap id)) == id;; - - : bool = true - # unwrap (omega (`Wrap omega));; - - -But we won't try to explain this now.] - - -Even if we can't (easily) express omega in OCaml, we can do this: - - # let rec blackhole x = blackhole x;; - -By the way, what's the type of this function? - -If you then apply this `blackhole` function to an argument, - - # blackhole 3;; - -the interpreter goes into an infinite loop, and you have to type 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.) - -You may also see this: - - # (function x -> x);; - - : 'a -> 'a = - -This works the same as `fun` in simple cases like this, and slightly differently in more complex cases. If you learn more OCaml, you'll read about the difference between them. - -We can try our usual tricks: - - # (fun x -> true) blackhole;; - - : bool = true - -OCaml declined to try to fully reduce the argument before applying the -lambda function. Question: Why is that? Didn't we say that OCaml is a call-by-value/eager language? - -Remember that `blackhole` is a function too, so we can -reverse the order of the arguments: - - # blackhole (fun x -> true);; - -Infinite loop. - -Now consider the following variations in behavior: - - # let test = blackhole blackhole;; - - - # let test () = blackhole blackhole;; - val test : unit -> 'a = - - # test;; - - : unit -> 'a = - - # test ();; - - -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"). - -Question: why do thunks work? We know that `blackhole ()` doesn't terminate, so why do expressions like: - - let f = fun () -> blackhole () - in true - -terminate? - -Bottom type, divergence ------------------------ - -Expressions that don't terminate all belong to the **bottom type**. This is a subtype of every other type. That is, anything of bottom type belongs to every other type as well. More advanced type systems have more examples of subtyping: for example, they might make `int` a subtype of `real`. But the core type system of OCaml doesn't have any general subtyping relations. (Neither does System F.) Just this one: that expressions of the bottom type also belong to every other type. It's as if every type definition in OCaml, even the built in ones, had an implicit extra clause: - - type 'a option = None | Some of 'a;; - type 'a option = None | Some of 'a | bottom;; - -Here are some exercises that may help better understand this. Figure out what is the type of each of the following: - - fun x y -> y;; - - fun x (y:int) -> y;; - - fun x y : int -> y;; - - let rec blackhole x = blackhole x in blackhole;; - - let rec blackhole x = blackhole x in blackhole 1;; - - let rec blackhole x = blackhole x in fun (y:int) -> blackhole y y y;; - - let rec blackhole x = blackhole x in (blackhole 1) + 2;; - - let rec blackhole x = blackhole x in (blackhole 1) || false;; - - let rec blackhole x = blackhole x in 2 :: (blackhole 1);; - - let rec blackhole (x:'a) : 'a = blackhole x in blackhole - - -Back to thunks: the reason you'd want to control evaluation with thunks is to -manipulate when "effects" happen. In a strongly normalizing system, like the -simply-typed lambda calculus or System F, there are no "effects." In Scheme and -OCaml, on the other hand, we can write programs that have effects. One sort of -effect is printing (think of the [[damn]] example at the start of term). -Another sort of effect is mutation, which we'll be looking at soon. -Continuations are yet another sort of effect. None of these are yet on the -table though. The only sort of effect we've got so far is *divergence* or -non-termination. So the only thing thunks are useful for yet is controlling -whether an expression that would diverge if we tried to fully evaluate it does -diverge. As we consider richer languages, thunks will become more useful. - - -Towards Monads --------------- - -This has now been moved to [its own page](/towards_monads). -