Typed Lambda Calculus - Kinds of Typed Lambda Calculi

Kinds of Typed Lambda Calculi

Various typed lambda calculi have been studied: The types of the simply typed lambda calculus are only base types (or type variables) and function types . System T extends the simply typed lambda calculus with a type of natural numbers and higher order primitive recursion; in this system all functions provably recursive in Peano arithmetic are definable. System F allows polymorphism by using universal quantification over all types; from a logical perspective it can describe all functions which are provably total in second-order logic. Lambda calculi with dependent types are the base of intuitionistic type theory, the calculus of constructions and the logical framework (LF), a pure lambda calculus with dependent types. Based on work by Berardi on pure type systems, Barendregt proposed the Lambda cube to systematize the relations of pure typed lambda calculi (including simply typed lambda calculus, System F, LF and the calculus of constructions).

Some typed lambda calculi introduce a notion of subtyping, i.e. if is a subtype of, then all terms of type also have type . Typed lambda calculi with subtyping are the simply typed lambda calculus with conjunctive types and System F_<:.

All the systems mentioned so far, with the exception of the untyped lambda calculus, are strongly normalizing: all computations terminate. As a consequence they are consistent as a logic, i.e. there are uninhabited types. There exist, however, typed lambda calculi that are not strongly normalizing. For example the dependently typed lambda calculus with a type of all types (Type : Type) is not normalizing due to Girard's paradox. This system is also the simplest pure type system, a formalism which generalizes the Lambda cube. Systems with explicit recursion combinators, such as Plotkin's PCF, are not normalizing, but they are not intended to be interpreted as a logic. Indeed, PCF (for Programming language for Computable Functions) is a prototypical, typed functional programming language, where types are used to ensure that programs are well-behaved but not necessarily terminating.