Type inhabitation

In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem:^[1] given a type ${\displaystyle \tau }$ and a typing environment ${\displaystyle \Gamma }$, does there exist a ${\displaystyle \lambda }$-term M such that ${\displaystyle \Gamma \vdash M:\tau }$? With an empty type environment, such an M is said to be an inhabitant of ${\displaystyle \tau }$.

Relationship to logic[]

In the case of simply typed lambda calculus, a type has an inhabitant if and only if its corresponding proposition is a tautology of minimal implicative logic. Similarly, a System F type has an inhabitant if and only if its corresponding proposition is a tautology of second-order logic.

Girard's paradox 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 proved that for simply typed lambda calculus the type inhabitation problem is PSPACE-complete. For other calculi, like System F, the problem is even undecidable.

See also[]

• Curry–Howard isomorphism

References[]

${\displaystyle \Gamma \vdash x:{\text{Int}}}$

This programming language theory or type theory-related article is a stub. You can help Wikipedia by .

• v
• t