Algorithm W is the best known algorithm for implementing Hindley-Milner type inference. But it is a bit complicated as it intermingles two separate processes: constraint generation and solving.

There is an alternative approach based on constraints generation. In this approach, constraints are collected by bottom-up traversal, and then solved independently. Heeren’s Generalizing Hindley-Milner Type Inference Algorithms paper describes the algorithm in details.

Here’s my implementation of Heeren’s algorithm. I forked Stephen Diehls’s Poly and modified the type checker to use the Heeren’s algorithm.

I collected papers on the type inference algorithms used by Haskell-like languages.

Haskell

Haskell supports advanced type system features such as GADTs, type classes and type families. The current type checker implemented by GHC is described in OutsideIn(X): Modular type inference with local assumptions.

PureScript

The type checker of PureScript is inspired by the following papers. It supports type classes, row polymorphism, higher kinded polymorphism (rank N types). There are no soundness proofs yet.

• Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
• HMF: Simple Type Inference for First-Class Polymorphism
• Koka: Programming with Row-polymorphic Effect Types

Elm

Elm’s type checker is an implementation of Pottier and Rem’s The Essence of ML Type Inference with two extensions:

• A limited set of built-in type classes (i.e. number, appendable, comparable)
• Records based on Extensible records with scoped labels

There is no support for type classes or higher kinded polymorphism yet.