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.
 
 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
 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.
 
 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
 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))
 
     (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
 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 =
 is the singleton function `\p. [p]`, and the composition operator is:
 
         let (>=>) (j : 'a -> 'b list) (k : 'b -> 'c list) : 'a -> 'c list =