An Analysis of ML Typability

Abstract

We carry out an analysis of typability of terms in ML. Our main result is that this problem is DEXPTIME-hard, where by DEXPTIME we mean DTIME1994). This, together with the known exponential-time algorithm that solves the problem, yields the DEXPTIME-completeness result. This settles an open problem of P. Kanellakis and J. C. Mitchell. Part of our analysis is an algebraic characterization of ML typability in terms of a restricted form of semi-unification, which we identify as acyclic semi-unification. We prove that ML typability and acyclic semi-unification can be reduced to each other in polynomial time. We believe this result is of independent interest. © 1994, ACM. All rights reserved.