edits

[lambda.git] / week6.mdwn

diff --git a/week6.mdwn b/week6.mdwn
index f26285f..7a5ae2c 100644 (file)
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -1,16 +1,16 @@
 [[!toc]]
 
 [[!toc]]
 

-Types, OCAML
+Types, OCaml

 ------------
 
 ------------
 

-OCAML has type inference: the system can often infer what the type of
+OCaml has type inference: the system can often infer what the type of

 an expression must be, based on the type of other known expressions.
 
 an expression must be, based on the type of other known expressions.
 

-For instance, if we type 
+For instance, if we type

 
     # let f x = x + 3;;
 
 
     # let f x = x + 3;;
 

-The system replies with 
+The system replies with

 
     val f : int -> int = <fun>
 
 
     val f : int -> int = <fun>
 


@@ -32,7 +32,7 @@ element:
     # (3) = 3;;
     - : bool = true
 
     # (3) = 3;;
     - : bool = true
 

-though OCAML, like many systems, refuses to try to prove whether two
+though OCaml, like many systems, refuses to try to prove whether two

 functional objects may be identical:
 
     # (f) = f;;
 functional objects may be identical:
 
     # (f) = f;;


@@ -41,11 +41,11 @@ functional objects may be identical:
 Oh well.
 
 
 Oh well.
 
 

-Booleans in OCAML, and simple pattern matching
+Booleans in OCaml, and simple pattern matching

 ----------------------------------------------
 
 Where we would write `true 1 2` in our pure lambda calculus and expect
 ----------------------------------------------
 
 Where we would write `true 1 2` in our pure lambda calculus and expect

-it to evaluate to `1`, in OCAML boolean types are not functions
+it to evaluate to `1`, in OCaml boolean types are not functions

 (equivalently, are functions that take zero arguments).  Selection is
 accomplished as follows:
 
 (equivalently, are functions that take zero arguments).  Selection is
 accomplished as follows:
 


@@ -65,7 +65,7 @@ That is,
     # match true with true -> 1 | false -> 2;;
     - : int = 1
 
     # match true with true -> 1 | false -> 2;;
     - : int = 1
 

-Compare with 
+Compare with

 
     # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
     - : int = 9
 
     # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
     - : int = 9


@@ -73,7 +73,7 @@ Compare with
 Unit and thunks
 ---------------
 
 Unit and thunks
 ---------------
 

-All functions in OCAML take exactly one argument.  Even this one:
+All functions in OCaml take exactly one argument.  Even this one:

 
     # let f x y = x + y;;
     # f 2 3;;
 
     # let f x y = x + y;;
     # f 2 3;;


@@ -87,7 +87,7 @@ Here's how to tell that `f` has been curry'd:
 After we've given our `f` one argument, it returns a function that is
 still waiting for another argument.
 
 After we've given our `f` one argument, it returns a function that is
 still waiting for another argument.
 

-There is a special type in OCAML called `unit`.  There is exactly one
+There is a special type in OCaml called `unit`.  There is exactly one

 object in this type, written `()`.  So
 
     # ();;
 object in this type, written `()`.  So
 
     # ();;


@@ -112,7 +112,7 @@ correct type is the unit:
 
 Let's have some fn: think of `rec` as our `Y` combinator.  Then
 
 
 Let's have some fn: think of `rec` as our `Y` combinator.  Then
 

-    # let rec f n = if (0 = n) then 1 else (n * (f (n - 1)));; 
+    # let rec f n = if (0 = n) then 1 else (n * (f (n - 1)));;

     val f : int -> int = <fun>
     # f 5;;
     - : int = 120
     val f : int -> int = <fun>
     # f 5;;
     - : int = 120


@@ -145,7 +145,7 @@ So we can try our usual tricks:
     # (fun x -> true) omega;;
     - : bool = true
 
     # (fun x -> true) omega;;
     - : bool = true
 

-OCAML declined to try to evaluate the argument before applying the
+OCaml declined to try to evaluate the argument before applying the

 functor.  But remember that `omega` is a function too, so we can
 reverse the order of the arguments:
 
 functor.  But remember that `omega` is a function too, so we can
 reverse the order of the arguments:
 


