Date: Fri, 20 Mar 2015 12:59:49 0400
Subject: [PATCH] refinements

topics/week7_introducing_monads.mdwn  38 ++++++++++++++++++++++
1 file changed, 23 insertions(+), 15 deletions()
diff git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index 5bc139f5..1911566a 100644
 a/topics/week7_introducing_monads.mdwn
+++ b/topics/week7_introducing_monads.mdwn
@@ 83,18 +83,10 @@ For instance, the following are Kleisli arrows:
In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type Q
is bool
).
Note that the lefthand schema `P` is permitted to itself be a boxed
type. That is, if `Î± list` is our box type, and `P` is the boxed type
`int list`, we can write the boxed type that has `P` as its lefthand
side as
+Note that the lefthand schema `P` is permitted to itself be a boxed type. That is, where if `Î± list` is our box type, we can write the second type as:
int > int list
If it's clear that we're uniformly talking about the same box type (in
this example, `Î± list`), we can equivalently write

int > int

Here are some examples of values of these Kleisli arrow types, where the box type is `Î± list`, and the Kleisli arrow types are int > int
(that is, `int > int list`) or int > bool
:
\x. [x]
@@ 125,7 +117,7 @@ Here are the types of our crucial functions, together with our pronunciation, an
m$ or mapply (/Îµm@plai/): P > Q > P > Q
> We'll use `m$` as an infix operator, reminiscent of `$` which is just ordinary function application (also expressed by mere juxtaposition). In the class presentation Jim called `m$` `â`. In Haskell, it's called `Control.Monad.ap` or `Control.Applicative.<*>`.
+> We'll use `m$` as a leftassociative infix operator, reminiscent of (the rightassociative) `$` which is just ordinary function application (also expressed by mere leftassociative juxtaposition). In the class presentation Jim called `m$` `â`. In Haskell, it's called `Control.Monad.ap` or `Control.Applicative.<*>`.
<=< or mcomp : (Q > R) > (P > Q) > (P > R)
@@ 143,7 +135,7 @@ Here are the types of our crucial functions, together with our pronunciation, an
> In Haskell, this is `Control.Monad.join`. In other theoretical contexts it is sometimes called `Î¼`.
Haskell uses the symbol `>>=` but calls it "bind". This is not well chosen from the perspective of formal semantics, but it's too deeply entrenched to change. We've at least preprended an `m` to the front of "bind".
+Haskell uses the symbol `>>=` but calls it "bind". This is not well chosen from the perspective of formal semantics, but it's too deeply entrenched to change. We've at least preprended an "m" to the front of "bind".
Haskell's names "return" and "pure" for `mid` are even less well chosen, and we think it will be clearer in our discussion to use a different name. (Also, in other theoretical contexts this notion goes by other names, anyway, like `unit` or `Î·`  having nothing to do with `Î·`reduction in the Lambda Calculus.)
@@ 176,10 +168,26 @@ has to obey the following Map Laws:
1. mid (id : P>P) : P > P
is a left identity for `m$`, that is: `(mid id) m$ xs = xs`
2. `mid (f a) = (mid f) m$ (mid a)`
 3. The `map2`ing of composition onto boxes `fs` and `gs` of functions, when `m$`'d to a box `xs` of arguments == the `m$`ing of `fs` to the `m$`ing of `gs` to xs: `((mid â) m$ fs m$ gs) m$ xs = fs m$ (gs m$ xs)`.
 4. When the arguments are `mid`'d, the order of `m$`ing doesn't matter: `fs m$ (mid x) = (mid ($ x)) m$ fs`. In examples we'll be working with at first, order _never_ matters; but down the road, sometimes it will. This Law states a class of cases where it's guaranteed not to.
 5. A consequence of the laws already stated is that when the functions are `mid`'d, the order of `m$`ing doesn't matter either: TODO

+ 3. The `map2`ing of composition onto boxes `fs` and `gs` of functions, when `m$`'d to a box `xs` of arguments == the `m$`ing of `fs` to the `m$`ing of `gs` to xs: `(mid (â) m$ fs m$ gs) m$ xs = fs m$ (gs m$ xs)`.
+ 4. When the arguments are `mid`'d, the order of `m$`ing doesn't matter: `fs m$ (mid x) = mid ($x) m$ fs`. (Note that it's `mid ($x)`, or `mid (\f. f x)` that gets `m$`d onto `fs`, not the original `mid x`.) Here's an example where the order *does* matter: `[succ,pred] m$ [1,2] == [2,3,0,1]`, but `[($1),($2)] m$ [succ,pred] == [2,0,3,1]`. This Law states a class of cases where the order is guaranteed not to matter.
+ 5. A consequence of the laws already stated is that when the functions are `mid`'d, the order of `m$`ing doesn't matter either: `mid f m$ xs == map (flip ($)) xs m$ mid f`.
+
+
* ***Monad*** (or "Composables") A MapNable box type is a *Monad* if there
is in addition an associative `mcomp` having `mid` as its left and

2.11.0