add mappable laws

[lambda.git] / topics / week7_introducing_monads.mdwn

diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index 14695ec..adcf0cc 100644 (file)
--- a/topics/week7_introducing_monads.mdwn
+++ b/topics/week7_introducing_monads.mdwn
@@ -84,9 +84,9 @@ 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>).
 
 Note that the left-hand schema `P` is permitted to itself be a boxed type. That is, where
-if `α list` is our box type, we can write the second arrow as
+if `α list` is our box type, we can write the second type as:
 
-<code><u>int</u> -> <u>Q</u></code>
+<code><u>int</u> -> <u>int list</u></code>
 
 As semanticists, you are no doubt familiar with the debates between those who insist that propositions are sets of worlds and those who insist they are context change potentials. We hope to show you, in coming weeks, that propositions are (certain sorts of) Kleisli arrows. But this doesn't really compete with the other proposals; it is a generalization of them. Both of the other proposed structures can be construed as specific Kleisli arrows.
 
@@ -107,11 +107,11 @@ Here are the types of our crucial functions, together with our pronunciation, an
 
 <code>&lt;=&lt; or mcomp : (Q -> <u>R</u>) -> (P -> <u>Q</u>) -> (P -> <u>R</u>)</code>
 
-<code>&gt;=&gt; or mpmoc (flip mcomp): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
+<code>&gt;=&gt; (flip mcomp, should we call it mpmoc?): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
 
 <code>&gt;&gt;= or mbind : (<u>Q</u>) -> (Q -> <u>R</u>) -> (<u>R</u>)</code>
 
-<code>=&lt;&lt; or mdnib (flip mbind) (<u>Q</u>) -> (Q -> <u>R</u>) -> (<u>R</u>)</code>
+<code>=&lt;&lt; (flip mbind, should we call it mdnib?) (Q -> <u>R</u>) -> (<u>Q</u>) -> (<u>R</u>)</code>
 
 <code>join: <span class="box2">P</span> -> <u>P</u></code> 
 
@@ -127,7 +127,11 @@ certain useful guarantees.
 if there is a `map` function defined for that box type with the type given above. This
 has to obey the following Map Laws:
 
-    TODO LAWS
+    <code>map (id : α -> α) = (id : <u>α</u> -> <u>α</u>)</code>  
+    <code>map (g ○ f) = (map g) ○ (map f)</code>
+
+    Essentially these say that `map` is a homomorphism from `(α -> β, ○, id)` to <code>(<u>α</u> -> <u>β</u>, ○', id')</code>, where `○'` and `id'` are `○` and `id` restricted to arguments of type <code><u>_</u></code>.
+
 
 *   ***MapNable*** (in Haskelese, "Applicatives") A Mappable box type is *MapNable*
        if there are in addition `map2`, `mid`, and `mapply`.  (Given either