# Theory about mutual recursion

**URL:** <https://discuss.ocaml.org/t/theory-about-mutual-recursion/10822>\
**Category:** Learning\
**Tags:** type-inference, theory, mutual-recursion\
**Created:** [November 19, 2022, 1:32pm UTC](https://discuss.ocaml.org/t/theory-about-mutual-recursion/10822 "2022-11-19T13:32:32Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Kakadu](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/kakadu/32/1204_2.png) [@Kakadu](https://discuss.ocaml.org/u/Kakadu)\
**Post date:** [November 19, 2022, 1:32pm UTC](https://discuss.ocaml.org/t/theory-about-mutual-recursion/10822/1 "2022-11-19T13:32:32Z")

</div>

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](https://www.informatik.uni-kiel.de/~wflp2001/proceedings/papers/paper28.ps.gz)

---

<div class="post-metadata">

**Author:** ![luke36](https://avatars.discourse-cdn.com/v4/letter/l/5fc32e/32.png) [@luke36](https://discuss.ocaml.org/u/luke36)\
**Post date:** [November 19, 2022, 2:27pm UTC](https://discuss.ocaml.org/t/theory-about-mutual-recursion/10822/2 "2022-11-19T14:27:04Z")

</div>

Mutual recursion can be desugared in some sense.

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

```

is equivalent to

```ocaml
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.

---

<div class="post-metadata">

**Author:** ![gasche](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/gasche/32/4_2.png) [@gasche](https://discuss.ocaml.org/u/gasche)\
**Post date:** [November 19, 2022, 3:09pm UTC](https://discuss.ocaml.org/t/theory-about-mutual-recursion/10822/3 "2022-11-19T15:09:34Z")

</div>

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:

```ocaml
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?](https://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00918.html) , [Re: Decidable polymorphic recursion?](https://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00924.html) for the heated details).

---

<div class="post-metadata">

**Author:** ![Kakadu](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/kakadu/32/1204_2.png) [@Kakadu](https://discuss.ocaml.org/u/Kakadu)\
**Post date:** [November 19, 2022, 3:28pm UTC](https://discuss.ocaml.org/t/theory-about-mutual-recursion/10822/4 "2022-11-19T15:28:48Z")

</div>

> [@gasche](#):
>
> 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`.)

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

---

<div class="post-metadata">

**Author:** ![gasche](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/gasche/32/4_2.png) [@gasche](https://discuss.ocaml.org/u/gasche)\
**Post date:** [November 19, 2022, 8:32pm UTC](https://discuss.ocaml.org/t/theory-about-mutual-recursion/10822/5 "2022-11-19T20:32:15Z")

</div>

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