restore Chris's double boxes

[lambda.git] / topics / week7_introducing_monads.mdwn

diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index 4b6ed35..718677e 100644 (file)
--- a/topics/week7_introducing_monads.mdwn
+++ b/topics/week7_introducing_monads.mdwn
@@ -83,18 +83,17 @@ For instance, the following are Kleisli arrows:
 
 In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type <code><u>Q</u></code> is <code><u>bool</u></code>).
 
 
 In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type <code><u>Q</u></code> is <code><u>bool</u></code>).
 

-Note that the left-hand schema `P` is permitted to itself be a boxed
-type. That is, if `α list` is our box type, and `P` is to boxed type
-`int list`, we can write the boxed type that has `P` as its left-hand
-side as
+Note that either of the schemas `P` or `Q` are permitted to themselves be boxed
+types. That is, if `α list` is our box type, we can write the second type as:

 
 <code><u>int</u> -> <u>int list</u></code>
 
 
 <code><u>int</u> -> <u>int list</u></code>
 

-If it's clear that we're uniformly talking about the same box type (in
-this example, `α list`), we can equivalently write
+And also what the rhs there is a boxing of is itself a boxed type (with the same kind of box):, so we can write it as:

 
 <code><u>int</u> -> <span class="box2">int</span></code>
 
 
 <code><u>int</u> -> <span class="box2">int</span></code>
 

+We have to be careful though not to to unthinkingly equivocate between different kinds of boxes.
+

 Here are some examples of values of these Kleisli arrow types, where the box type is `α list`, and the Kleisli arrow types are <code>int -> <u>int</u></code> (that is, `int -> int list`) or <code>int -> <u>bool</u></code>:
 
 <pre>\x. [x]
 Here are some examples of values of these Kleisli arrow types, where the box type is `α list`, and the Kleisli arrow types are <code>int -> <u>int</u></code> (that is, `int -> int list`) or <code>int -> <u>bool</u></code>:
 
 <pre>\x. [x]


@@ -125,7 +124,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>
 
 
 <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>
 
 
 <code>&lt;=&lt; or mcomp : (Q -> <u>R</u>) -> (P -> <u>Q</u>) -> (P -> <u>R</u>)</code>
 


@@ -143,7 +142,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 `μ`.
 
 
 > 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.)
 
 
 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 +175,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)`
 
     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
 
 *   ***Monad*** (or "Composables") A MapNable box type is a *Monad* if there
        is in addition an associative `mcomp` having `mid` as its left and