In collaboration with Martin Odersky ,
I developed a general framework HM(X) for Hindley/Milner
style type systems with constraints, analogous to the CLP(X) framework in constrained logic programming.
Particular type systems can be obtained by instantiating the parameter X to a specific constraint system.
The Hindley/Milner system itself is obtained by instantiating X to the trivial constraint system.
Type systems in HM(X) are sound with respect to a standard untyped compositional semantics provided the
constraint system X is sound. Furthermore, we can give a generic type inference algorithm for HM(X).
Under sufficient conditions on X, type inference will always compute the principal type of a term.
Implementation of the HM(X) generic inference system:
Available are so far the core inferencer written in Haskell .
I've documented the parts which you need to fill in order to
obtain your own HM(X) instance.
As specific instances, you can download records in style of Ohori
and units in style of Kennedy.
- Yale Haskell Group
Last modified: Tue Jul 18 10:21:43 SGT 2006