Merge branch 'working'
[lambda.git] / exercises / assignment7.mdwn
index bd614b3..029a779 100644 (file)
@@ -75,30 +75,30 @@ This part of the exercise is the "V2" part of that code.
 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-><u>Q</u>) -> (Q-><u>R</u>) -> (P-><u>R</u>)`.
+Recall that a monad requires a singleton function <code>⇧ (\* mid \*) : P-> <u>P</u></code>, and a
+composition operator like <code>&gt;=&gt; : (P-><u>Q</u>) -> (Q-><u>R</u>) -> (P-><u>R</u>)</code>.
 
 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))
@@ -107,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
@@ -119,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))
@@ -129,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.