| Type inference algorithms form an important component of many functional language compilers. Traditional type inference algorithms, for example Alg. W , Alg. M etc., are characterized by intermittent constraint generation and constraint solving. Over the years, however, focus has shifted to algorithms which have a clear separation between constraint generation and constraint solving phases. Wand's algorithm was the first algorithm with such a separation. However, there is no direct extension of this algorithm to polymorphic let - a useful construct in many functional programming languages.;This work discusses an extension of Wand's type inference algorithm to the polymorphic let construct and the attempts at formal correctness of the extension. Specifically, this work discusses: (1) A multi-phase unification algorithm for a direct extension of Wand's algorithm to polymorphic let. (2) Informal proofs of completeness and soundness of Wand's algorithm (with respect to the Damas-Hindley-Milner type system) and its extension to polymorphic let. (3) Formal verification of a model of idempotent MGU axioms in Coq. (4) A formal proof of soundness of theWand's algorithm with respect to the Damas-Hindley-Milner type system. (5) Formal verification (in Coq) of several properties of Wand's algorithm which are helpful in a formal proof of completness of the Wand's type inference algorithm. |
