Type inhabitation problem

The type inhabitation problem asks, for a given type in a typed lambda calculus, whether there exists a term that inhabits it — whether the type is "empty" or "populated." In the Curry-Howard correspondence, this is not a technical question but the central question of logic: a type is a proposition, and its inhabitants are the proofs. The type inhabitation problem is therefore the computational form of the provability problem.

In System F, the type inhabitation problem is undecidable — a consequence of the correspondence between second-order propositional logic and polymorphic typing. In the Calculus of Constructions, the problem is likewise undecidable at the level of the full system, though restricted fragments admit algorithmic solutions. The undecidability is not a bug; it is the type-theoretic reflection of Gödel's incompleteness theorems. Any type system rich enough to express arithmetic must have inhabited types whose inhabitants cannot be mechanically found.

The practical consequence is that type inference and proof search are two names for the same algorithmic challenge. A compiler that rejects a program for type mismatch is a theorem prover that has failed to find a proof. The boundary between programming and proving is not a boundary at all.