Typed λ-calculi with one binder

Abstract

Type theory was invented at the beginning of the twentieth century with the aim of avoiding the paradoxes which result from the self-application of functions. λ-calculus was developed in the early 1930s as a theory of functions. In 1940, Church added type theory to his λ-calculus giving us the influential simply typed λ-calculus where types were simple and never created by binders (or abstractors). However, realising the limitations of the simply typed λ-calculus, in the second half of the twentieth century we saw the birth of new more powerful typed λ-calculi where types are indeed created by abstraction. Most of these calculi use two binders λ and ∏ to distinguish between functions (created by λ-abstraction) and types (created by ∏-abstraction). Moreover, these calculi allow β-reduction but not ∏-reduction. That is, (πx·A. B)C →B[x := C] is only allowed when π is λ but not when it is ∏. This means that, modern systems do not allow types to have the same instantiation right as functions. In particular, when b has type B, the type of (λx:A.b)C is taken immediately to be B[x := C] instead of (Hx·A.B)C. Extensions of modern type systems with both Fl-reduction and type instantiation have appeared in (Kamareddine, Bloo and Nederpelt, 1999; Kamareddine and Nederpelt, 1996; Peyton-Jones and Meijer, 1997). This makes the λ and ∏ very similar and hence leads to the obvious question: why not use a unique binder instead of the λ and ∏? This makes more sense since already, versions of de Bruijn's Automath unified λ and ∏ giving more elegant systems. This paper studies the main properties of type systems with unified λ and ∏. © 2005 Cambridge University Press.