From 80ad862c64373ac07b6e33236a47a50e98583d62 Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sun, 24 Oct 2010 17:08:05 -0400 Subject: [PATCH] week 6 start --- assignment5.mdwn | 110 +++++++++++++++++++++++++++++++++++ week6.mdwn | 172 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 282 insertions(+) create mode 100644 assignment5.mdwn create mode 100644 week6.mdwn diff --git a/assignment5.mdwn b/assignment5.mdwn new file mode 100644 index 00000000..87d5566c --- /dev/null +++ b/assignment5.mdwn @@ -0,0 +1,110 @@ +Types and OCAML + +1. Which of the following expressions is well-typed in OCAML? + For those that are, give the type of the expression as a whole. + For those that are not, why not? + + let rec f x = f x;; + + let rec f x = f f;; + + let rec f x = f x in f f;; + + let rec f x = f x in f ();; + + let rec f () = f f;; + + let rec f () = f ();; + + let rec f () = f () in f f;; + + let rec f () = f () in f ();; + +2. Throughout this problem, assume that we have + + let rec omega x = omega x;; + + All of the following are well-typed. + Which ones terminate? What are the generalizations? + + omega;; + + omega ();; + + fun () -> omega ();; + + (fun () -> omega ()) ();; + + if true then omega else omega;; + + if false then omega else omega;; + + if true then omega else omega ();; + + if false then omega else omega ();; + + if true then omega () else omega;; + + if false then omega () else omega;; + + if true then omega () else omega ();; + + if false then omega () else omega ();; + + let _ = omega in 2;; + + let _ = omega () in 2;; + +3. The following expression is an attempt to make explicit the +behavior of `if`-`then`-`else` explored in the previous question. +The idea is to define an `if`-`then`-`else` expression using +other expression types. So assume that "yes" is any OCAML expression, +and "no" is any other OCAML expression (of the same type as "yes"!), +and that "bool" is any boolean. Then we can try the following: +"if bool then yes else no" should be equivalent to + + let b = bool in + let y = yes in + let n = no in + match b with true -> y | false -> n + +This almost works. For instance, + + if true then 1 else 2;; + +evaluates to 1, and + + let b = true in let y = 1 in let n = 2 in + match b with true -> 1 | false -> 2;; + +also evaluates to 1. Likewise, + + if false then 1 else 2;; + +and + + let b = false in let y = 1 in let n = 2 in + match b with true -> y | false -> n;; + +both evaluate to 2. + +However, + + let rec omega x = omega x in + if true then omega else omega ();; + +terminates, but + + let rec omega x = omega x in + let b = true in + let y = omega in + let n = omega () in + match b with true -> y | false -> n;; + +does not terminate. Incidentally, `match bool with true -> yes | +false -> no;;` works as desired, but your assignment is to solve it +without using the magical evaluation order properties of either `if` +or of `match`. That is, you must keep the `let` statements, though +you're allowed to adjust what `b`, `y`, and `n` get assigned to. + +[[Hint assignment 5 problem 3]] 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"). + -- 2.11.0