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.

This is my short summary of Philip Wadler’s Proofs are Programs: 19th Century Logic and 21st Century Computing.

Proofs and programs are the same thing. But it took a century of efforts to recognize the relationship.

• Modern logic began with Gottlob Frege’s Begriffschrift in 1879.
• Gerhard Gentzen introduced natural deduction in 1934.
• Alonzo Church introduced lambda calculus in 1932. He also introduced a typed version of lambda calculus in 1940.
• Dag Prawitz showed how to simplify natural deduction proofs directly in 1956.
• Haskell Curry noted a correspondence between the types of the combinators and the laws of logic as formulated by Hilbert in 1956.
• W. A. Howard put together the results of Curry and Prawitz, and wrote down the correspondence between natural deduction and lambda calculus in 1969.
• Howard’s work was published in 1980.

So it took more than 30 years to recognize the correspondence between Gentzen’s natural deduction and Church’s typed lambda calculus. They are the same thing! Proofs and programs. This correspondence is called Curry-Howard Isomorphism.

Logicians and computer scientists have discovered exactly the same type systems!

• Hindley-Milner type system: Hindley (1969), Milner (1978).
• Girard-Reynolds system: Girard (1972), Reynolds (1974).
• .. still being discovered