--- /dev/null
+Types and OCAML
+
+1. Which of the following expressions is well-typed in OCAML?
+ For those that are, give the type of the expression as a whole.
+ For those that are not, why not?
+
+ let rec f x = f x;;
+
+ let rec f x = f f;;
+
+ let rec f x = f x in f f;;
+
+ let rec f x = f x in f ();;
+
+ let rec f () = f f;;
+
+ let rec f () = f ();;
+
+ let rec f () = f () in f f;;
+
+ let rec f () = f () in f ();;
+
+2. Throughout this problem, assume that we have
+
+ let rec omega x = omega x;;
+
+ All of the following are well-typed.
+ Which ones terminate? What are the generalizations?
+
+ omega;;
+
+ omega ();;
+
+ fun () -> omega ();;
+
+ (fun () -> omega ()) ();;
+
+ if true then omega else omega;;
+
+ if false then omega else omega;;
+
+ if true then omega else omega ();;
+
+ if false then omega else omega ();;
+
+ if true then omega () else omega;;
+
+ if false then omega () else omega;;
+
+ if true then omega () else omega ();;
+
+ if false then omega () else omega ();;
+
+ let _ = omega in 2;;
+
+ let _ = omega () in 2;;
+
+3. The following expression is an attempt to make explicit the
+behavior of `if`-`then`-`else` explored in the previous question.
+The idea is to define an `if`-`then`-`else` expression using
+other expression types. So assume that "yes" is any OCAML expression,
+and "no" is any other OCAML expression (of the same type as "yes"!),
+and that "bool" is any boolean. Then we can try the following:
+"if bool then yes else no" should be equivalent to
+
+ let b = bool in
+ let y = yes in
+ let n = no in
+ match b with true -> y | false -> n
+
+This almost works. For instance,
+
+ if true then 1 else 2;;
+
+evaluates to 1, and
+
+ let b = true in let y = 1 in let n = 2 in
+ match b with true -> y | false -> n;;
+
+also evaluates to 1. Likewise,
+
+ if false then 1 else 2;;
+
+and
+
+ let b = false in let y = 1 in let n = 2 in
+ match b with true -> y | false -> n;;
+
+both evaluate to 2.
+
+However,
+
+ let rec omega x = omega x in
+ if true then omega else omega ();;
+
+terminates, but
+
+ let rec omega x = omega x in
+ let b = true in
+ let y = omega in
+ let n = omega () in
+ match b with true -> y | false -> n;;
+
+does not terminate. Incidentally, `match bool with true -> yes |
+false -> no;;` works as desired, but your assignment is to solve it
+without using the magical evaluation order properties of either `if`
+or of `match`. That is, you must keep the `let` statements, though
+you're allowed to adjust what `b`, `y`, and `n` get assigned to.
+
+[[Hint assignment 5 problem 3]]
--- /dev/null
+Use thunks!
+
+[[Hint assignment 5 problem 3 hint]]
--- /dev/null
+What does
+
+ let x = (fun () -> 2) in
+ let y = (fun () -> 3) in
+ match true with true -> x | false -> y;;
+
+evaluate to?
##The simply-typed lambda calculus##
-The untyped lambda calculus is pure computation. It is much more
-common, however, for practical programming languages to be typed.
+The untyped lambda calculus is pure. Pure in many ways: all variables
+and lambdas, with no constants or other special symbols; also, all
+functions without any types. As we'll see eventually, pure also in
+the sense of having no side effects, no mutation, just pure
+computation.
+
+But we live in an impure world. It is much more common for practical
+programming languages to be typed, either implicitly or explicitly.
Likewise, systems used to investigate philosophical or linguistic
issues are almost always typed. Types will help us reason about our
computations. They will also facilitate a connection between logic
and computation.
+From a linguistic perspective, types are generalizations of (parts of)
+programs. To make this comment more concrete: types are to (e.g.,
+lambda) terms as syntactic categories are to expressions of natural
+language. If so, if it makes sense to gather a class of expressions
+together into a set of Nouns, or Verbs, it may also make sense to
+gather classes of terms into a set labelled with some computational type.
+
Soon we will consider polymorphic type systems. First, however, we
-will consider the simply-typed lambda calculus. There's good news and
-bad news: the good news is that the simply-type lambda calculus is
-strongly normalizing: every term has a normal form. We shall see that
-self-application is outlawed, so Ω can't even be written, let
-alone undergo reduction. The bad news is that fixed-point combinators
-are also forbidden, so recursion is neither simple nor direct.
+will consider the simply-typed lambda calculus.
+
+[Pedantic on. Why "simply typed"? Well, the type system is
+particularly simple. As mentioned in class by Koji Mineshima, Church
+tells us that "The simple theory of types was suggested as a
+modification of Russell's ramified theory of types by Leon Chwistek in
+1921 and 1922 and by F. P. Ramsey in 1926." This footnote appears in
+Church's 1940 paper [A formulation of the simple theory of
+types](church-simple-types.pdf). In this paper, as Will Starr
+mentioned in class, Church does indeed write types by simple
+apposition, without the ugly angle brackets and commas used by
+Montague. Furthermore, he omits parentheses under the convention that
+types associated to the *left*---the opposite of the modern
+convention. This is ok, however, because he also reverses the order,
+so that `te` is a function from objects of type `e` to objects of type
+`t`. Cool paper! If you ever want to see Church numerals in their
+native setting--but I'm getting ahead of my story. Pedantic off.]
+
+There's good news and bad news: the good news is that the simply-type
+lambda calculus is strongly normalizing: every term has a normal form.
+We shall see that self-application is outlawed, so Ω can't even
+be written, let alone undergo reduction. The bad news is that
+fixed-point combinators are also forbidden, so recursion is neither
+simple nor direct.
#Types#
-We will have at least one ground type, `o`. From a linguistic point
-of view, think of the ground types as the bar-level 0 categories, that
-is, the lexical types, such as Noun, Verb, Preposition (glossing over
-the internal complexity of those categories in modern theories).
+We will have at least one ground type. For the sake of linguistic
+familiarity, we'll use `e`, the type of individuals, and `t`, the type
+of truth values.
In addition, there will be a recursively-defined class of complex
types `T`, the smallest set such that
-* ground types, including `o`, are in `T`
+* ground types, including `e` and `t`, are in `T`
* for any types σ and τ in `T`, the type σ -->
τ is in `T`.
For instance, here are some types in `T`:
- o
- o --> o
- o --> o --> o
- (o --> o) --> o
- (o --> o) --> o --> o
+ e
+ e --> t
+ e --> e --> t
+ (e --> t) --> t
+ (e --> t) --> e --> t
and so on.
The definitions of types and of typed terms should be highly familiar
to semanticists, except that instead of writing σ --> τ,
-linguists (following Montague, who followed Church) write <σ,
-τ>. We will use the arrow notation, since it is more iconic.
+linguists write <σ, τ>. We will use the arrow notation,
+since it is more iconic.
Some examples (assume that `x` has type `o`):
As we have seen many times, in the lambda calculus, function
application is left associative, so that `f x y z == (((f x) y) z)`.
-Types, *THEREFORE*, are right associative: if `f`, `x`, `y`, and `z`
-have types `a`, `b`, `c`, and `d`, respectively, then `f` has type `a
---> b --> c --> d == (a --> (b --> (c --> d)))`.
+Types, *THEREFORE*, are right associative: if `x`, `y`, and `z`
+have types `a`, `b`, and `c`, respectively, then `f` has type
+`a --> b --> c --> d == (a --> (b --> (c --> d)))`, where `d` is the
+type of the complete term.
It is a serious faux pas to associate to the left for types. You may
as well use your salad fork to stir your tea.
Version 1 type numerals are not a good choice for the simply-typed
lambda calculus. The reason is that each different numberal has a
-different type! For instance, if zero has type σ, then `false`
-has type τ --> τ --> τ, for some τ. Since one is
-represented by the function `\x.x false 0`, one must have type (τ
---> τ --> τ) --> σ --> σ. But this is a different
-type than zero! Because each number has a different type, it becomes
-impossible to write arithmetic operations that can combine zero with
-one. We would need as many different addition operations as we had
-pairs of numbers that we wanted to add.
-
-Fortunately, the Church numberals are well behaved with respect to
+different type! For instance, if zero has type σ, then since
+one is represented by the function `\x.x false 0`, it must have type
+`b --> σ --> σ`, where `b` is the type of a boolean. But
+this is a different type than zero! Because each number has a
+different type, it becomes unbearable to write arithmetic operations
+that can combine zero with one, since we would need as many different
+addition operations as we had pairs of numbers that we wanted to add.
+
+Fortunately, the Church numerals are well behaved with respect to
types. They can all be given the type (σ --> σ) -->
σ --> σ.
--- /dev/null
+[[!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 = <fun>
+
+Since `+` is only defined on integers, it has type
+
+ # (+);;
+ - : int -> int -> int = <fun>
+
+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 <bool expression> with true -> <expression1> | false -> <expression2>
+
+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 = <fun>
+
+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 = <fun>
+
+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 = <fun>
+ # 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>
+ # (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 = <fun>
+
+ # test;;
+ - : unit -> 'a = <fun>
+
+ # 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):
+
+<pre>
+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
+</pre>
+
+`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:
+
+<pre>
+------- Id
+A |- A
+---------- Weak
+A, B |- A
+------------- --> I
+A |- B --> A
+----------------- --> I
+|- A --> B --> A
+</pre>
+
+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:
+
+<pre>
+Axiom: -----------
+ x:A |- x:A
+
+Structural Rules:
+
+ Γ, x:A, y:B, Δ |- R:C
+Exchange: -------------------------------
+ Γ, y:B, x:A, Δ |- R:C
+
+ Γ, x:A, x:A |- R:B
+Contraction: --------------------------
+ Γ, x:A |- R:B
+
+ Γ |- R:B
+Weakening: ---------------------
+ Γ, x:A |- R:B [x chosen fresh]
+
+Logical Rules:
+
+ Γ, x:A |- R:B
+--> I: -------------------------
+ Γ |- \xM:A --> B
+
+ Γ |- f:(A --> B) Γ |- x:A
+--> E: -------------------------------------
+ Γ |- (fx):B
+</pre>
+
+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:
+
+<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
+</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.
+
+[To do: add pairs and destructors; unit and negation...]
+
+Excercise: construct a proof whose labeling is the combinator S.