move Towards Monads to own page

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/assignment5.mdwn b/assignment5.mdwn
index fee1d83..b1f65d2 100644 (file)
--- a/assignment5.mdwn
+++ b/assignment5.mdwn
@@ -210,7 +210,7 @@ value to give back if the argument is the empty list.  Ultimately, we might
 want to make use of our `'a option` technique, but for this assignment, just
 pick a strategy, no matter how clunky. 
 
 want to make use of our `'a option` technique, but for this assignment, just
 pick a strategy, no matter how clunky. 
 

-Be sure to test your proposals with simple lists. (You'll have to make_list
+Be sure to test your proposals with simple lists. (You'll have to `make_list`

 the lists yourself; don't expect OCaml to magically translate between its
 native lists and the ones you buil.d)
 
 the lists yourself; don't expect OCaml to magically translate between its
 native lists and the ones you buil.d)
 


@@ -233,20 +233,20 @@ any auxiliary functions you need.
 Baby monads
 -----------
 
 Baby monads
 -----------
 

-Read the lecture notes for week 6, then write a
-function `lift'` that generalized the correspondence between + and
-`add'`: that is, `lift'` takes any two-place operation on integers
-and returns a version that takes arguments of type `int option`
-instead, returning a result of `int option`.  In other words,
-`lift'` will have type
+Read the material on dividing by zero/towards monads from the end of lecture
+notes for week 6, then write a function `lift'` that generalized the
+correspondence between + and `add'`: that is, `lift'` takes any two-place
+operation on integers and returns a version that takes arguments of type `int
+option` instead, returning a result of `int option`.  In other words, `lift'`
+will have type:

 
        (int -> int -> int) -> (int option) -> (int option) -> (int option)
 
 
        (int -> int -> int) -> (int option) -> (int option) -> (int option)
 

-so that `lift' (+) (Some 3) (Some 4)` will evalute to `Some 7`.  
+so that `lift' (+) (Some 3) (Some 4)` will evalute to `Some 7`.

 Don't worry about why you need to put `+` inside of parentheses.
 You should make use of `bind'` in your definition of `lift'`:
 
 Don't worry about why you need to put `+` inside of parentheses.
 You should make use of `bind'` in your definition of `lift'`:
 

-       let bind' (x: int option) (f: int -> (int option)) =
-               match x with None -> None | Some n -> f n;;
+       let bind' (u: int option) (f: int -> (int option)) =
+               match u with None -> None | Some x -> f x;;

 
 
 
 

diff --git a/index.mdwn b/index.mdwn
index 902bb2e..fd607e6 100644 (file)
--- a/index.mdwn
+++ b/index.mdwn
@@ -36,18 +36,18 @@ arithmetical and list operations, some relatively advanced.
 
 (27 Sept) Lecture notes for [[Week3]];  [[Assignment3]];
 an evaluator with the definitions used for homework 3
 
 (27 Sept) Lecture notes for [[Week3]];  [[Assignment3]];
 an evaluator with the definitions used for homework 3

-preloaded is available at [[assignment 3 evaluator]]. 
+preloaded is available at [[assignment 3 evaluator]].

 
 >      Topics: [[Evaluation Order]]; Recursion with Fixed Point Combinators
 
 (4 Oct) Lecture notes for [[Week4]]; [[Assignment4]].
 
 
 >      Topics: [[Evaluation Order]]; Recursion with Fixed Point Combinators
 
 (4 Oct) Lecture notes for [[Week4]]; [[Assignment4]].
 

->      Topics: More on Fixed Points; Sets; Aborting List Traversals; [[Implementing Trees]] 
+>      Topics: More on Fixed Points; Sets; Aborting List Traversals; [[Implementing Trees]]

 
 
 (18 Oct, 25 Oct) Lecture notes for [[Week5]] and [[Week6]]; [[Assignment5]].
 
 
 
 (18 Oct, 25 Oct) Lecture notes for [[Week5]] and [[Week6]]; [[Assignment5]].
 

