X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=exercises%2Fassignment7.mdwn;h=f26f5d834912a1d846855645033f2514a82f3538;hb=29fb3ed9c63e37aeaeef765c1c11986bd1f84f41;hp=ea387b93cebea8d9453e76f9b6af6012619c751f;hpb=801480959fd53e08278383acc1471a2e994b7a36;p=lambda.git
diff --git a/exercises/assignment7.mdwn b/exercises/assignment7.mdwn
index ea387b93..f26f5d83 100644
--- a/exercises/assignment7.mdwn
+++ b/exercises/assignment7.mdwn
@@ -42,8 +42,13 @@ Instead, we're going to give you almost the complete program, with a few gaps
in it that you have to complete. You have to understand enough to
add the last pieces to make the program function.
-We're still writing up the (substantial) exposition of this, and will post a link
-to it here soon.
+You can find the skeleton code [[here|/code/untyped_evaluator.ml]].
+
+We've also prepared a much fuller version, that has user-friendly input
+and printing of results. We'll provide a link to that shortly. It
+will be easiest for you to understand that code if you've
+completed the gaps in the simplified skeleton linked above.
+
## Evaluation in the untyped lambda calculus: environments
@@ -61,8 +66,8 @@ since it amounts to evaluating terms relative to an assignment
function. The difference between the substitute-and-repeat approach
above, and this approach, is one huge step towards monads.
-We're still writing up the exposition of this, too, and will post a link
-to it here soon.
+The skeleton code for this is at the [[same link as before|/code/untyped_evaluator.ml]].
+This part of the exercise is the "V2" part of that code.
## Monads
@@ -70,30 +75,30 @@ to it here soon.
Mappables (functors), MapNables (applicative functors), and Monads
(composables) are ways of lifting computations from unboxed types into
boxed types. Here, a "boxed type" is a type function with one unsaturated
-hole (which may have several occurrences). We can think of the box type
-as a function from a type to a type. Call this type function M, and let P, Q, R, and S be schematic variables over types.
+hole (which may have several occurrences, as in `(α,α) tree`). We can think of the box type
+as a function from a type to a type.
-Recall that a monad requires a singleton function `mid : P-> MP`, and a
-composition operator like `>=> : (P->Q) -> (Q->R) -> (P->R)`.
+Recall that a monad requires a singleton function ⧠(* mid *) : P-> P
, and a
+composition operator like >=> : (P->Q) -> (Q->R) -> (P->R)
.
As we said in the notes, we'll move freely back and forth between using `>=>` and using `<=<` (aka `mcomp`), which
is just `>=>` with its arguments flipped. `<=<` has the virtue that it corresponds more
closely to the ordinary mathematical symbol `â`. But `>=>` has the virtue
that its types flow more naturally from left to right.
-Anyway, `mid` and (let's say) `<=<` have to obey the following Monad Laws:
+Anyway, `mid`/`â§` and (let's say) `<=<` have to obey the Monad Laws:
- mid <=< k = k
- k <=< mid = k
- j <=< (k <=< l) = (j <=< k) <=< l
+ ⧠<=< k == k
+ k <=< ⧠== k
+ j <=< (k <=< l) == (j <=< k) <=< l
-For example, the Identity monad has the identity function `I` for `mid`
+For example, the Identity monad has the identity function `I` for `â§`
and ordinary function composition `â` for `<=<`. It is easy to prove
that the laws hold for any terms `j`, `k`, and `l` whose types are
-suitable for `mid` and `<=<`:
+suitable for `â§` and `<=<`:
- mid <=< k == I â k == \p. I (k p) ~~> \p. k p ~~> k
- k <=< mid == k â I == \p. k (I p) ~~> \p. k p ~~> k
+ ⧠<=< k == I â k == \p. I (k p) ~~> \p. k p ~~> k
+ k <=< ⧠== k â I == \p. k (I p) ~~> \p. k p ~~> k
(j <=< k) <=< l == (\p. j (k p)) â l == \q. (\p. j (k p)) (l q) ~~> \q. j (k (l q))
j <=< (k <=< l) == j â (k â l) == j â (\p. k (l p)) == \q. j ((\p. k (l p)) q) ~~> \q. j (k (l q))
@@ -102,7 +107,7 @@ suitable for `mid` and `<=<`:
conceptual world neat and tidy (for instance, think of [[our discussion
of Kaplan's Plexy|topics/week6_plexy]]). As we learned in class, there is a natural monad
for the Option type. Using the vocabulary of OCaml, let's say that
-"`'a option`" is the type of a boxed `'a`, whatever type `'a` is.
+`'a option` is the type of a boxed `'a`, whatever type `'a` is.
More specifically,
type 'a option = None | Some 'a
@@ -114,8 +119,8 @@ More specifically,
Show that your composition operator obeys the Monad Laws.
2. Do the same with lists. That is, given an arbitrary type
-`'a`, let the boxed type be `['a]` or `'a list`, that is, lists of objects of type `'a`. The singleton
-is `\p. [p]`, and the composition operator is:
+`'a`, let the boxed type be `['a]` or `'a list`, that is, lists of values of type `'a`. The `â§`
+is the singleton function `\p. [p]`, and the composition operator is:
let (>=>) (j : 'a -> 'b list) (k : 'b -> 'c list) : 'a -> 'c list =
fun a -> List.flatten (List.map k (j a))
@@ -124,4 +129,9 @@ is `\p. [p]`, and the composition operator is:
let j a = [a; a+1];;
let k b = [b*b; b+b];;
- (j >=> k) 7 (* ==> [49; 14; 64; 16] *)
+ (j >=> k) 7
+ (* which OCaml evaluates to:
+ - : int list = [49; 14; 64; 16]
+ *)
+
+ Show that these obey the Monad Laws.