Principal typings demystified: what they are, why you want them,
and why your type system doesn't have them.
Joe Wells
Abstract
Let S be some type system. A typing in S for a typable term
M is the collection of all of the information other than M which
appears in the final judgement of a proof derivation showing that M is
typable. For example, suppose there is a derivation in S ending with
the judgement A |- M : tau meaning that M has result type tau when
assuming the types of free variables are given by A. Then (A, tau) is
a typing for M.
A principal typing in S for a term M is a typing for M which somehow
represents all other possible typings in S for M. It is important not
to confuse this notion with the weaker notion of principal type often
mentioned in connection with the Hindley/Milner type system. Previous
definitions of principal typings for specific type systems have
involved various syntactic operations on typings such as substitution
of types for type variables, expansion, lifting, etc.
This talk presents a new general definition of principal typings which
does not depend on the details of any particular type system. This
talk shows that the new general definition correctly generalizes
previous system-dependent definitions. This talk explains why the new
definition is the right one. Furthermore, the new definition is used
to prove that certain polymorphic type systems using "for all"
quantifiers, namely System F and the Hindley/Milner system, do not
have principal typings.