Writing type inference algorithms in OCaml

What recommendations would you give for OCaml libraries and tooling for writing type inference (or specifically unification) algorithms?

I often find myself writing small programming languages in OCaml. Thanks to Menhir and OCamllex, the parsing part of that problem is pretty straightforward, and the use of ADTs makes the subsequent compilation process fairly easy as well.

However, the last time I tried implementing a type inference algorithm for a non-trivial small language, I spent around a week doing it, and ended up with a buggy unification algorithm, with errors that that were quite hard to wrap my head around.

Are there any libraries that I could outsource to do the unification part for me (performance be damned)? Ideally, It would be best if I could express the typing judgements as declarative statements, and have the library handle resolving type variables to their instantiations.

ELPI seems like the most promising solution, but its documentation leaves a lot to be desired, and after a few hours trying to navigate its rather complex API, have little to show for it.

2 Likes

The Programming Languages Zoo is a good place to find such examples as well as this repository to Grow Your Own Type System.

1 Like

Ah, thanks for the links - I hadn’t come across those before, and probably would serve as a good place to look for ideas on structuring a compiler pipeline, but having skimmed a few of these, they all seem to implement the type unification manually rather than using a library.

To be clear, I’m roughly familiar with the structure of how type inference should be done - i.e traverse the parse tree, generate a fresh type variable for each expression and then generate constraints, and then use these constraints to resolve the type variables to corresponding types.

I once wrote one such algorithm:

Overall, this ended up being ~7000 lines, and rather impenetrable to follow, and pretty much put me off trying to write unification from scratch ever again.

I am more looking for some kind of approach/library that could make it possible to implement the type inference algorithm with slightly less hassle.

1 Like

I was going to suggest that you consider Elpi. I am currently using this for my PhD, as a meta-language for Coq, to implement a tactic that changes a Coq goal and proves the applied changes. Therefore I am doing a lot of term manipulations in Elpi, and I must say the Prolog-flavour unification and logical rule shape of the code are appreciable for such applications.

If you need any help concerning the language in itself do not hesitate to ask, I would be happy to help. Concerning the API to access it from OCaml, I am afraid I cannot really give any advice as I haven’t tried such a connection yet.

3 Likes

There’s the inferno library (POTTIER Francois / inferno · GitLab) that deals with unification using constraints.

But I’ve never actually used the library. I usually just implement the union find algorithm described in Chapter 6 of Programming Language Concepts by Peter Sestoft, which usually takes ~20 lines or so of code to implement unification if you don’t need generalization or occurs checks.

2 Likes

“Reusable type-inference library” is the goal of the Inferno library from @fpottier, which I use and contribute to. Have a look!

This being said, it is a hard problem to abstract over, and the high-level layers of Inferno require new contributions for each new/orthogonal type-system feature one wants to support – currently only a fragment of ML-family languages are supported. There is a lower-level layer of efficient unification, that is easier to reuse for arbitrary type-inference programs.

I agree that Elpi is also a tool worth looking at in this design space; you could try implementing your type-inference engine in Lambda-prolog as powered by Elpi, but I think that requires some familiarity with Lambda-prolog to work well. Another prolog-family language in this space is Makam.

3 Likes

Thanks you for the reference - ahh, I should definitely read the parts about the implementation of type inference rather than just winging it - I guess once I had the general picture of how the constraint based inference worked, I skipped straight to implementing it without reading about union-find/efficient ways of solving constraints - my implementation used a mix of equivalence classes for cannonicalising type variables, and a substitution based unification loop.

Ah, thanks, yes, inferno looks promising, and having looked at the examples, seems fairly straightforward to use.

Looking through the Elpi repository, there seem to be enough examples there that I feel reasonably confident that I could work out how to embed a type system into the language - the problem I’m having is that it’s rather challenging to access it programmatically - the compiler/parser part is somewhat straightforward, but I’ve been stumped on which API endpoints I would use to convert my syntax tree (parsed elsewhere) into a query to submit to Elpi.

Oleg’s site has a pretty awesome description of union-find style unification as well: Efficient and Insightful Generalization

1 Like

Thanks for the reference - just went through it, and it was very insightful.

Actually, I had briefly skimmed this article before, but had not read it in detail because the type checking / inference was being done during the traversal of the AST:

let rec typeof : env -> term -> typ = fun env -> function
  | Var n -> inst (lookup_ty n env)
  | Lam tm ->
    let ty_x = new_var () in
    let ty_e = typeof (ty_x :: env) tm in
    Tarrow (ty_x, ty_e)
  | App (e1, e2) ->
    let ty_fun = typeof env e1 in
    let ty_arg = typeof env e2 in
    let ty_res = new_var () in
    unify ty_fun (Tarrow (ty_arg, ty_res));
    ty_res

