Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Hindley Milner type inference for mutually recursive functions

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?

like image 567
suhdonghwi Avatar asked Oct 17 '22 21:10

suhdonghwi


1 Answers

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

like image 117
PatJ Avatar answered Nov 15 '22 05:11

PatJ