Proofs About a Folklore Let-Polymorphic Type InferenceAlgorithm

Abstract

The Hindley/Milner let-polymorphic type inference system has two different algorithms: one is the de facto standard Algorithm W that is bottom-up (or context-insensitive), and the other is a. "folklore" algorithm that is top-down (or context-sensitive). Because the latter algorithm has not been formally presented with its soundness and completeness proofs, and its relation with the W algorithm has not been rigorously investigated, its use in place of (or in combination with) W is not well founded. In this article, we formally define the context-sensitive, top-down type inference algorithm (named "M"), prove its soundness and completeness, and show a distinguishing property that M always stops earlier than W if the input program is ill typed. Our proofs can be seen as theoretical justifications for various type-checking strategies being used in practice.