Typed lambda-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. $\lambda$ -calculus was developed in the early 1930s as a theory of functions. In 1940, Church added type theory to his $\lambda$ -calculus giving us the influential simply typed $\lambda$ -calculus where types were simple and never created by binders (or abstractors). However, realising the limitations of the simply typed $\lambda$ -calculus, in the second half of the twentieth century we saw the birth of new more powerful typed $\lambda$ -calculi where types are indeed created by abstraction. Most of these calculi use two binders $\lambda$ and $\Pi$ to distinguish between functions (created by $\lambda$ -abstraction) and types (created by $\Pi$ -abstraction). Moreover, these calculi allow $\beta$ -reduction but not $\Pi$ -reduction. That is, $(\pi_{x:A}.B)C \rightarrow B[x:=C]$ is only allowed when $\pi$ is $\lambda$ but not when it is $\Pi$ . 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 $(\lambda_{x:A}.b)C$ is taken immediately to be $B[x:=C]$ instead of $(\Pi_{x:A}.B)C$ . Extensions of modern type systems with both $\Pi$ -reduction and type instantiation have appeared in (Kamareddine, Bloo and Nederpelt, 1999; Kamareddine and Nederpelt, 1996; Peyton-Jones and Meijer, 1997). This makes the $\lambda$ and $\Pi$ very similar and hence leads to the obvious question: why not use a unique binder instead of the $\lambda$ and $\Pi$ ? This makes more sense since already, versions of de Bruijn's Automath unified $\lambda$ and $\Pi$ giving more elegant systems. This paper studies the main properties of type systems with unified $\lambda$ and $\Pi$ .