Type inference algorithms of Haskell-like languages

- December 31, 2016
Kwang's Haskell Blog - Type inference algorithms of Haskell-like languages

Type inference algorithms of Haskell-like languages

Posted on December 31, 2016 by Kwang Yul Seo

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


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.


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.


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

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

Read more

Summary of Philip Walder’s "Proofs are Programs"

- June 19, 2015
Kwang's Haskell Blog - Summary of Philip Walder’s "Proofs are Programs"

Summary of Philip Walder’s "Proofs are Programs"

Posted on June 19, 2015 by Kwang Yul Seo

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
Read more