X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=exercises%2Fassignment7.mdwn;h=029a7798c182c8c0125848c9f6e70089a4baec77;hb=d3be9d07f791548dd8bb9b54d07e3b666cfa2379;hp=7ec7a4726fbb60a961e2de459039578b00c033db;hpb=c7724ab43624fa37c971971f40799c2d5527fac0;p=lambda.git
diff --git a/exercises/assignment7.mdwn b/exercises/assignment7.mdwn
index 7ec7a472..029a7798 100644
--- a/exercises/assignment7.mdwn
+++ b/exercises/assignment7.mdwn
@@ -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 mid : P-> P
, and a
+Recall that a monad requires a singleton function ⧠(\* mid \*) : P-> P
, and a
composition operator like >=> : (P->Q) -> (Q->R) -> (P->R)
.
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 =