Theory about mutual recursion

Learning
, ,
1

I want to extend my HM typechecker with letrec by mutual recursion. Which sources could you recommend me, to get something close to OCaml type inference? I found [1] “Principal Typing and Mutual Recursion” paper, and it seems that LETREC^o rule is a way to go, but I’m not sure.

Also, the paper mentions both mutual an polymorphic recursion. Is it right to consider them as orthogonal features, such that (for simple languages) the former allows principal types, and the latter doesn’t?

[1] https://www.informatik.uni-kiel.de/~wflp2001/proceedings/papers/paper28.ps.gz

2

Mutual recursion can be desugared in some sense.

let rec f a = ... f x ... g y ...
and g b = ... f z ... g u ...

is equivalent to

let rec u = {
  f = (fun a -> ... u.f x ... u.g y ...);
  g = (fun b -> ... u.f z ... u.g u ...)
}

Of course the type checker, interpreter or compiler should not actually do that.

3

To infer letrec x = e in e', you infer the type of e and guess a monotype x : tau for x at the same time, and then you generalize this monotype into a type scheme x : sigma to check e'. Operationally, this can be described as "type-check e with a fresh inference variable '_a for x.

To infer letrec x1 = e1 and x2 = e2 in e', you infer e1 and e2, guessing monotypes for x1 and x2 at the same time, and then you generalize both to type-check e'. (Or: create inference variables x: '_a, y : '_b, and type-check e1 then e2.)

You can do slightly better in cases where some definitions don’t depend on others, so that the recursive definitions can be ordered – there is a non-trivial topological sorting into several strongly-conneected components. For example, if e1 needs x and y but e2 only needs x, you can first infer the type of e2, guessing a monotype for x, then generalize the type of e2 before checking e1 (so it infers a monotype for x, but gets a polymorphic scheme for e2); this can type-check more programs. For example:

let rec x n =
  if n = 0 then []
  else (y n "foo", y n true) :: x (n - 1)
and y n z =
  if n = 0 then z
  else y (n - 1) z
in ...

Finally, if you support polymorphic recursion through explicit annotations, you can refine the way you do the topological sorting above, by not considering as a dependency the mention of a recursive variable that is explicitly annotated (terms do not “need” explicitly-annotated variables in the sense above).

Note: you mention a paper by Figueiredo and Camarão, which is a sort of tutorial implementation. I would be careful with this paper, because the system it implements, which is presented in an earlier work of their, is probably incorrect: it claims to provide a decidable inference procedure for polymorphic recursion without annotations, which is known to be undecidable. (See Re: Decidable polymorphic recursion? , Re: Decidable polymorphic recursion? for the heated details).

1 Like
4

I thought about this but I didn’t understood in which order I should do generalization of types of x1 and x2. It was not obvious for me why two permutations should give the same result. So, I decided to google something, and got a buggy paper:)

5

If you geeneralize the types after checking all recursive definitions, you can generalize them in any order indeed, and you will get the same polymorphic schemes. (In my post I mentioned situations where you generalize some of those types before using them in other recursive definitions, and this does change the result.)