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 =