TYPE INFERENCE WITH POLYMORPHIC RECURSION

The Damas-Milner Calculus is the typed lambda-calculus underlying the type system for ML an several other strongly typed polymorphic functio nal languages such as Miranda1 and Haskell. Mycroft has extended its p roblematic monomorphic typing rule for recursive definitions with a po lymorphic typing rule. He proved the resulting type system, which we c all the Milner-Mycroft Calculus, sound with respect to Milner's semant ics, and showed that it preserves the principal typing property of the Damas-Milner Calculus. The extension is of practical significance in typed logic programming languages and, more generally, in any language with (mutually) recursive definitions. In this paper we show that the type inference problem for the Milner-Mycroft Calculus is log-space e quivalent to semiunification, the problem of solving subsumption inequ ations between first-order terms. This result has been proved independ ently by Kfoury et al. In connection with the recently established und ecidability of semiunification this implies that typability in the Mil ner-Mycroft Calculus is undecidable. We present some reasons why type inference with polymorphic recursion appears to be practical despite i ts undecidability. This also sheds some light on the observed practica lity of ML in the face of recent theoretical intractability results. F inally, we exhibit a semiunification algorithm upon which a flexible, practical, and implementable type inference algorithm for both Damas-M ilner and Milner-Mycroft typing can be based.