From da8c71643ef408b942d125d17b6b746bace93ee5 Mon Sep 17 00:00:00 2001 From: Chris Date: Sat, 21 Feb 2015 17:04:58 -0500 Subject: [PATCH] starting lecture on types --- topics/_week5_simply_typed_lambda.mdwn | 188 +++++++++++++++++++++++++++++++++ 1 file changed, 188 insertions(+) create mode 100644 topics/_week5_simply_typed_lambda.mdwn diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn new file mode 100644 index 00000000..cfadf7a0 --- /dev/null +++ b/topics/_week5_simply_typed_lambda.mdwn @@ -0,0 +1,188 @@ +[[!toc]] + +##The simply-typed lambda calculus## + +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. + +[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. 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 `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`: + + e + e --> t + e --> e --> t + (e --> t) --> t + (e --> t) --> e --> t + +and so on. + +#Typed lambda terms# + +Given a set of types `T`, we define the set of typed lambda terms Λ_T, +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 + σ, 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 σ --> τ. + +The definitions of types and of typed terms should be highly familiar +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) x) o + +Excercise: write down terms that have the following types: + + o --> o --> o + (o --> o) --> o --> o + (o --> o --> o) --> o + +#Associativity of types versus terms# + +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 +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. + +#The simply-typed lambda calculus is strongly normalizing# + +If `M` is a term with type τ in Λ_T, then `M` has a +normal form. The proof is not particularly complex, but we will not +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) + +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 σ --> +τ. By repeating this reasoning, `\x.xx` must also have type +(σ --> τ) --> τ; 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. + +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. + +#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 (σ --> σ) --> +σ --> σ. + + + + + + -- 2.11.0