%0 Conference Proceedings
%F he88c
%A Henglein, Fritz
%T Type inference and semi-unification
%B LFP '88: Proceedings of the 1988 ACM conference on LISP and functional programming
%P 184-197
%I ACM
%C New York, NY, USA
%X 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.]
%U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein1988.pdf
%U http://doi.acm.org/10.1145/62678.62701
%8 July
%D 1988
%K parametricity