author jim Mon, 23 Mar 2015 14:17:11 +0000 (10:17 -0400) committer Linux User Mon, 23 Mar 2015 14:17:11 +0000 (10:17 -0400)

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 =