edits
[lambda.git] / topics / _week8_reader_monad.mdwn
index 9bbc015..557bd2f 100644 (file)
@@ -1,5 +1,7 @@
 <!-- λ Λ ∀ ≡ α β γ ρ ω Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ¢ ⇧ -->
 
+[[!toc levels=2]]
+
 The Reader Monad
 ================
 
@@ -149,171 +151,7 @@ is the ⇧ and the map2 function from the notes on safe division:
 Then we lift the entire computation into the monad by applying ⇧ to
 the integers, and by applying `map1` to the operators:
 
-\tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
-
-     ___________________
-     |                 |
-  ___|____         ____|_____
-  |      |         |        |
-map2 +  ⇧1    _____|_____  ⇧4
-              |         |
-            map2 *  ____|____
-                    |       |
-                 ___|____  ⇧0
-                 |      |
-               map2 /  ⇧6
-
-With these adjustments, the faulty computation now completes smoothly:
-
-    1. Reduce head ((map2 +)  -->
-
-The Reader Monad
-================
-
-The goal for this part is to introduce the Reader Monad, and present
-two linguistics applications: binding and intensionality.  Along the
-way, we'll continue to think through issues related to order, and a
-related notion of flow of information.
-
-At this point, we've seen monads in general, and three examples of
-monads: the identity monad (invisible boxes), the Maybe monad (option
-types), and the List monad.  
-
-We've also seen an application of the Maybe monad to safe division.
-The starting point was to allow the division function to return an int
-option instead of an int.  If we divide 6 by 2, we get the answer Just
-3.  But if we divide 6 by 0, we get the answer Nothing.  
-
-The next step was to adjust the other arithmetic functions to know how
-to handle receiving Nothing instead of a (boxed) integer.  This meant
-changing the type of their input from ints to int options.  But we
-didn't need to do this piecemeal; rather, we could "lift" the ordinary
-arithmetic operations into the monad using the various tools provided
-by the monad.  
-
-So let's see how this works in terms of a specific computation.
-
 <pre>
-\tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))
-
- ___________
- |         |
-_|__    ___|___
-|  |    |     |
-+  1  __|___  4
-      |    |
-      *  __|___
-         |    |
-        _|__  2
-        |  |
-        /  6
-</pre>
-
-This computation should reduce to 13.  But given a specific reduction
-strategy, we can watch the order in which the computation proceeds.
-Following on the lambda evaluator developed during the previous
-homework, let's adopt the following reduction strategy:
-
-    In order to reduce (head arg), do the following in order:
-    1. Reduce head to h'
-    2. Reduce arg to a'.
-    3. If (h' a') is a redex, reduce it.
-
-There are many details left unspecified here, but this will be enough
-for today.  The order in which the computation unfolds will be
-
-    1. Reduce head (+ 1) to itself
-    2. Reduce arg ((* (/ 6 2)) 3)
-         1. Reduce head (* ((/ 6) 2))
-              1. Reduce head * 
-              2. Reduce arg ((/ 6) 2)
-                   1. Reduce head (/ 6) to itself
-                   2. Reduce arg 2 to itself
-                   3. Reduce ((/ 6) 2) to 3
-              3. Reduce (* 3) to itself
-         2. Reduce arg 4 to itself
-         3. Reduce ((* 3) 4) to 12
-     3. Reduce ((+ 1) 12) to 13
-
-This reduction pattern follows the structure of the original
-expression exactly, at each node moving first to the left branch,
-processing the left branch, then moving to the right branch, and
-finally processing the results of the two subcomputation.  (This is
-called depth-first postorder traversal of the tree.)
-
-It will be helpful to see how the types change as we make adjustments.
-
-    type num = int
-    type contents = Num of num   | Op of (num -> num -> num)
-    type tree = Leaf of contents | Branch of tree * tree
-
-Never mind that these types will allow us to construct silly
-arithmetric trees such as `+ *` or `2 3`.  Note that during the
-reduction sequence, the result of reduction was in every case a
-well-formed subtree.  So the process of reduction could be animated by
-replacing subtrees with the result of reduction on that subtree, till
-the entire tree is replaced by a single integer (namely, 13).
-
-Now we replace the number 2 with 0:
-
-<pre>
-\tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
-
- ___________
- |         |
-_|__    ___|___
-|  |    |     |
-+  1  __|___  4
-      |    |
-      *  __|___
-         |    |
-        _|__  0
-        |  |
-        /  6
-</pre>
-
-When we reduce, we get quite a ways into the computation before things
-go south:
-
-    1. Reduce head (+ 1) to itself
-    2. Reduce arg ((* (/ 6 0)) 3)
-         1. Reduce head (* ((/ 6) 0))
-              1. Reduce head * 
-              2. Reduce arg ((/ 6) 0)
-                   1. Reduce head (/ 6) to itself
-                   2. Reduce arg 0 to itself
-                   3. Reduce ((/ 6) 0) to ACKKKK
-
-This is where we replace `/` with `safe-div`.  This means changing the
-type of the arithmetic operators from `int -> int -> int` to 
-`int -> int -> int option`; and since we now have to anticipate the
-possibility that any argument might involve division by zero inside of
-it, here is the net result for our types:
-
-    type num = int option
-    type contents = Num of num   | Op of (num -> num -> num)
-    type tree = Leaf of contents | Branch of tree * tree
-
-The only difference is that instead of defining our numbers to be
-simple integers, they are now int options; and so Op is an operator
-over int options.
-
-At this point, we bring in the monadic machinery.  In particular, here
-is the ⇧ and the map2 function from the notes on safe division:
-
-    ⇧ (a: 'a) = Just a;;
-
-    map2 (g : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) =
-      match u with
-      | None -> None
-      | Some x ->
-          (match v with
-          | None -> None
-          | Some y -> Some (g x y));;
-
-Then we lift the entire computation into the monad by applying ⇧ to
-the integers, and by applying `map1` to the operators:
-
 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
 
      ___________________
@@ -327,6 +165,7 @@ map2 +  ⇧1    _____|_____  ⇧4
                  ___|____  ⇧0
                  |      |
                map2 /  ⇧6
+</pre>
 
 With these adjustments, the faulty computation now completes smoothly: