Decision problems in polymorphic type
This talk will survey known results (some old ones and some new ones)
and open questions concerning decision problems related to various
type-assignment systems. These decision problems fall into essentially
• Typability and type-checking: Given a term M, determine if M can be
assigned a given type (or any type at all) in a given (or arbitrary)
• Type inhabitation (provability): Given a type t, determine if thereis
a term M such that M has type t (or equivalently, if t has a proof) in a
given type environment.
For the simply typed lambda-calculus, these problems are decidable in
polynomial time (type inference) or space (inhabitation). In polymorphic
calculi each of them can be undecidable; in particular the famous
theorem of Wells states that typability in system F is undecidable.
Little is known about decidable subsystems (or variants) of F, for
example it is an open problem if typability is decidable in the
In addition to the universal polymorphism of system F and its relatives,
this survey will cover the decision problems originating from
Curry-style, Church-style and domain-free calculi involving other forms
of polymorphism: existential, ad hoc (intersection types) and
first-order (dependent types).