Fritz Henglein. Polymorphic Type Inference and Semi-Unification. PhD Thesis Rutgers University, April 1989.
Download paper:
Adobe portable document (pdf)
Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
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
[ Parametricity ]
@PhdThesis{he89a,
Author = {Henglein, Fritz},
Title = {Polymorphic Type Inference and Semi-Unification},
School = {Rutgers University},
Month = {April},
Year = {1989}
}
Get EndNote Reference (.ref)