In
type theory
In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.
Some type theories serve as alternatives to set theory as a foundation of ...
, a branch of
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, 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, whe ...
, 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 (), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The ...
, 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 polymorph ...
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 f ...
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 on ...
.
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).
System U was proved inconsistent by ...
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 (), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The ...
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 (PSPACE, polynomial space) and if every other problem that can be solved in polynomial sp ...
. 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 polymorph ...
, the problem is even
undecidable.
See also
*
Curry–Howard isomorphism
References
Lambda calculus
Type theory
{{type-theory-stub