Explicit type binding and mutual recursion

Learning
3

For most use cases, if you want an explicit annotation for recursive function, it will be much simpler to use the type a. ... form:

let rec foo: type a. a -> a = fun x -> x
and bar: type a. a -> a = fun x -> foo x

This form is a shortcut for both adding an explicit universal quantified and and a corresponding locally abstract type (in other words let f : 'a . .... = fun (type a) -> ... ).

The root issue with

let rec f (type a) (x:a) = f x

is that the locally abstract type a is introduced after f. Moreover, without an explicit type annotation, a recursive function like f is monomorphic in its body and a monorphic function cannot be called on a type that was defined after the function.

In other words, the issue is that in term of type scopes, the function f is equivalent to

let f = ref Fun.id
type t = A
let x = !f A

which also fails with

Error: This expression has type t but an expression was expected of type 'a
       The type constructor t would escape its scope

This is why the second solution proposed by @Gopiandcode works. Indeed, in

let foo, bar = fun (type a) ->
  let rec foo (x: a) : a = x
  and bar (x: a) : a = foo x in
  foo, bar

the type a is defined before the recursive functions foo and bar, thus foo a does not break any scope constraint.

3 Likes