An optimized type inference algorithm with lazy type substitution

We propose a new type inference algorithm for polymorphic programming languages based on the idea of delaying type substitution until type variables are referenced. The resulting algorithm is expected to be practically more efficient by avoiding repeated and redundant application of type substitutions and scanning large type terms. We establish the soundness of the algorithm. The algorithm has been implemented for the full set of Standard ML type system, Our preliminary benchmark results show the expected performance.