Pure type system
Encyclopedia
In the branches of mathematical logic
known as proof theory
and type theory
, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus
that allows an arbitrary number of sorts and dependencies between any of these. The framework can be seen as a generalisation of Barendregt
's lambda cube
, in the sense that all corners of the cube can be represented as instances of a PTS with just two sorts. In fact Barendregt (1991) framed his cube in this setting. Pure type systems may obscure the distinction between types and terms and collapse the type hierarchy, as it is the case of the calculus of constructions
, but this is not generally the case, e.g. the simply typed lambda calculus
allows only terms to depend on types.
Pure type systems were independently introduced by Stefano Berardi (1988) and Jan Terlouw (1989). Intuitionistic
logics were first described as pure type systems by Barendregt. In his PhD thesis, Berardi defined a classical logic cube containing constructive logics akin to the lambda cube (these specifications are non-dependent). A modification of this cube was later called the L-cube by Geuvers, which in his PhD thesis extended the Curry–Howard correspondence to this setting. Based on these ideas, Barthe and others defined classical pure type systems (CPTS) by adding a double negation
operator.
Similarly, in 1998, Tijn Borghuis introduced modal pure type systems (MPTS). Roorda has discussed the application of pure type systems to functional programming; and Roorda and Jeuring have proposed a programming language based on pure type systems.
The systems from the lambda cube are all known to be strongly normalizing. Pure type systems in general need not be, for example U from Girard's paradox is not. (Roughly speaking, Girard
found pure systems in which one can express the sentence "a type is a type".) Furthermore, all pure type systems that are not strongly normalizing are not even (weakly) normalizing: they contain expressions that do not have normal forms, just like the untyped lambda calculus. It is a major open problem in the field whether this is always the case, i.e. whether a (weakly) normalizing PTS always has the strong normalization property. This is known as the Barendregt–Geuvers–Klop conjecture (named after Henk Barendregt, Herman Geuvers, and Jan Willem Klop).
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
known as proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
and type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus
Typed lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
that allows an arbitrary number of sorts and dependencies between any of these. The framework can be seen as a generalisation of Barendregt
Henk Barendregt
Hendrik Pieter Barendregt is a Dutch logician, known for his work in lambda calculus and type theory.Barendregt studied mathematical logic at Utrecht University, obtaining his Masters in 1968 and his Ph.D. in 1971, both cum laude, under Dirk van Dalen and Georg Kreisel...
's lambda cube
Lambda cube
In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions as its diametrically opposite...
, in the sense that all corners of the cube can be represented as instances of a PTS with just two sorts. In fact Barendregt (1991) framed his cube in this setting. Pure type systems may obscure the distinction between types and terms and collapse the type hierarchy, as it is the case of the calculus of constructions
Calculus of constructions
The calculus of constructions is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.-General traits:The CoC is a...
, but this is not generally the case, e.g. the simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a typed lambda calculus...
allows only terms to depend on types.
Pure type systems were independently introduced by Stefano Berardi (1988) and Jan Terlouw (1989). Intuitionistic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
logics were first described as pure type systems by Barendregt. In his PhD thesis, Berardi defined a classical logic cube containing constructive logics akin to the lambda cube (these specifications are non-dependent). A modification of this cube was later called the L-cube by Geuvers, which in his PhD thesis extended the Curry–Howard correspondence to this setting. Based on these ideas, Barthe and others defined classical pure type systems (CPTS) by adding a double negation
Double negation
In the theory of logic, double negation is expressed by saying that a proposition A is identical to not , or by the formula A = ~~A. Like the Law of Excluded Middle, this principle when extended to an infinite collection of individuals is disallowed by Intuitionistic logic...
operator.
Similarly, in 1998, Tijn Borghuis introduced modal pure type systems (MPTS). Roorda has discussed the application of pure type systems to functional programming; and Roorda and Jeuring have proposed a programming language based on pure type systems.
The systems from the lambda cube are all known to be strongly normalizing. Pure type systems in general need not be, for example U from Girard's paradox is not. (Roughly speaking, Girard
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
found pure systems in which one can express the sentence "a type is a type".) Furthermore, all pure type systems that are not strongly normalizing are not even (weakly) normalizing: they contain expressions that do not have normal forms, just like the untyped lambda calculus. It is a major open problem in the field whether this is always the case, i.e. whether a (weakly) normalizing PTS always has the strong normalization property. This is known as the Barendregt–Geuvers–Klop conjecture (named after Henk Barendregt, Herman Geuvers, and Jan Willem Klop).
Implementations
The following programming languages have pure type systems:Further reading
- David A. Schmidt, The structure of typed programming languages, MIT Press, 1994, ISBN 0262193493, section 8.3, "Generalized Type Systems"
External links
- Pure Type Systems overview by Roger Bishop Jones