Chapter 9: Simply Typed Lambda-Calculus

 < 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).

9.1 Function Types

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 safetyi.e., satisfy the type preservation and progress theorems, 8.3.2 and 8.3.3and (b) are not too conservativei.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 T1T2, each classifying functions that expect arguments of type T1 and return results of type T2.

9.1.1 Definition

The set of simple types over the type Bool is generated by the following grammar:

  •  

     T ::=         Bool         TT 

    types:

    type of booleans

    type of functions

The type constructor is right-associativethat is, the expression T1T2 T3 stands for T1(T2T3).

For example BoolBool is the type of functions mapping boolean arguments to boolean results. (BoolBool)(BoolBool)or, equivalently, (BoolBool)BoolBoolis 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 > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net