In this thesis we present an implementation of the general
system for type inference algorithms HM(X) using Prolog and Constraint Handling
Rules. The type inference process may involve constraint resolution. Although
equality constraints might be easily solved using an unification algorithm,
other constraints may need more complex algorithms. In our implementation,
equality constraints are solved by unification using Prolog unification
with
occur-check, and other constraints are solved by a constraint
solver implemented in CHR. Based on the general system for type inference
algorithms HM(X), we implement:
- A general type inference algorithm;
- Instances for:
- the Damas-Milner type system;
- the Ohori system with records;
- the Nipkow e Prehofer system with type classes;
- the system O of Odersky, Wadler and Wehr.
In our implementation the difference between the general aspects of
the type inference algorithms and the constraint resolution module becomes
more clear when compared to other implementations of the same systems, usually
made in a functional programming language. CHR rules are a clear and natural
way of specifying the simplification mechanism.
