Hindley Milner type inference for mutually recursive functions

Question

I'm making a strongly typed toy functional programming language. It uses the Hindley Milner algorithm as type inference algorithm.

Implementing the algorithm, I have a question on how to infer types of the mutually recursive functions.

let rec f n = if n == 0 then 0 else g (n - 1)
let rec g n = if n == 0 then 0 else f (n - 1)

f and g are mutually recursive functions. Now, when the type checker is inferring the type of function f, it should also be able to infer the type of function g, since it is a subexpression.

But, in that moment, function g is not defined yet. Therefore, the type checker doesn't even know the existence of function g, as well as the type of function g, obviously.

What are some solutions that real world compilers/intepreters use?

This problem (family of problems?) in general is called unification, and there are several known algorithms for solving it. This applies to both types and logical formulas because the two are quite similar — Cubic
@Cubic I didn't know this problem is related to unification algorithm. Actually, I already implemented unify function, maybe without actually deeply understanding it. — suhdonghwi

PatJ PatJ · Accepted Answer · 2018-03-06T15:29:49

In OCaml, mutually recursive values are separated by the keyword and instead of another let rec. When the typing system arrives at a recursive definitions, it adds all the recursive names to the environment and then continues pretty much as usual.

UPDATE (thanks to K.A. Buhr):

It is totally possible to create a new variable with type 'a (with 'a being fresh) and then later unify it. Be sure to generalize your variable at the right place (usually, after the definition).

Hindley Milner type inference for mutually recursive functions

1 Answers