X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek7_introducing_monads.mdwn;h=1911566abbeeee09f6ee0732a2c347386a8dc50d;hp=4ce25641859817be47cc91a6aa18ce2c06acec4e;hb=6475bb8430df17a74277b7835ba9f2b334a4761f;hpb=1f63d64f765efea28a315af8e92654023bea45cc

diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index 4ce25641..1911566a 100644
--- a/topics/week7_introducing_monads.mdwn
+++ b/topics/week7_introducing_monads.mdwn
@@ -117,7 +117,7 @@ Here are the types of our crucial functions, together with our pronunciation, an
 
 <code>m$ or mapply (/εm@plai/): <u>P -> Q</u> -> <u>P</u> -> <u>Q</u></code>
 
-> 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 left-associative infix operator, reminiscent of (the right-associative) `$` which is just ordinary function application (also expressed by mere left-associative juxtaposition). In the class presentation Jim called `m$` `●`. In Haskell, it's called `Control.Monad.ap` or `Control.Applicative.<*>`.
 
 <code>&lt;=&lt; or mcomp : (Q -> <u>R</u>) -> (P -> <u>Q</u>) -> (P -> <u>R</u>)</code>
 
@@ -135,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.)
 
@@ -168,10 +168,26 @@ has to obey the following Map Laws:
 
     1. <code>mid (id : P->P) : <u>P</u> -> <u>P</u></code> 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`.
+
+<!-- Probably there's a shorter proof, but:
+   mid T m$ xs m$ mid f
+== mid T m$ ((mid id) m$ xs) m$ mid f, by 1
+== mid (○) m$ mid T m$ mid id m$ xs m$ mid f, by 3
+== mid ($id) m$ (mid (○) m$ mid T) m$ xs m$ mid f, by 4
+== mid (○) m$ mid ($id) m$ mid (○) m$ mid T m$ xs m$ mid f, by 3
+== mid ((○) ($id)) m$ mid (○) m$ mid T m$ xs m$ mid f, by 2
+== mid ((○) ($id) (○)) m$ mid T m$ xs m$ mid f, by 2
+== mid id m$ mid T m$ xs m$ mid f, by definitions of ○ and $
+== mid T m$ xs m$ mid f, by 1
+== mid ($f) m$ (mid T m$ xs), by 4
+== mid (○) m$ mid ($f) m$ mid T m$ xs, by 3
+== mid ((○) ($f)) m$ mid T m$ xs, by 2
+== mid ((○) ($f) T) m$ xs, by 2
+== mid f m$ xs, by definitions of ○ and $ and T == flip ($)
+-->
 
 *   ***Monad*** (or "Composables") A MapNable box type is a *Monad* if there
        is in addition an associative `mcomp` having `mid` as its left and