From 7c6b9557ee34b8106123687679fe43092fc48103 Mon Sep 17 00:00:00 2001 From: jim Date: Mon, 23 Mar 2015 10:17:11 -0400 Subject: [PATCH] use arrow for mid --- exercises/assignment7.mdwn | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/exercises/assignment7.mdwn b/exercises/assignment7.mdwn index 7ec7a472..f26f5d83 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 = -- 2.11.0