Types in programming languages serve to rule out nonsensical programs. Although untyped languages provide flexibility, they can contain subtle bugs. Types can be intrinsic or extrinsic depending on whether they appear annotated in the source program or not. For intrinsic types, the compiler verifies that a program admits a given type (type checking); for extrinsic types the compiler infers an appropriate type (type inference). Type annotations can be cumbersome in a practice, and so extrinsic types are desirable.

There are trade-offs between expressiveness and static guarantees. System F is an expressive type system that exhibits parametric polymorphism, which can enable code reuse in practice. Unfortunately, type inference is undecidable for System F. Robin Milner invented the ML language as a restricted variant of System F with a decidable type inference.

In this talk, I will discuss how we adapted results of constraint-based type systems to develop a modular ML type inference algorithm in Haskell. We use constraints as an intermediate representation, which enables a modular type inference algorithm.

The idea of a modularity is that a compiler only produces constraints and invokes an independent solver. The strengths are extensibility, complexity reasoning, and easier proofs of properties. HM(X) is a constraint-based generalization of Damas-Milner type system parametrized by constraints. For ML, we use syntactic equality constraints. Our representation consists of generation, transformation, and constraint solving. We present the generation and transformation functions suitable for a Haskell implementation. In the constraint generation stage, a ML program is translated to constraints. The constraint transformation stage translates constraints to a form solvable by first-order unification. We consider an important optimization step: avoiding multiple solving of a same constraint set that can be caused by let expression. In the constraint solving stage, the Robinson’s algorithm for first-order unification is implemented.