A General Type Inference Framework for Hindley/Milner Style Systems

摘要

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.