Fritz Henglein. Type inference and semi-unification. In LFP '88: Proceedings of the 1988 ACM conference on LISP and functional programming, Pages 184-197, New York, NY, USA, July 1988.
Download paper: (link)
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.
The Milner Calculus is the typed lambda-calculus underlying the type system for the programming language ML [Har8G] and several other strongly typed polymorphic functional languages such as Miranda [Tur86] and SPS [Wan84]. Mycroft [Myc84] extended the problematical typing rule for recursive definitions and proved that the resulting calculus, termed Milner-Mycroft Calculus here, is sound with respect to Milner's [Mi178] semantics and that it preserves the principal typing property [DM82] of the Milner Calculus. The extension is of practical significance in typed logic programming languages [MO841 and, more generally, in any language with (mutually) recursive definitions. Mycroft didn't solve the decidability problem for typings in this calculus, though. This was an open problem independently raised also by Meertens [Mee83]. The decidability question was answered in the affirmative just recently by Kfoury et al. in [KTU88]. We show that the type inference problems in the Milner and the Milner-Mycroft Calculi can be reduced to solving equations and inequations between first-order terms, a problem we have termed semi-unification. We show that semi-unification problems have most general solutions in analogy to unification problems - which translates into principal typing properties for the underlying calculi. In con- trast to t!le (essentially) nonconstructive methods of [KTU88] we present functional specifications, which we prove partially correct, for computing the most general solution of semi-unification problems, and we devise a concrete nondeterministic algorithm on a graph-theoretic representation for computing these most general solutions. Finally, we point out some erroneous statements about the efficiency of polymor- phic type checking that have persisted throughout the literature including an incorrect claim, submitted by ourselves, of polynomial time type checking in the Milner-Mycroft Calculus. [Postscript: The above-mentioned decidability of semi-unification unfortunately turned out to be incorrect, as shown by the same authors who proved the problem to be undecidable in 1989.]
[ Parametricity ]
@InProceedings{he88c,
Author = {Henglein, Fritz},
Title = {Type inference and semi-unification},
BookTitle = {LFP '88: Proceedings of the 1988 ACM conference on LISP and functional programming},
Pages = {184--197},
Publisher = {ACM},
Address = {New York, NY, USA},
Month = {July},
Year = {1988}
}
Get EndNote Reference (.ref)