Unification and ML Type Reconstruction

We study the complexity of type reconstruction for a core fragment of ML with lambda abstraction, function application, and the polymorphic let declaration. We derive exponential upper and lower bounds on recognizing the typable core ML expressions. Our primary technical tool is unification of succinctly represented type expressions. After observing that core ML expressions, of size $n$, can be typed in $ DTIME( 2^n) $, we exhibit two different families of programs whose principal types grow exponentially. We show how to exploit the expressiveness of the let-polymorphism in these constructions to derive lower bounds on deciding typability: one leads naturally to NP-hardness and the other to $ DTIME( 2 ^ {n ^ k} )$-hardness of each integer $k~\geq~1$. Our generic simulation of any exponential-time Turing machine by ML type reconstruction may be viewed as a nonstandard way of computing with types. Our worst-case lower bounds stand in contrast to practical experience, which suggests that commonly used algorithms for type reconstruction do not slow compilation substantially.