->      Topics: Types, Polymorphism, Dividing by Zero
+>      Topics: Types, Polymorphism, Unit and Bottom, Dividing by Zero/[[Towards Monads]]

 
 (1 Nov) Lecture notes for Week7; Assignment6.
 
 
 (1 Nov) Lecture notes for Week7; Assignment6.
 

diff --git a/towards_monads.mdwn b/towards_monads.mdwn
new file mode 100644 (file)
index 0000000..223c592
--- /dev/null
+++ b/towards_monads.mdwn
@@ -0,0 +1,142 @@
+Dividing by zero
+----------------
+
+Integer division operation presupposes that its second argument
+(the divisor) is not zero, upon pain of presupposition failure.
+Here's what my OCaml interpreter says:
+
+    # 12/0;;
+    Exception: Division_by_zero.
+
+So we want to explicitly allow for the possibility that
+division will return something other than a number.
+We'll use OCaml's option type, which works like this:
+
+    # type 'a option = None | Some of 'a;;
+    # None;;
+    - : 'a option = None
+    # Some 3;;
+    - : int option = Some 3
+
+So if a division is normal, we return some number, but if the divisor is
+zero, we return None. As a mnemonic aid, we'll append a `'` to the end of our new divide function.
+
+<pre>
+let div' (x:int) (y:int) =
+  match y with 0 -> None |
+               _ -> Some (x / y);;
+
+(*
+val div' : int -> int -> int option = fun
+# div' 12 3;;
+- : int option = Some 4
+# div' 12 0;;
+- : int option = None
+# div' (div' 12 3) 2;;
+Characters 4-14:
+  div' (div' 12 3) 2;;
+      ^^^^^^^^^^
+Error: This expression has type int option
+       but an expression was expected of type int
+*)
+</pre>
+
+This starts off well: dividing 12 by 3, no problem; dividing 12 by 0,
+just the behavior we were hoping for.  But we want to be able to use
+the output of the safe-division function as input for further division
+operations.  So we have to jack up the types of the inputs:
+
+<pre>
+let div' (x:int option) (y:int option) =
+  match y with None -> None |
+               Some 0 -> None |
+               Some n -> (match x with None -> None |
+                                       Some m -> Some (m / n));;
+
+(*
+val div' : int option -> int option -> int option = <fun>
+# div' (Some 12) (Some 4);;
+- : int option = Some 3
+# div' (Some 12) (Some 0);;
+- : int option = None
+# div' (div' (Some 12) (Some 0)) (Some 4);;
+- : int option = None
+*)
+</pre>
+
+Beautiful, just what we need: now we can try to divide by anything we
+want, without fear that we're going to trigger any system errors.
+
+I prefer to line up the `match` alternatives by using OCaml's
+built-in tuple type:
+
+<pre>
+let div' (x:int option) (y:int option) =
+  match (x, y) with (None, _) -> None |
+                    (_, None) -> None |
+                    (_, Some 0) -> None |
+                    (Some m, Some n) -> Some (m / n);;
+</pre>
+
+So far so good.  But what if we want to combine division with
+other arithmetic operations?  We need to make those other operations
+aware of the possibility that one of their arguments will trigger a
+presupposition failure:
+
+<pre>
+let add' (x:int option) (y:int option) =
+  match (x, y) with (None, _) -> None |
+                    (_, None) -> None |
+                    (Some m, Some n) -> Some (m + n);;
+
+(*
+val add' : int option -> int option -> int option = <fun>
+# add' (Some 12) (Some 4);;
+- : int option = Some 16
+# add' (div' (Some 12) (Some 0)) (Some 4);;
+- : int option = None
+*)
+</pre>
+
+This works, but is somewhat disappointing: the `add'` operation
+doesn't trigger any presupposition of its own, so it is a shame that
+it needs to be adjusted because someone else might make trouble.
+
+But we can automate the adjustment.  The standard way in OCaml,
+Haskell, etc., is to define a `bind` operator (the name `bind` is not
+well chosen to resonate with linguists, but what can you do). To continue our mnemonic association, we'll put a `'` after the name "bind" as well.
+
+<pre>
+let bind' (x: int option) (f: int -> (int option)) =
+  match x with None -> None |
+               Some n -> f n;;
+
+let add' (x: int option) (y: int option)  =
+  bind' x (fun x -> bind' y (fun y -> Some (x + y)));;
+
+let div' (x: int option) (y: int option) =
+  bind' x (fun x -> bind' y (fun y -> if (0 = y) then None else Some (x / y)));;
+
+(*
+#  div' (div' (Some 12) (Some 2)) (Some 4);;
+- : int option = Some 1
+#  div' (div' (Some 12) (Some 0)) (Some 4);;
+- : int option = None
+# add' (div' (Some 12) (Some 0)) (Some 4);;
+- : int option = None
+*)
+</pre>
+
+Compare the new definitions of `add'` and `div'` closely: the definition
+for `add'` shows what it looks like to equip an ordinary operation to
+survive in dangerous presupposition-filled world.  Note that the new
+definition of `add'` does not need to test whether its arguments are
+None objects or real numbers---those details are hidden inside of the
+`bind'` function.
+
+The definition of `div'` shows exactly what extra needs to be said in
+order to trigger the no-division-by-zero presupposition.
+
+For linguists: this is a complete theory of a particularly simply form
+of presupposition projection (every predicate is a hole).
+

