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.
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.
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
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
[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.