use arrow for mid
authorjim <jim@web>
Mon, 23 Mar 2015 14:17:11 +0000 (10:17 -0400)
committerLinux User <ikiwiki@localhost.members.linode.com>
Mon, 23 Mar 2015 14:17:11 +0000 (10:17 -0400)
exercises/assignment7.mdwn

index 7ec7a47..f26f5d8 100644 (file)
@@ -78,7 +78,7 @@ boxed types.  Here, a "boxed type" is a type function with one unsaturated
 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 <code>mid : P-> <u>P</u></code>, and a
+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
@@ -86,19 +86,19 @@ is just `>=>` with its arguments flipped. `<=<` has the virtue that it correspon
 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 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))
@@ -119,7 +119,7 @@ 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 values of type `'a`.  The `mid`
+`'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 =