A Simple Algorithm and Proof for Type Inference

What is this?

This repository contains my OCaml implementation of Mitchell Wand's paper: "A Simple Algorithm and Proof for Type Inference"(1987).

This papers lays the foundations for type inference algorithms based on constraint generation and unification.

How do I use it?

The implementation is in inference.ml, just run it with ocaml inference.ml.

The test function inference takes an AST as input and prints the type of the AST and the generated equations. To solve the equations an algorithm such as Huet's first order unification algorithm can be used.

The AST is just Lambda Calculus so Variables, Lambda abstractions and Applications are defined.