diff --git a/week6.mdwn b/week6.mdwn
index 1614972..e244af7 100644 (file)
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -265,145 +265,8 @@ whether an expression that would diverge if we tried to fully evaluate it does
 diverge. As we consider richer languages, thunks will become more useful.
 
 
 diverge. As we consider richer languages, thunks will become more useful.
 
 

+Towards Monads
+--------------
+
+This has now been moved to [its own page](/towards_monads).

 
 

-Dividing by zero: Towards Monads
---------------------------------
-
-So the integer division operation presupposes that its second argument
-(the divisor) is not zero, upon pain of presupposition failure.
-Here's what my OCaml interpreter says:
-
-    # 12/0;;
-    Exception: Division_by_zero.
-
-So we want to explicitly allow for the possibility that
-division will return something other than a number.
-We'll use OCaml's option type, which works like this:
-
-    # type 'a option = None | Some of 'a;;
-    # None;;
-    - : 'a option = None
-    # Some 3;;
-    - : int option = Some 3
-
-So if a division is normal, we return some number, but if the divisor is
-zero, we return None. As a mnemonic aid, we'll append a `'` to the end of our new divide function.
-
-<pre>
-let div' (x:int) (y:int) =
-  match y with 0 -> None |
-               _ -> Some (x / y);;
-
-(*
-val div' : int -> int -> int option = fun
-# div' 12 3;;
-- : int option = Some 4
-# div' 12 0;;
-- : int option = None
-# div' (div' 12 3) 2;;
-Characters 4-14:
-  div' (div' 12 3) 2;;
-      ^^^^^^^^^^
-Error: This expression has type int option
-       but an expression was expected of type int
-*)
-</pre>
-
-This starts off well: dividing 12 by 3, no problem; dividing 12 by 0,
-just the behavior we were hoping for.  But we want to be able to use
-the output of the safe-division function as input for further division
-operations.  So we have to jack up the types of the inputs:
-
-<pre>
-let div' (x:int option) (y:int option) =
-  match y with None -> None |
-               Some 0 -> None |
-               Some n -> (match x with None -> None |
-                                       Some m -> Some (m / n));;
-
-(*
-val div' : int option -> int option -> int option = <fun>
-# div' (Some 12) (Some 4);;
-- : int option = Some 3
-# div' (Some 12) (Some 0);;
-- : int option = None
-# div' (div' (Some 12) (Some 0)) (Some 4);;
-- : int option = None
-*)
-</pre>
-
-Beautiful, just what we need: now we can try to divide by anything we
-want, without fear that we're going to trigger any system errors.
-
-I prefer to line up the `match` alternatives by using OCaml's
-built-in tuple type:
-
-<pre>
-let div' (x:int option) (y:int option) =
-  match (x, y) with (None, _) -> None |
-                    (_, None) -> None |
-                    (_, Some 0) -> None |
-                    (Some m, Some n) -> Some (m / n);;
-</pre>
-
-So far so good.  But what if we want to combine division with
-other arithmetic operations?  We need to make those other operations
-aware of the possibility that one of their arguments will trigger a
-presupposition failure:
-
-<pre>
-let add' (x:int option) (y:int option) =
-  match (x, y) with (None, _) -> None |
-                    (_, None) -> None |
-                    (Some m, Some n) -> Some (m + n);;
-
-(*
-val add' : int option -> int option -> int option = <fun>
-# add' (Some 12) (Some 4);;
-- : int option = Some 16
-# add' (div' (Some 12) (Some 0)) (Some 4);;
-- : int option = None
-*)
-</pre>
-
-This works, but is somewhat disappointing: the `add'` operation
-doesn't trigger any presupposition of its own, so it is a shame that
-it needs to be adjusted because someone else might make trouble.
-
-But we can automate the adjustment.  The standard way in OCaml,
-Haskell, etc., is to define a `bind` operator (the name `bind` is not
-well chosen to resonate with linguists, but what can you do). To continue our mnemonic association, we'll put a `'` after the name "bind" as well.
-
-<pre>
-let bind' (x: int option) (f: int -> (int option)) =
-  match x with None -> None |
-               Some n -> f n;;
-
-let add' (x: int option) (y: int option)  =
-  bind' x (fun x -> bind' y (fun y -> Some (x + y)));;
-
-let div' (x: int option) (y: int option) =
-  bind' x (fun x -> bind' y (fun y -> if (0 = y) then None else Some (x / y)));;
-
-(*
-#  div' (div' (Some 12) (Some 2)) (Some 4);;
-- : int option = Some 1
-#  div' (div' (Some 12) (Some 0)) (Some 4);;
-- : int option = None
-# add' (div' (Some 12) (Some 0)) (Some 4);;
-- : int option = None
-*)
-</pre>
-
-Compare the new definitions of `add'` and `div'` closely: the definition
-for `add'` shows what it looks like to equip an ordinary operation to
-survive in dangerous presupposition-filled world.  Note that the new
-definition of `add'` does not need to test whether its arguments are
-None objects or real numbers---those details are hidden inside of the
-`bind'` function.
-
-The definition of `div'` shows exactly what extra needs to be said in
-order to trigger the no-division-by-zero presupposition.
-
-For linguists: this is a complete theory of a particularly simply form
-of presupposition projection (every predicate is a hole).

diff --git a/week7.mdwn b/week7.mdwn
index 19cc224..9a88221 100644 (file)
--- a/week7.mdwn
+++ b/week7.mdwn
@@ -1,10 +1,11 @@
 [[!toc]]
 
 [[!toc]]
 

+

 Monads
 ------
 
 Start by (re)reading the discussion of monads in the lecture notes for
 Monads
 ------
 
 Start by (re)reading the discussion of monads in the lecture notes for

-week 6 [Towards Monads](http://lambda.jimpryor.net//week6/#index4h2).
+week 6 [[Towards Monads]].

 In those notes, we saw a way to separate thinking about error
 conditions (such as trying to divide by zero) from thinking about
 normal arithmetic computations.  We did this by making use of the
 In those notes, we saw a way to separate thinking about error
 conditions (such as trying to divide by zero) from thinking about
 normal arithmetic computations.  We did this by making use of the