From: jim <jim@web>
Date: Sun, 22 Mar 2015 16:14:20 +0000 (-0400)
Subject: refinements, diagrams
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=5b304e0cbe18ba3bc9b372e3ca8faf3edaa4e8e5;ds=sidebyside

refinements, diagrams
---

diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index d73d4cbb..0e9ab56f 100644
--- a/topics/week7_introducing_monads.mdwn
+++ b/topics/week7_introducing_monads.mdwn
@@ -327,6 +327,10 @@ Identity is a monad.  Here is a demonstration that the laws hold:
 
 The Identity monad is favored by mimes.
 
+
+
+
+
 To take a slightly less trivial (and even more useful) example,
 consider the box type `α list`, with the following operations:
 
@@ -358,8 +362,51 @@ Contrast that to `m$` (`mapply`), which operates not on two *box-producing funct
     let xs = [7, 5] in
     mapply js xs ==> [49, 25, 14, 10]
 
+These implementations of `<=<` and `m$` for lists use the "crossing" strategy for pairing up multiple lists, as opposed to the "zipping" strategy. Nothing forces that choice; you could also define `m$` using the "zipping" strategy instead. (But then you wouldn't be able to build a corresponding Monad; see below.) Haskell talks of the List Monad in the first case, and the ZipList Applicative in the second case.
+
+Sticking with the "crossing" strategy, here's how to motivate our implementation of `<=<`. Recall that we have on the one hand, an operation `filter` for lists, that applies a predicate to each element of the list, and returns a list containing only those elements which satisfied the predicate. But the elements it does retain, it retains unaltered. On the other hand, we have the operation `map` for lists, that is capable of _changing_ the list elements in the result. But it doesn't have the power to throw list elements away; elements in the source map one-to-one to elements in the result. In many cases, we want something in between `filter` and `map`. We want to be able to ignore or discard some list elements, and possibly also to change the list elements we keep. One way of doing this is to have a function `optmap`, defined like this:
+
+    let rec optmap (f : α -> β option) (xs : α list) : β list =
+      match xs with
+      | [] -> []
+      | x' :: xs' ->
+          (match f x' with
+          | None -> optmap f xs'
+          | Some b -> b :: optmap f xs')
+
+Then we retain only those `α`s for which `f` returns `Some b`; when `f` returns `None`, we just leave out any corresponding element in the result.
+
+That can be helpful, but it only enables us to have _zero or one_ elements in the result corresponding to a given element in the source list. What if we sometimes want more? Well, here is a more general approach:
+
+    let rec catmap (k : α -> β list) (xs : α list) : β list =
+      match xs with
+      | [] -> []
+      | x' :: xs' -> List.append (k x') (catmap f xs')
+
+Now we can have as many elements in the result for a given `α` as `k` cares to return. Another way to write `catmap k xs` is as `List.concat (map k xs)`. And this is just the definition of `mbind` or `>>=` for the List Monad. The definition of `mcomp` or `<=<`, that we gave above, differs only in that it's the way to compose two functions `j` and `k`, that you'd want to `catmap`, rather than the way to `catmap` one of those functions over a value that's already a list.
+
+This example is a good intuitive basis for thinking about the notions of `mbind` and `mcomp` more generally. Thus `mbind` for the option/Maybe type takes an option value, applies `k` to its element (if there is one), and returns the resulting option value. `mbind` for a tree with `α`-labeled leaves would apply `k` to each of the leaves, and return a tree containing arbitrarily large subtrees in place of all its former leaves, depending on what `k` returned.
+
+<pre>
+[3, 2, 0, 1]  >>=<sub>α list</sub>    (\a -> dup a a)  ==>  [3, 3, 3, 2, 2, 1]
+
+      Some a  >>=<sub>α option</sub>  (\a -> Some 0) ==> Some 0
+      None    >>=<sub>α option</sub>  (\a -> Some 0) ==> None
+
+    .                                                   _____
+   / \                                  .              /     \
+  .   3       >>=<sub>(α,unit) tree</sub>  (\a ->  / \  )  ==>   _/_      .
+ / \                                  a   a         /   \    / \
+1   2                                              .     .  3   3
+                                                  / \   / \
+                                                 1   1 2   2
+</pre>
+
+
+Though as we warned before, only some of the Monads we'll be working with are naturally thought of "containers"; so in other cases the similarity of their `mbind` operations to what we have here will be more abstract.
+
 
-The question came up in class of when box types might fail to be Mappable, or Mappables might fail to be MapNables, or MapNables might fail to be Monads.
+The question came up in class of **when box types might fail to be Mappable, or Mappables might fail to be MapNables, or MapNables might fail to be Monads**.
 
 For the first failure, we noted that it's easy to define a `map` operation for the box type `R -> α`, for a fixed type `R`. You `map` a function of type `P -> Q` over a value of the boxed type <code><u>P</u></code>, that is a value of type `R -> P`, by just returning a function that takes some `R` as input, first supplies it to your `R -> P` value, and then supplies the result to your `map`ped function of type `P -> Q`. (We will be working with this Mappable extensively; in fact it's not just a Mappable but more specifically a Monad.)