Hindley-Milner type inference with constraints

- January 2, 2017
Kwang's Haskell Blog - Hindley-Milner type inference with constraints

Hindley-Milner type inference with constraints

Posted on January 2, 2017 by Kwang Yul Seo

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.

Read more

Parametric Polymorphism and Girard-Reynolds Isomorphism

- February 21, 2014
Kwang's Haskell Blog - Parametric Polymorphism and Girard-Reynolds Isomorphism

Parametric Polymorphism and Girard-Reynolds Isomorphism

Posted on February 21, 2014 by Kwang Yul Seo

A talk by Phil Gossett given in Google’s Advanced Programming Language series is the best explanation of Curry-Howard isomorphism I’ve seen.

IMAGE ALT TEXT

He briefly mentioned the origin of type system at the beginning and explained Hindley-Milner, Type Classes (Wadler-Blott), Curry-Howard and Girard-Reynolds. Especially, he showed the relationship between parametricity and Girard-Reynolds isomorphism.

He finished his talk by describing Lennart Augustsson’s Djinn, which is small program that takes a (Haskell) type and gives you back a function of that type if one exists.

In his talk, he gave some examples of Curry-Howard isomorphism.

  • Intuitonistic logic <-> Combinatory logic (-> Lambda Calculus)
  • Girard representation theorem <-> Reynolds abstraction theorem
  • F2 <-> P2

BTW, there are a few technical errors in the talk. Please refer to Wadler’s comment on the talk.

Read more