A General Type Inference Framework for Hindley/Milner Style Systems

Abstract

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 substitutionbased 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.

Acknowledgments

This work gained from fruitful discussions with Kevin Glynn, Peter Stuckey, Harald SØndergaard, Kwangkeun Yi and Christoph Zenger. Thanks goes also to the anonymous referres for their valuable feedback. In particular, I would like to thank Martin Müller for stimulating discussions about HM(X). He also contributed to the observation to separate the different type inference phases. Parts of this work were carried out while the author was at Yale University supported by DARPA Grant F30602-96-2-0232.