What is an unsafe functor?

Learning
8

Here’s a use-case for a recursive functor. I don’t know whether this is convincing as a case to add them to the language, since there seems to be a workaround. But I don’t really understand why the workaround works: it seems that recursive functors are allowed as long as the recursive functor call isn’t ever named or opened, but it can be referred to inline in a type definition. Is that intentional?

Suppose I have a functor defined elsewhere (like in someone else’s library that I can’t modify), for example:

module type Type = sig type t end
module Pair (T : Type) = struct type t = T.t * T.t end

I want to define a new type that recursively involves Pair of itself. I can do this with an ordinary recursive module (this is the main reason I ever use recursive modules):

module rec Foo1 : sig
  type t
end = struct
  module P = Pair(Foo1)
  type t = Zero | Suc of P.t
end

Now suppose I want my new type to also be parametrized over some other type in a functor. If I straightforwardly convert Foo1 into a functor, I get the “unsafe functor” error:

module rec Foo2 : functor (T : Type) -> sig
  type t
end = functor (T : Type) -> struct
  module P = Pair(Foo2(T))
  type t = Zero of T.t | Suc of P.t
end

--> Module Foo2 defines an unsafe functor, Foo2

It seems to be possible to avoid this error by doing the functor application inline rather than declaring the module P first, i.e. this works:

module rec Foo3 : functor (T : Type) -> sig
  type t
end = functor (T : Type) -> struct
  type t = Zero of T.t | Suc of Pair(Foo3(T)).t
end

Next suppose Foo also needs to define functions recursively on t. The naive way to do this gives a different error:

module rec Foo4 : functor (T : Type) -> sig
  type t
  val to_int : t -> int
end = functor (T : Type) -> struct
  type t = Zero of T.t | Suc of Pair(Foo4(T)).t
  let rec to_int : t -> int = function Zero _ -> 0 | Suc (x,_) -> to_int x + 1
end

-> Error: This expression has type Foo4(T).t
   but an expression was expected of type t

I assume what’s happening here is that the current module hasn’t been identified with its recursive call yet, so the compiler doesn’t know that t is the same type as Foo4(T).t. We can fix this by calling the version of to_int in Foo4(T) rather than the current module. But we can’t write Foo4(T).to_int, so we need to declare Foo4(T) as a local module, and then we get the same unsafe functor error:

module rec Foo5 : functor (T : Type) -> sig
  type t
  val to_int : t -> int
end = functor (T : Type) -> struct
  type t = Zero of T.t | Suc of Pair(Foo5(T)).t
  let to_int : t -> int = function
  | Zero _ -> 0
  | Suc (x,_) -> let module F = Foo5(T) in F.to_int x + 1
end

--> Module Foo5 defines an unsafe functor, Foo5.

Finally, this can be worked around by defining two separate functors, one recursive one for the type and another nonrecursive one to add the functions:

module rec InternalFoo : functor (T : Type) -> sig
  type t = Zero of T.t | Suc of Pair(InternalFoo(T)).t
end = functor (T : Type) -> struct
  type t = Zero of T.t | Suc of Pair(InternalFoo(T)).t
end

module Foo6 (T : Type) : sig
  type t
  val to_int : t -> int
end = struct
  include InternalFoo(T)
  let rec to_int : t -> int = function
  | Zero _ -> 0
  | Suc (x, _) -> to_int x + 1
end

This is a bit more boilerplate, though perhaps not that bad. But I don’t understand why it works, and I do think it would be more intuitive if Foo2 and Foo5 could work directly.