I had read somewhere that it was better to handle these separately - i.e to do the traversal in one pass and generate constraints, and then solve them separately. Hence, in my code, I’d first traverse and generate a set of constraints:

    | S.AlphaFunction (f1, e1) ->
      let loc = (S.expr_to_loc e1) in

      let f1 = annotate_comparison_func f1 in
      let e1, c1 = annotate_expr src env e1 in
      let constraints =
        (* ref value must be float *)
        `Eq (from_variable (AstUtils.type_expr e1),
             from_scalar @@ (Type.TyFloat loc)) :: c1 in
      AlphaFunction (f1, e1), constraints

and then separately run an algorithm to loop over these constraints and iteratively reduce them.

This may have been the cause of the complexity, because when the type inference failed, all I had was a long list of constraints, with no direct link back to the program AST, which made it near impossible to localise where my errors came from.

I’m curious - Oleg’s site doesn’t mention splitting out the inference from the traversal at all - obviously it shouldn’t be too hard to translate between the two approaches, but I’m wondering if this was omitted for the sake of simplifying the example, or whether in practice you don’t actually need to do this?

1 Like

Alright, I’ve been messing around some more with the code from Oleg’s site, but I seem to have run into a bug with the code on the site.

In particular, with the unify function:

     let rec unify : typ -> typ -> unit = fun t1 t2 ->
       if t1 == t2 then ()                   (* t1 and t2 are physically the same *)
       else match (t1,t2) with
       | (TVar ({contents = Unbound _} as tv),t') | (t',TVar ({contents = Unbound _} as tv)) -> 
           occurs tv t'; tv := Link t'
       | (TVar {contents = Link t1},t2) | (t1,TVar {contents = Link t2}) -> 
           unify t1 t2
       | (TArrow (tyl1,tyl2), TArrow (tyr1,tyr2)) ->
           unify tyl1 tyr1;
           unify tyl2 tyr2

Shouldn’t the case for handling links occur before the case for unbound type variables?

For example in the case where you have arguments as:

let t = fresh_var () in
(t, Tvar { contents = Link t })

i.e (the two arguments are semantically equal modulo a irrelevant Link, but because the link case is second, the code would run an occurs check and cause a failure)

1 Like

I have a few issues mapping stuff descriped in Oleg’s paper to OCaml implementation. It looks like in OCaml we have two-level types, so a mutable field is declared in upper level. On lower level Oleg has two algebraic constructors | TVar of tv ref and | QVar of qname but in OCaml I found only single one: | Tvar of string option (option is not important though).

Could somebody point me to the second constructor for variable or explain why we don’t need the second one in case of two-level types?

Maybe I’m misunderstanding your question, but isn’t that [the lack of a separate constructor for quantified type variables], explained later on in the article:

The first, seemingly unprincipled change, is to eliminate QVar as a distinct alternative and dedicate a very large positive integer – which should be treated as the inaccessible ordinal ω – as a generic_level. A free type variable TVar at generic_level is taken to be a quantified type variable.

    let generic_level = 100000000           (* as in OCaml typing/btype.ml *)

Thanks for the interesting point, and I love all the comments here. I hope this discussion develops further so that maybe it becomes a gentle introduction to the OCaml type system!

1 Like

I think we have pretty much exhausted the discussion on “Writing type inference algorithms in OCaml”.

For more on OCaml’s type system, I can recommend Didier Rémy’s notes from Applied Semantics:

Also a disclaimer. I’ve only only read Chapter 3: The object layer. The chapter is definitely worth reading if you want to know about the object layer, but the warning below applies to this chapter as well.

I don’t think the notes are “a gentle introduction”. Especially, if you have not seen formal definitions of type systems before. I don’t want to discourage people from diving into it and learning type theory/systems as they go and skipping over things that they aren’t ready to handle, but beginners beware!

(Sorry if the warning feels patronizing, I have no idea what your background is. I am very self-conscious about trying to introduce people to type theory when they aren’t ready for it.)

2 Likes

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

W.r.t what to follow on from Oleg’s article, I found The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy to be quite a nice and straightforward paper to read after reading Oleg’s one, and I was able to see how the type inference algorithm described in Efficient and Insightful Generalization could be extended to handle subtyping in the way described in the paper. It was quite reassuring to be able to relate the implementation from Oleg’s article in OCaml to the Scala implementation, and I think it helped improve my understanding overall.

3 Likes

Yes, I think that you are correct. (With a repr function that normalizes along links we would use let t1, t2 = repr t1, repr t2 before the equality test.)

1 Like

I’ve also been playing with type inference recently/implementing that paper in OCaml, another thing that’s fun to implement is row polymorphism as described very clearly in Extensible records with scoped labels.

2 Likes