| < Free Open Study > |
|
This chapter introduces the most elementary member of the family of typed languages that we shall be studying for the rest of the book: the simply typed lambda-calculus of Church (1940) and Curry (1958).
In Chapter 8, we introduced a simple static type system for arithmetic expressions with two types: Bool, classifying terms whose evaluation yields a boolean, and Nat, classifying terms whose evaluation yields a number. The "ill-typed" terms not belonging to either of these types include all the terms that reach stuck states during evaluation (e.g., if 0 then 1 else 2) as well as some terms that actually behave fine during evaluation, but for which our static classification is too conservative (like if true then 0 else false).
Suppose we want to construct a similar type system for a language combining booleans (for the sake of brevity, we'll ignore numbers in this chapter) with the primitives of the pure lambda-calculus. That is, we want to introduce typing rules for variables, abstractions, and applications that (a) maintain type safety—i.e., satisfy the type preservation and progress theorems, 8.3.2 and 8.3.3—and (b) are not too conservative—i.e., they should assign types to most of the programs we actually care about writing.
Of course, since the pure lambda-calculus is Turing complete, there is no hope of giving an exact type analysis for these primitives. For example, there is no way of reliably determining whether a program like
if <long and tricky computation> then true else (λx.x)
yields a boolean or a function without actually running the long and tricky computation and seeing whether it yields true or false. But, in general, the [1] long and tricky computation might even diverge, and any typechecker that tries to predict its outcome precisely will then diverge as well.
Figure 9-1: Pure Simply Typed Lambda-Calculus (λ→)
To extend the type system for booleans to include functions, we clearly need to add a type classifying terms whose evaluation results in a function. As a first approximation, let's call this type →. If we add a typing rule
λx.t :→
giving every λ-abstraction the type →, we can classify both simple terms like λx.x and compound terms like if true then (λx.true) else (λx.λy.y) as yielding functions.
But this rough analysis is clearly too conservative: functions like λx.true and λx.λy.y are lumped together in the same type →, ignoring the fact that applying the first to true yields a boolean, while applying the second to true yields another function. In general, in order to give a useful type to the result of an application, we need to know more about the left-hand side than just that it is a function: we need to know what type the function returns. Moreover, in order to be sure that the function will behave correctly when it is called, we need to keep track of what type of arguments it expects. To keep track of this information, we replace the bare type → by an infinite family of types of the form T1→T2, each classifying functions that expect arguments of type T1 and return results of type T2.
The set of simple types over the type Bool is generated by the following grammar:
T ::= Bool T→T | types: type of booleans type of functions |
The type constructor → is right-associative—that is, the expression T1→T2→ T3 stands for T1→(T2→T3).
For example Bool→Bool is the type of functions mapping boolean arguments to boolean results. (Bool→Bool)→(Bool→Bool)—or, equivalently, (Bool→Bool)→Bool→Bool—is the type of functions that take boolean-to-boolean functions as arguments and return them as results.
[1]The system studied in this chapter is the simply typed lambda-calculus (Figure 9-1) with booleans (8-1). The associated OCaml implementation is fullsimple.
| < Free Open Study > |
|