%O Thesis 
%9 PhdThesis 
%F he89a
%A Henglein, Fritz
%T Polymorphic Type Inference and Semi-Unification
%I Rutgers University
%X In the last ten years declaration-free programming languages with a polymorphic typing discipline (ML, B) have been developed to approximate the flexibility and conciseness of dynamically typed languages (LISP, SETL) while retaining the safety and execution efficiency of conventional statically typed languages (Algol68, Pascal). These polymorphic languages can be type-checked at compile time, yet allow functions whose arguments range over a variety of types. We investigate several polymorphic type systems, the most powerful of which, termed Milner-Mycroft Calculus, extends the so-called let-polymorphism found in, e.g., ML with a polymorphic typing rule for recursive definitions. We show that semi-unification, the problem of solving inequalities over first-order terms, characterizes type checking in the Milner-Mycroft Calculus to polynomial time, even in the restricted case where nested definitions are disallowed. This permits us to extend some infeasibility results for related combinatorial problems to type inference and to correct several claims and statements in the literature. We prove the existence of unique most general solutions of term inequalities, called most general semi-unifiers, and present an algorithm for computing them that terminates for all known inputs due to a novel ``extended occurs check''. We conjecture this algorithm to be uniformly terminating even though, at present, general semi-unification is not known to be decidable. We prove termination of our algorithm for a restricted case of semi-unification that is of independent interest. Finally, we offer an explanation for the apparent practicality of polymorphic type inference in the face of theoretical intractability results
%U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein1989.pdf
%8 April
%D 1989
%K parametricity