@@ -171,145 +171,144 @@ We can use functions that take arguments of type unit to control
 execution.  In Scheme parlance, functions on the unit type are called
 *thunks* (which I've always assumed was a blend of "think" and "chunk").
 
 execution.  In Scheme parlance, functions on the unit type are called
 *thunks* (which I've always assumed was a blend of "think" and "chunk").
 

-Curry-Howard, take 1
---------------------
+Towards Monads
+--------------

 
 

-We will return to the Curry-Howard correspondence a number of times
-during this course.  It expresses a deep connection between logic,
-types, and computation.  Today we'll discuss how the simply-typed
-lambda calculus corresponds to intuitionistic logic.  This naturally
-give rise to the question of what sort of computation classical logic
-corresponds to---as we'll see later, the answer involves continuations.
+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:

 
 

-So at this point we have the simply-typed lambda calculus: a set of
-ground types, a set of functional types, and some typing rules, given
-roughly as follows:
+    # 12/0;;
+    Exception: Division_by_zero.

 
 

-If a variable `x` has type &sigma; and term `M` has type &tau;, then 
-the abstract `\xM` has type &sigma; `-->` &tau;.
+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:

 
 

-If a term `M` has type &sigma; `-->` &tau;, and a term `N` has type
-&sigma;, then the application `MN` has type &tau;.
+    # type 'a option = None | Some of 'a;;
+    # None;;
+    - : 'a option = None
+    # Some 3;;
+    - : int option = Some 3

 
 

-These rules are clearly obverses of one another: the functional types
-that abstract builds up are taken apart by application.
-
-The next step in making sense out of the Curry-Howard corresponence is
-to present a logic.  It will be a part of intuitionistic logic.  We'll
-start with the implicational fragment (that is, the part of
-intuitionistic logic that only involves axioms and implications):
+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>
 
 <pre>

-Axiom: ---------
-        A |- A
-
-Structural Rules:
-
-          &Gamma;, A, B, &Delta; |- C
-Exchange: ---------------------------
-          &Gamma;, B, A, &Delta; |- C
-
-             &Gamma;, A, A |- B
-Contraction: -------------------
-             &Gamma;, A |- B
-
-           &Gamma; |- B
-Weakening: -----------------
-           &Gamma;, A |- B 
-
-Logical Rules:
-
-         &Gamma;, A |- B
---> I:   -------------------
-         &Gamma; |- A --> B  
-
-         &Gamma; |- A --> B         &Gamma; |- A
---> E:   -----------------------------------
-         &Gamma; |- B
+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>
 
 </pre>
 

-`A`, `B`, etc. are variables over formulas.  
-&Gamma;, &Delta;, etc. are variables over (possibly empty) sequences
-of formulas.  &Gamma; `|- A` is a sequent, and is interpreted as
-claiming that if each of the formulas in &Gamma; is true, then `A`
-must also be true.
-
-This logic allows derivations of theorems like the following:
+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>
 
 <pre>

--------  Id
-A |- A
----------- Weak
-A, B |- A
-------------- --> I
-A |- B --> A
------------------ --> I
-|- A --> B --> A
+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>
 
 </pre>
 

-Should remind you of simple types.  (What was `A --> B --> A` the type
-of again?)
+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.

 
 

-The easy way to grasp the Curry-Howard correspondence is to *label*
-the proofs.  Since we wish to establish a correspondence between this
-logic and the lambda calculus, the labels will all be terms from the
-simply-typed lambda calculus.  Here are the labeling rules:
+I prefer to line up the `match` alternatives by using OCaml's
+built-in tuple type:

 
 <pre>
 
 <pre>

-Axiom: -----------
-       x:A |- x:A
-
-Structural Rules:
-
-          &Gamma;, x:A, y:B, &Delta; |- R:C
-Exchange: -------------------------------
-          &Gamma;, y:B, x:A, &Delta; |- R:C
-
-             &Gamma;, x:A, x:A |- R:B
-Contraction: --------------------------
-             &Gamma;, x:A |- R:B
-
-           &Gamma; |- R:B
-Weakening: --------------------- 
-           &Gamma;, x:A |- R:B     [x chosen fresh]
-
-Logical Rules:
+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>

 
 

-         &Gamma;, x:A |- R:B
---> I:   -------------------------
-         &Gamma; |- \xM:A --> B  
+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:

 
 

-         &Gamma; |- f:(A --> B)      &Gamma; |- x:A
---> E:   -------------------------------------
-         &Gamma; |- (fx):B
+<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>
 
 </pre>
 

-In these labeling rules, if a sequence &Gamma; in a premise contains
-labeled formulas, those labels remain unchanged in the conclusion.
+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.

 
 

-What is means for a variable `x` to be chosen *fresh* is that
-`x` must be distinct from any other variable in any of the labels
-used in the proof.
-
-Using these labeling rules, we can label the proof
-just given:
+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>
 
 <pre>

-------------  Id
-x:A |- x:A
----------------- Weak
-x:A, y:B |- x:A
-------------------------- --> I
-x:A |- (\y.x):(B --> A)
----------------------------- --> I
-|- (\x y. x):A --> B --> A
+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>
 
 </pre>
 

-We have derived the *K* combinator, and typed it at the same time!
-
-Need a proof that involves application, and a proof with cut that will
-show beta reduction, so "normal" proof.
+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.

 
 

-[To do: add pairs and destructors; unit and negation...]
+The definition of `div'` shows exactly what extra needs to be said in
+order to trigger the no-division-by-zero presupposition.

 
 

-Excercise: construct a proof whose labeling is the combinator S.
+For linguists: this is a complete theory of a particularly simply form
+of presupposition projection (every predicate is a hole).