[[!toc]] Types, OCAML ------------ 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. For instance, if we type # let f x = x + 3;; The system replies with val f : int -> int = Since `+` is only defined on integers, it has type # (+);; - : int -> int -> int = The parentheses are there to turn off the trick that allows the two arguments of `+` to surround it in infix (for linguists, SOV) argument order. That is, # 3 + 4 = (+) 3 4;; - : bool = true In general, tuples with one element are identical to their one element: # (3) = 3;; - : bool = true though OCAML, like many systems, refuses to try to prove whether two functional objects may be identical: # (f) = f;; Exception: Invalid_argument "equal: functional value". Oh well. Booleans in OCAML, and simple pattern matching ---------------------------------------------- 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 (equivalently, are functions that take zero arguments). Selection is accomplished as follows: # if true then 1 else 2;; - : int = 1 The types of the `then` clause and of the `else` clause must be the same. The `if` construction can be re-expressed by means of the following pattern-matching expression: match with true -> | false -> That is, # match true with true -> 1 | false -> 2;; - : int = 1 Compare with # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;; - : int = 9 Unit and thunks --------------- All functions in OCAML take exactly one argument. Even this one: # let f x y = x + y;; # f 2 3;; - : int = 5 Here's how to tell that `f` has been curry'd: # f 2;; - : int -> int = 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 object in this type, written `()`. So # ();; - : unit = () Just as you can define functions that take constants for arguments # let f 2 = 3;; # f 2;; - : int = 3;; you can also define functions that take the unit as its argument, thus # let f () = 3;; val f : unit -> int = Then the only argument you can possibly apply `f` to that is of the correct type is the unit: # f ();; - : int = 3 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)));; val f : int -> int = # f 5;; - : int = 120 We can't define a function that is exactly analogous to our ω. We could try `let rec omega x = x x;;` what happens? However, we can do this: # let rec omega x = omega x;; By the way, what's the type of this function? If you then apply this omega to an argument, # omega 3;; the interpreter goes into an infinite loop, and you have to control-C to break the loop. Oh, one more thing: lambda expressions look like this: # (fun x -> x);; - : 'a -> 'a = # (fun x -> x) true;; - : bool = true (But `(fun x -> x x)` still won't work.) So we can try our usual tricks: # (fun x -> true) omega;; - : bool = true 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: # omega (fun x -> true);; Infinite loop. Now consider the following variations in behavior: # let test = omega omega;; [Infinite loop, need to control c out] # let test () = omega omega;; val test : unit -> 'a = # test;; - : unit -> 'a = # test ();; [Infinite loop, need to control c out] 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"). Curry-Howard, take 1 -------------------- 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 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: If a variable `x` has type σ and term `M` has type τ, then the abstract `\xM` has type σ `-->` τ. If a term `M` has type σ `-->` τ, and a term `N` has type σ, then the application `MN` has type τ. 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):
Axiom: ---------
        A |- A

Structural Rules:

          Γ, A, B, Δ |- C
Exchange: ---------------------------
          Γ, B, A, Δ |- C

             Γ, A, A |- B
Contraction: -------------------
             Γ, A |- B

           Γ |- B
Weakening: -----------------
           Γ, A |- B 

Logical Rules:

         Γ, A |- B
--> I:   -------------------
         Γ |- A --> B  

         Γ |- A --> B         Γ |- A
--> E:   -----------------------------------
         Γ |- B
`A`, `B`, etc. are variables over formulas. Γ, Δ, etc. are variables over (possibly empty) sequences of formulas. Γ `|- A` is a sequent, and is interpreted as claiming that if each of the formulas in Γ is true, then `A` must also be true. This logic allows derivations of theorems like the following:
-------  Id
A |- A
---------- Weak
A, B |- A
------------- --> I
A |- B --> A
----------------- --> I
|- A --> B --> A
Should remind you of simple types. (What was `A --> B --> A` the type of again?) 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:
Axiom: -----------
       x:A |- x:A

Structural Rules:

Exchange: Γ, x:A, y:B, Δ |- R:C
          -------------------------------
          Γ, y:B, x:A, Δ |- R:C

Contraction: Γ, x:A, x:A |- R:B
             --------------------------
             Γ, x:A |- R:B

Weakening: Γ |- R:B
           --------------------- 
           Γ, x:A |- R:B     [x chosen fresh]

Logical Rules:

--> I:   Γ, x:A |- R:B
         -------------------------
         Γ |- \xM:A --> B  

--> E:   Γ |- f:(A --> B)      Γ |- x:A
         -------------------------------------
         Γ |- (fx):B
In these labeling rules, if a sequence Γ in a premise contains labeled formulas, those labels remain unchanged in the conclusion. 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:
------------  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
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. [To do: add pairs and destructors; unit and negation...] Excercise: construct a proof whose labeling is the combinator S.