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>>=> : (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
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))
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 =
let j a = [a; a+1];;
let k b = [b*b; b+b];;
- (j >=> k) 7 (* ==> [49; 14; 64; 16] *)
+ (j >=> k) 7
+ (* which OCaml evaluates to:
+ - : int list = [49; 14; 64; 16]
+ *)
+
+ Show that these obey the Monad Laws.