Let-Polymorphism and Eager Type Schemes 1997

Abstract:  This paper presents a new algorithm for polymorphic type inferencing involving the let contruct of ML. It avoids the gen operation of the algorithm W of Damas and Milner. This new algorithm is a closer counterpart to the proof-theoretic formulation of the ML typing discipline than other approaches. Sketches of the proofs of correctness, including completeness for the let case, are also given. The basic technique of the algorithm also facilitates the declarative formulation of type inference as goal-directed proof-search. Introduction Various formulations and algorithms for the inference or assignment of principal types to untyped -terms have long existed. In [2] Damas and Milner extended type-inferencing to involve the polymorphic let construct of functional programming langugaes (ML). They formulated a declarative, proof-theoretic calculus for the ML type system, given here in Figure 1. Unfortunately, this calculus does not by itself lead directly to an inference algorithm tha...