XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week5.mdwn;h=cfadf7a0510c6e842dde993407f2ce9043e9dae4;hp=3eed60e476a7595bb4a71af863a9f23ff750aa97;hb=9efbe94f74c2ea61522fcdb3e3d012fde6034fcd;hpb=9b16c80479fe22202709f0801a961e2aba0562f6;ds=sidebyside
diff git a/week5.mdwn b/week5.mdwn
index 3eed60e4..cfadf7a0 100644
 a/week5.mdwn
+++ b/week5.mdwn
@@ 2,43 +2,73 @@
##The simplytyped 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 simplytyped lambda calculus. There's good news and
bad news: the good news is that the simplytype lambda calculus is
strongly normalizing: every term has a normal form. We shall see that
selfapplication is outlawed, so Ω can't even be written, let
alone undergo reduction. The bad news is that fixedpoint combinators
are also forbidden, so recursion is neither simple nor direct.
+will consider the simplytyped 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](churchsimpletypes.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 settingbut I'm getting ahead of my story. Pedantic off.]
+
+There's good news and bad news: the good news is that the simplytype
+lambda calculus is strongly normalizing: every term has a normal form.
+We shall see that selfapplication is outlawed, so Ω can't even
+be written, let alone undergo reduction. The bad news is that
+fixedpoint 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 barlevel 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 recursivelydefined 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.
@@ 58,8 +88,8 @@ which is the smallest set such that
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`):
@@ 77,9 +107,10 @@ Excercise: write down terms that have the following types:
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.
@@ 113,16 +144,15 @@ functions, one for each type.
Version 1 type numerals are not a good choice for the simplytyped
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 (σ > σ) >
σ > σ.