Dependent type
Encyclopedia
In computer science
and logic
, a dependent type is a type
that depends on a value. Dependent types play a central role in intuitionistic type theory
and in the design of functional programming languages like ATS
, Agda and Epigram.
An example is the type of n-tuples of real numbers. This is a dependent type because the type depends on the value n.
Deciding equality of dependent types in a program may require computations. If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence type checking becomes undecidable
.
The Curry–Howard correspondence implies that types can be constructed that express arbitrarily complex mathematical properties. If the user can supply a constructive proof
that a type is inhabited (i.e., that a value of that type exists) then a compiler can check the proof and convert it into executable computer code that computes the value by carrying out the construction. The proof checking feature makes dependently typed languages closely related to proof assistants. The code-generation aspect provides a powerful approach to formal program verification and proof-carrying code
, since the code is derived directly from a mechanically verified mathematical proof.
developed the lambda cube
as a means of classifying type systems along three axes. The eight corners of the resulting cube-shaped diagram each correspond to a type system, with simply typed lambda calculus
in the least expressive corner, and calculus of constructions
in the most expressive. The three axes of the cube correspond to three different augmentations of the simply typed lambda calculus: the addition of dependent types, the addition of polymorphism, and the addition of higher kinded
type constructors (functions from types to types, for example). The lambda cube is generalized further by pure type system
s.
of pure first order dependent types, corresponding to the logical framework LF
, is obtained by generalising the function space type of the simply typed lambda calculus
to the dependent product type.
Writing
for 
-tuples of real numbers, as above, 
stands for the type of functions which given a natural number
n returns a tuple of real numbers of size n. The usual function space arises as a special case when the range type does not actually depend on the input, e.g.
is the type of functions from natural numbers to the real numbers, written as 
in the simply typed lambda calculus.
of second order dependent types is obtained from 
by allowing quantification over type constructors. In this theory the dependent product operator subsumes both the 
operator of simply typed lambda calculus and the 
binder of System F
.
extends 
to all four forms of abstraction from the lambda cube
: functions from terms to terms, types to types, terms to types and types to terms. The system corresponds to the Calculus of constructions
whose derivative, the calculus of inductive constructions
is the underlying system of the Coq proof assistant
.
.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
and logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, a dependent type is a type
Type system
A type system associates a type with each computed value. By examining the flow of these values, a type system attempts to ensure or prove that no type errors can occur...
that depends on a value. Dependent types play a central role in intuitionistic type theory
Intuitionistic type theory
Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
and in the design of functional programming languages like ATS
ATS (programming language)
ATS is a programming language whose stated purpose is to support theorem proving in combination with practical programming through the use of advanced type systems. The performance of ATS has been demonstrated to be comparable to that of the C and C++ programming languages...
, Agda and Epigram.
An example is the type of n-tuples of real numbers. This is a dependent type because the type depends on the value n.
Deciding equality of dependent types in a program may require computations. If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence type checking becomes undecidable
Undecidable problem
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is impossible to construct a single algorithm that always leads to a correct yes-or-no answer....
.
The Curry–Howard correspondence implies that types can be constructed that express arbitrarily complex mathematical properties. If the user can supply a constructive proof
Constructive proof
In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object with certain properties by creating or providing a method for creating such an object...
that a type is inhabited (i.e., that a value of that type exists) then a compiler can check the proof and convert it into executable computer code that computes the value by carrying out the construction. The proof checking feature makes dependently typed languages closely related to proof assistants. The code-generation aspect provides a powerful approach to formal program verification and proof-carrying code
Proof-Carrying Code
Proof-carrying code is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application's executable code. The host system can quickly verify the validity of the proof, and it can compare the conclusions of the proof to...
, since the code is derived directly from a mechanically verified mathematical proof.
Systems of the lambda cube
Henk BarendregtHenk 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...
developed the 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...
as a means of classifying type systems along three axes. The eight corners of the resulting cube-shaped diagram each correspond to a type system, with 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...
in the least expressive corner, and 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...
in the most expressive. The three axes of the cube correspond to three different augmentations of the simply typed lambda calculus: the addition of dependent types, the addition of polymorphism, and the addition of higher kinded
Kind (type theory)
In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator...
type constructors (functions from types to types, for example). The lambda cube is generalized further by pure type system
Pure type system
In the branches of mathematical logic known as proof theory and type theory, a pure type system , previously known as a generalized type system , is a form of typed lambda calculus that allows an arbitrary number of sorts and dependencies between any of these...
s.
First order dependent type theory
The system of pure first order dependent types, corresponding to the logical framework LFLF (logical framework)
In logic, a logical framework provides a means to define a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for ...
, is obtained by generalising the function space type of 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...
to the dependent product type.
Writing
for -tuples of real numbers, as above, stands for the type of functions which given a natural numberNatural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
n returns a tuple of real numbers of size n. The usual function space arises as a special case when the range type does not actually depend on the input, e.g.
is the type of functions from natural numbers to the real numbers, written as in the simply typed lambda calculus.Second order dependent type theory
The system of second order dependent types is obtained from by allowing quantification over type constructors. In this theory the dependent product operator subsumes both the operator of simply typed lambda calculus and the binder of System FSystem F
System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
.
Higher order dependently typed polymorphic lambda calculus
The higher order system extends to all four forms of abstraction from the lambda cubeLambda 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...
: functions from terms to terms, types to types, terms to types and types to terms. The system corresponds to 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...
whose derivative, the calculus of inductive constructions
Calculus of inductive constructions
The calculus of inductive constructions is the underlying core language of the Coq Proof Assistant. It is based on the calculus of constructions extended by inductive definitions as they are known from intuitionistic type theory....
is the underlying system of the Coq proof assistant
Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
.
Object-oriented programming
Some recent research has been directed at combining dependent type theory with object-oriented programmingObject-oriented programming
Object-oriented programming is a programming paradigm using "objects" – data structures consisting of data fields and methods together with their interactions – to design applications and computer programs. Programming techniques may include features such as data abstraction,...
.
Comparison
| Language | Actively developed | Tactics | Proof terms | Termination checking | Universes Universe (mathematics) In mathematics, and particularly in set theory and the foundations of mathematics, a universe is a class that contains all the entities one wishes to consider in a given situation... | Proof irrelevance | Program extraction | Extraction erases irrelevant terms | ||
|---|---|---|---|---|---|---|---|---|---|---|
| Agda | Purely functional Purely functional Purely functional is a term in computing used to describe algorithms, data structures or programming languages that exclude destructive modifications... |
Few/limited | Any term | Proof-irrelevant arguments (experimental) | ||||||
| ATS ATS (programming language) ATS is a programming language whose stated purpose is to support theorem proving in combination with practical programming through the use of advanced type systems. The performance of ATS has been demonstrated to be comparable to that of the C and C++ programming languages... |
Functional / imperative | |||||||||
| Cayenne | Purely functional | Any term | ||||||||
| Coq Coq In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification... |
Purely functional | Any term | ||||||||
| Dependent ML Dependent ML Dependent ML is an experimental functional programming language proposed by Hongwei Xi and Frank Pfenning. Dependent ML extends ML by a restricted notion of dependent types: types may be dependent on static indices of type Nat... |
Natural numbers | |||||||||
| Epigram 2 | Purely functional | Any term | ||||||||
| Guru http://code.google.com/p/guru-lang/ | Purely functional | Any term | ||||||||
| Idris http://www.cs.st-andrews.ac.uk/~eb/Idris/ | Purely functional | Any term | ||||||||
| Matita http://matita.cs.unibo.it/ | Purely functional | Any term | O'Caml | |||||||
| NuPRL NuPRL NuPRL is a higher-order proof development system developed at Cornell University. It was founded by Joseph L. Bates and Robert L. Constable in 1979 and, since then, many have contributed to the development of NuPRL.... |
||||||||||
| PVS Prototype Verification System The Prototype Verification System is a specification language integrated with support tools and a theorem prover.It was developed at the Computer Science Laboratory of SRI International in California. PVS is based on a kernel consisting of an extension of Church's theory of types with dependent... |
||||||||||
| Sage http://sage.soe.ucsc.edu/ | Hybrid typechecking | |||||||||
| Twelf Twelf Twelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory.-Introduction:... |
Logic programming Logic programming Logic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a... |
Any (LF) term | ||||||||
| Xanadu http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html | Imperative |
Further reading
- Why Dependent Types Matter T. Altenkirch, C. McBride, J. McKinna