Posted on December 31, 2016
by Kwang Yul Seo
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.