Typed λ-calculi with one binder

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)

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, (px·A. B)C ?B[x := C] is only allowed when p 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.

Original languageEnglish
Pages (from-to)771-796
Number of pages26
JournalJournal of Functional Programming
Volume15
Issue number5
DOIs
Publication statusPublished - Sept 2005

Fingerprint

Dive into the research topics of 'Typed λ-calculi with one binder'. Together they form a unique fingerprint.

Cite this