X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=topics%2F_week5_simply_typed_lambda.mdwn;h=14e21729d3c573984875fcdd4dca223008622f1a;hb=6dc0f03a2b7a5081fa378f0a1af4e37682b7242c;hp=1fedd2a3c9843afd4b0721ba26e7be798c75dac3;hpb=967055fbde4c32649cdf8acf16ac127d43ec3118;p=lambda.git
diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index 1fedd2a3..14e21729 100644
--- a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ -54,11 +54,10 @@ 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
+types](church-simple-types.pdf). In this paper, Church writes 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
@@ -82,16 +81,16 @@ types `T`, the smallest set such that
* ground types, including `e` and `t`, are in `T`
-* for any types σ and τ in `T`, the type σ -->
+* for any types σ and τ in `T`, the type σ ->
τ is in `T`.
For instance, here are some types in `T`:
e
- e --> t
- e --> e --> t
- (e --> t) --> t
- (e --> t) --> e --> t
+ e -> t
+ e -> e -> t
+ (e -> t) -> t
+ (e -> t) -> e -> t
and so on.
@@ -103,28 +102,28 @@ which is the smallest set such that
* each type `t` has an infinite set of distinct variables, {x^t}_1,
{x^t}_2, {x^t}_3, ...
-* If a term `M` has type σ --> τ, and a term `N` has type
+* If a term `M` has type σ -> τ, and a term `N` has type
σ, then the application `(M N)` has type τ.
* If a variable `a` has type σ, and term `M` has type τ,
- then the abstract λ a M
has type σ --> τ.
+ then the abstract λ a M
has type σ -> τ.
The definitions of types and of typed terms should be highly familiar
-to semanticists, except that instead of writing σ --> τ,
+to semanticists, except that instead of writing σ -> τ,
linguists write <σ, τ>. We will use the arrow notation,
since it is more iconic.
Some examples (assume that `x` has type `o`):
x o
- \x.x o --> o
+ \x.x o -> o
((\x.x) x) o
Excercise: write down terms that have the following types:
- o --> o --> o
- (o --> o) --> o --> o
- (o --> o --> o) --> o
+ o -> o -> o
+ (o -> o) -> o -> o
+ (o -> o -> o) -> o
#Associativity of types versus terms#
@@ -132,7 +131,7 @@ 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 `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
+`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
@@ -147,13 +146,13 @@ present it here; see Berendregt or Hankin.
Since Ω does not have a normal form, it follows that Ω
cannot have a type in Λ_T. We can easily see why:
- Ω = (\x.xx)(\x.xx)
+Ω = (\x.xx)(\x.xx)
Assume Ω has type τ, and `\x.xx` has type σ. Then
because `\x.xx` takes an argument of type σ and returns
-something of type τ, `\x.xx` must also have type σ -->
+something of type τ, `\x.xx` must also have type σ ->
τ. By repeating this reasoning, `\x.xx` must also have type
-(σ --> τ) --> τ; and so on. Since variables have
+(σ -> τ) -> τ; and so on. Since variables have
finite types, there is no way to choose a type for the variable `x`
that can satisfy all of the requirements imposed on it.
@@ -161,51 +160,107 @@ In general, there is no way for a function to have a type that can
take itself for an argument. It follows that there is no way to
define the identity function in such a way that it can take itself as
an argument. Instead, there must be many different identity
-functions, one for each type.
+functions, one for each type. Some of those types can be functions,
+and some of those functions can be (type-restricted) identity
+functions; but a simply-types identity function can never apply to itself.
#Typing numerals#
-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 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 (σ --> σ) -->
-σ --> σ.
-
-
-
-
-
-
+The Church numerals are well behaved with respect to types.
+To see this, consider the first three Church numerals (starting with zero):
+
+ \s z . z
+ \s z . s z
+ \s z . s (s z)
+
+Given the internal structure of the term we are using to represent
+zero, its type must have the form ρ -> σ -> σ for
+some ρ and σ. This type is consistent with term for one,
+but the structure of the definition of one is more restrictive:
+because the first argument (`s`) must apply to the second argument
+(`z`), the type of the first argument must describe a function from
+expressions of type σ to some result type. So we can refine
+ρ by replacing it with the more specific type σ -> τ.
+At this point, the overall type is (σ -> τ) -> σ ->
+σ. Note that this refined type remains compatible with the
+definition of zero. Finally, by examinining the definition of two, we
+see that expressions of type τ must be suitable to serve as
+arguments to functions of type σ -> τ, since the result of
+applying `s` to `z` serves as the argument of `s`. The most general
+way for that to be true is if τ ≡ σ. So at this
+point, we have the overall type of (σ -> σ) -> σ
+-> σ.
+
+
+
+## Predecessor and lists are not representable in simply typed lambda-calculus ##
+
+As Oleg Kiselyov points out, [[predecessor and lists can't be
+represented in the simply-typed lambda
+calculus|http://okmij.org/ftp/Computation/lambda-calc.html#predecessor]].
+This is not because there is any difficulty typing what the functions
+involved do "from the outside": for instance, the predecessor function
+is a function from numbers to numbers, or τ -> τ, where τ
+is our type for Church numbers (i.e., (σ -> σ) -> σ
+-> σ). (Though this type will only be correct if we decide that
+the predecessor of zero should be a number, perhaps zero.)
+
+Rather, the problem is that the definition of the function requires
+subterms that can't be simply-typed. We'll illustrate with our
+implementation of the predecessor, sightly modified in inessential
+ways to suit present purposes:
+
+ let zero = \s z. z in
+ let snd = \a b. b in
+ let pair = \a b. \v. v a b in
+ let succ = \n s z. s (n s z) in
+ let collect = \p. p (\a b. pair (succ a) a)
+ let pred = \n. n collect (pair zero zero) snd in
+
+Let's see how far we can get typing these terms. `zero` is the Church
+encoding of zero. Using `N` as the type for Church numbers (i.e.,
+N ≡ (σ -> σ) -> σ -> σ
for some
+σ, `zero` has type `N`. `snd` takes two numbers, and returns
+the second, so `snd` has type `N -> N -> N`. Then the type of `pair`
+is `N -> N -> (type(snd)) -> N`, that is, `N -> N -> (N -> N -> N) ->
+N`. Likewise, `succ` has type `N -> N`, and `collect` has type `pair
+-> pair`, where `pair` is the type of an ordered pair of numbers,
+namely, pair ≡ (N -> N -> N) -> N
. So far so good.
+
+The problem is the way in which `pred` puts these parts together. In
+particular, `pred` applies its argument, the number `n`, to the
+`collect` function. Since `n` is a number, its type is (σ
+-> σ) -> σ -> σ
. This means that the type of
+`collect` has to match σ -> σ
. But we
+concluded above that the type of `collect` also had to be `pair ->
+pair`. Putting these constraints together, it appears that
+σ
must be the type of a pair of numbers. But we
+already decided that the type of a pair of numbers is `(N -> N -> N)
+-> N`. Here's the difficulty: `N` is shorthand for a type involving
+σ
. If σ
turns out to depend on
+`N`, and `N` depends in turn on σ
, then
+σ
is a proper subtype of itself, which is not
+allowed in the simply-typed lambda calculus.
+
+The way we got here is that the `pred` function relies on the built-in
+right-fold structure of the Church numbers to recursively walk down
+the spine of its argument. In order to do that, the argument had to
+apply to the `collect` operation. And since `collect` had to be the
+sort of operation that manipulates numbers, the infinite regress is
+established.
+
+Now, of course, this is only one of myriad possible implementations of
+the predecessor function in the lambda calculus. Could one of them
+possibly be simply-typeable? It turns out that this can't be done.
+See the works cited by Oleg for details.
+
+Because lists are (in effect) a generalization of the Church numbers,
+computing the tail of a list is likewise beyond the reach of the
+simply-typed lambda calculus.
+
+This result is surprising. It illustrates how recursion is built into
+the structure of the Church numbers (and lists). Most importantly for
+the discussion of the simply-typed lambda calculus, it demonstrates
+that even fairly basic recursive computations are beyond the reach of
+a simply-typed system.