Typed lambda calculus
|
|
A typed lambda calculus is a typed formalism which uses the lambda-symbol (<math>\lambda<math>) to denote anonymous function abstraction. Typed lambda calculi are foundational programming languages and are the base of typed functional programming languages such as ML and Haskell, they are closely related to intuitionistic logic via the Curry-Howard isomorphism and they can be considered as the internal language of classes of categories, e.g. the simply typed lambda calculus is the language of Cartesian Closed Categories (CCCs).
Traditionally, typed lambda calculi were seen as refinements of the untyped lambda calculus. A more modern view is to consider typed lambda calculi as fundamental and to consider the untyped lambda calculus as a special case of a typed lambda calculus with only one type.
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 <math>\sigma\to\tau<math>. System T extends the simply typed lambda calculus by a type of natural numbers and higher order primitive recursion, in this system all functions provable recursive in Peano Arithmetic are definable. System F allows to represent polymorphism by using universal quantification over all types, from a logical perspective it allows to represent functions which are provable total in higher 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, 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 <math>A<math> is a subtype of <math>B<math>, then all terms of type <math>A<math> also have type <math>B<math>. Typed lambda calculi with subtyping are the simply typed lambda calculus with conjunctive types and <math>F^\leq<math> (F-sub).
All the systems mentioned so far, with the exception of the untyped lambda calculus, are strongly normalizing; that is all computations terminate and as a consequence they are consistent as a logic, i.e. there are uninhabited types. However, there are typed lambda calculi which are not strongly normalizing, e.g. the dependently typed lambda calulus 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, like Plotkin's PCF, are not normalizing, but they are not intended to be interpreted as a logic. Indeed, PCF is a prototypical, typed functional programming language, where types are used to ensure that programs are well-behaved but not necessarily terminating. Indeed, typed lambda calculi play an important role in the design of new type systems for programming languages, here typability usually capture desirable properties of the program, e.g. the program will not cause a memory access violation.