Writing type inference algorithms in OCaml

Learning
15

I hope there’s at least some space left for more discussion, as there are at least a couple of questions in this thread that remain unanswered, and the only example of elpi being used to handle the type inference for a language no longer compiles.

Anyway, if anyone else is following through Oleg’s tutorial (Efficient and Insightful Generalization), I’ve made a small barebones project skeleton which would probably be a good place to start working from:

It has a helper PPX that also converts OCaml syntax into corresponding values of the following ADT:

type term =
    Var of int
  | Lam of term
  | App of term * term
  | Let of term * term

i.e

let%syntax f x y = y x

becomes:

let f  = 
   Lam (Lam (App (Var 0, Var 1)))

which was quite useful when going through Oleg’s article, as it allowed me to check the type-checking algorithm at each step against OCaml’s one by simply removing the “%syntax” annotation and checking the OCaml type for the term.

1 Like