Constraint inference

This repository contains an indipendent implementation of the type inference algorithm described in the paper Generalizing Hindley-Milner Type Inference Algorithms. The paper Constraint Based Type Inferencing in Helium describes similar forms of type constraint.

Implementation

All the code contained in this repository is public domain.

There may be small divergences between this implementation and the paper pseudo-implementation.

This repo contains the following branches:

• main Original algorithm implementation with some additions, unstable.
• original Original algorithm implementation with detailed comments.
• clean A copy of the original branch without the comments.
• parser A copy of the original branch with the addition of a parser and repl.
• if-expr Same as the parser branch with the addition of n-tuples and if expressions.

Grammar

The main branch contains a parser and a little repl to check what types is inferred to an expression. Additionally, the main branch extends the algorithm described in the paper with n-tuples and if expressions. There is also the addition of a limited form of recursive bindings.

E ::=
  | x
  | E1 E2
  | \x -> E
  | let x = E1 in E2
  | rec x = E1 in E2
  | E1, ..., En
  | lit

Example

rec fact = \n -> if eq n 1
                 then 1
                 else mul n (fact (sub n 1))
in fact

rec fib = \n -> if eq n 1
                then n
				else fib (add ((sub n 1)) (fib (sub n 2)))
in fib

References

[1] Bastiaan Heeren, Jurriaan Hage, and Doaitse Swierstra. Generalizing Hindley-Milner Type Inference Algorithms. Institute of Information and Computing Sciences, Utrecht University, Netherlands, 2002.

[2] Bastiaan Heeren, Jurriaan Hage, and S. Doaitse Swierstra. Constraint Based Type Inferencing in Helium. Institute of Information and Computing Science, Universiteit Utrecht, Netherlands, 2003.