In this paper we present an application of Constraint Logic Programming to the design and implementation of type inference algorithms for programming languages. We present implementations in Prolog and Constraint Handling Rules (CHR) of several algorithms which belong to the state of the art of type inference for programming languages: the Damas-Milner type system, the Ohory system for labeled records and the Rank-2 Intersection Type system. In our implementation the differences between the general aspects of the type inference algorithms and the constraint resolution modules become more clear, when compared to other implementations of the same systems, usually made in a functional programming language. In the constraint modules, solving equality constraints, here implemented by Prolog unification, is completely separated from constraint simplification, which is made by solvers implemented in CHR for each system. Constraint Logic Programming revealed to be a highly declarative specification and implementation language for type inference algorithms.

Keywords: Type systems; Lambda-calculus.