In
type theory
In mathematics, logic, and computer science, a type theory is the formal system, formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theor ...
, a branch of
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
, in a given typed calculus, the type inhabitation problem for this calculus is the following problem:
given a type
and a
typing environment In type theory a typing environment (or typing context) represents the association between variable names and data types.
More formally an environment \Gamma is a set or ordered list of pairs \langle x,\tau \rangle, usually written as x:\tau, where ...
, does there exist a
-term M such that
? With an empty type environment, such an M is said to be an inhabitant of
.
Relationship to logic
In the case of
simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of 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 ...
, a type has an inhabitant if and only if its
corresponding proposition is a
tautology of minimal implicative logic. Similarly, a
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphi ...
type has an inhabitant if and only if its
corresponding proposition is a tautology of
intuitionistic
In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of ...
second-order logic
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.
First-order logic quantifies ...
.
Girard's paradox
In mathematical logic, System U and System U− are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules (or dependencies between the sorts). They were both proved inconsistent by Jea ...
shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types.
Formal properties
For most typed calculi, the type inhabitation problem is very
hard.
Richard Statman
Richard Statman (born September 6, 1946) is an American computer scientist whose principal research interest is the theory of computation, especially symbolic computation. His research involves lambda calculus, type theory, and combinatory alge ...
proved that for
simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of 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 ...
the type inhabitation problem is
PSPACE-complete In computational complexity theory, a decision problem is PSPACE-complete if it can be solved using an amount of memory that is polynomial in the input length ( polynomial space) and if every other problem that can be solved in polynomial space can ...
. For other calculi, like
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphi ...
, the problem is even
undecidable.
See also
*
Curry–Howard isomorphism
References
Lambda calculus
Type theory
{{type-theory-stub