From: Jim Pryor Date: Mon, 1 Nov 2010 04:14:33 +0000 (-0400) Subject: move Towards Monads to own page X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=93d67277339f0aed8184a14bbc35ec5060a0c031;ds=sidebyside move Towards Monads to own page Signed-off-by: Jim Pryor --- diff --git a/assignment5.mdwn b/assignment5.mdwn index fee1d833..b1f65d2a 100644 --- 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. -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) @@ -233,20 +233,20 @@ any auxiliary functions you need. 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) -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'`: - 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 902bb2ee..fd607e69 100644 --- 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 -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: 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]]. -> Topics: Types, Polymorphism, Dividing by Zero +> Topics: Types, Polymorphism, Unit and Bottom, Dividing by Zero/[[Towards Monads]] (1 Nov) Lecture notes for Week7; Assignment6. diff --git a/towards_monads.mdwn b/towards_monads.mdwn new file mode 100644 index 00000000..223c592b --- /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. + +
+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
+*)
+
+ +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: + +
+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 = 
+# 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
+*)
+
+ +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: + +
+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);;
+
+ +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: + +
+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 = 
+# add' (Some 12) (Some 4);;
+- : int option = Some 16
+# add' (div' (Some 12) (Some 0)) (Some 4);;
+- : int option = None
+*)
+
+ +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. + +
+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
+*)
+
+ +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 16149724..e244af75 100644 --- 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. +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. - -
-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
-*)
-
- -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: - -
-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 = 
-# 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
-*)
-
- -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: - -
-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);;
-
- -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: - -
-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 = 
-# add' (Some 12) (Some 4);;
-- : int option = Some 16
-# add' (div' (Some 12) (Some 0)) (Some 4);;
-- : int option = None
-*)
-
- -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. - -
-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
-*)
-
- -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 19cc2248..9a882217 100644 --- a/week7.mdwn +++ b/week7.mdwn @@ -1,10 +1,11 @@ [[!toc]] + 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