Tech Report CS-89-40

Polymorphic Unification of ML Typing

Paris C. Kanellakis and John C. Mitchell

August 1989

Abstract:

We study the complexity of type inference for a core fragment of ML with lambda abstraction, function application, and the polymorphic let declaration. Our primary technical tool is the unification problem for a class of ``polymorphic'' type expressions. This form of unification, which we call {\em polymorphic unification,} allows us to separate a combinatorial aspect of type inference from the syntax of ML programs. After observing that ML typing is in DEXPTIME, we show that polymorphic unification is PSPACE hard. From this, we prove that recognizing the typable core ML programs is also PSPACE hard. From this, we prove that recognizing the typable core ML programs is also PSPACE hard. Our lower bound stands in contrast to the common belief that typing ML programs is ``efficient,'' and to practical experience which suggests that the algorithms commonly used for this task slow compilation substantially.

(complete text in pdf)