Martin Sulzmann. A General Type Inference Framework for Hindley/Milner Style Systems. In Herbert Kuchen, Kazunori Ueda, editors, Functional and Logic Programming, 5th International Symposium, FLOPS 2001, Tokyo, Japan, March 7-9, 2001, Proceedings. Volume 2024 of Lecture Notes in Computer Science, pages 248-263, Springer, 2001. [doi]
We propose a constraint-based formulation of Hindley/Milner style type inference system as opposed to the standard substitution-based formulation. This allows us to make important distinctions between different phases of type inference: Constraint generation/propagation, constraint solving, constraint simplification and term reconstruction. The inference system is parametric in the constraint domain, covering a wide range of application domains. A problem, incompleteness of substitution-based inference, identified by A. J. Kennedy can be solved naturally by employing a constraint-based view of type inference. In addition, our formulation of type inference can easily be tailored to different inference algorithms such as W and M. On the technical side, we present concise soundness and completeness results.