Merge branch 'working'
[lambda.git] / exercises / assignment7.mdwn
index 3d21629..ea387b9 100644 (file)
@@ -67,19 +67,16 @@ to it here soon.
 
 ## Monads
 
-Mappables (functors), MapNables (applicatives functors), and Monads
+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.
 
 Recall that a monad requires a singleton function `mid : P-> MP`, and a
-composition operator `>=> : (P->MQ) -> (Q->MR) -> (P->MR)`. The type for
-the composition operator stated here corrects a typo in the class handout.
-Also, in the handout we called `mid` `𝟭`. But now we've decided that `mid`
-is better. (Think of it as "m" plus "identity", not as the start of "midway".)
+composition operator like `>=> : (P-><u>Q</u>) -> (Q-><u>R</u>) -> (P-><u>R</u>)`.
 
-We will also move freely back and forth between using `>=>` and using `<=<` (aka `mcomp`), which
+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.
@@ -93,7 +90,7 @@ Anyway, `mid` and (let's say) `<=<` have to obey the following Monad Laws:
 For example, the Identity monad has the identity function `I` for `mid`
 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 `mid` 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
@@ -101,30 +98,30 @@ suitable for `mid` and `>=>`:
     (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))
 
-1.  On a number of occasions, we've used the Option type to make our
+1.  On a number of occasions, we've used the Option/Maybe type to make our
 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.  Borrowing the notation of OCaml, let's say that
+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.
 More specifically,
 
         type 'a option = None | Some 'a
 
-(If you have trouble keeping straight what is the OCaml terminology for this and what is the Haskell terminology, don't worry, we do too.)
+    (If you have trouble keeping straight what is the OCaml terminology for this and what is the Haskell terminology, don't worry, we do too.)
 
-Now the obvious singleton for the Option monad is `\p. Just p`.  Give
+    Now the obvious singleton for the Option monad is `\p. Some p`.  Give
 (or reconstruct) either of the composition operators `>=>` or `<=<`.
 Show that your composition operator obeys the Monad Laws.
 
-2.   Do the same with lists.  That is, given an arbitrary type
+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:
 
         let (>=>) (j : 'a -> 'b list) (k : 'b -> 'c list) : 'a -> 'c list =
           fun a -> List.flatten (List.map k (j a))
 
-For example:
+    For example:
 
-     let j a = [a; a+1];;
-     let k b = [b*b; b+b];;
-     (j >=> k) 7 (* ==> [49; 14; 64; 16] *)
+        let j a = [a; a+1];;
+        let k b = [b*b; b+b];;
+        (j >=> k) 7 (* ==> [49; 14; 64; 16] *)