What is an unsafe functor?

I am getting the following error:

Error: Cannot safely evaluate the definition of the following cycle
       of recursively-defined modules: Value -> Value.
       There are no safe modules in this cycle (see manual section 12.2).
  Module Value defines an unsafe functor, Monadic .

However, section 12.2 of the manual doesn’t say anything about what an “unsafe functor” is. I have looked through my code and I don’t think I have any unsafe values in the sense defined in the manual (I could try to post a MWE if it would help). And googling for “defines an unsafe functor” in quotes yields only two results from the entire Internet, neither of them helpful (one of them looks like it might be the source code for OCaml, the other I can’t find the phrase on the actual page).

All functors are considered as unsafe modules for the purpose of the recursive module check (there is a comment saying “can we do better ?”, probably left there a few decades ago). It doesn’t matter if the input or output signatures are safe or not.

Okay, thanks. It would be nice if that were documented, but at least now this discussion will be a third Google hit for “defines an unsafe functor”. Can you say anything about why functors are considered unsafe?

The following might be useful:

A proposal for recursive modules in Objective Caml
Xavier Leroy
INRIA Rocquencourt
Version 1.1, May 13, 2003

especially footnote 2 on p6:

² Notice that a functor is always unsafe. The reason for this is that the size of the closure representing the functor at run-time cannot be determined from its type, thus preventing the construction of a suitable initial value in phase 1 of the compilation scheme described later.

Thanks! I don’t know what “the closure representing a functor at run-time” is, or what its “size” is, or why that matters, but it sounds like it’s an implementation detail rather than a conceptual restriction or inconsistency.

Note that the whole notion of unsafe modules is an implementation detail. The exact definition of a “safe” module is “a module for which we have a hack allowing it to be initialized with a wrong value of the right type and patched later”. It excludes functors not because it is impossible to pre-initialize them but because we haven’t implemented it (and patching functions is a bit more complex than patching structures). In the same vein, a module that contains non-functional values whose definition does not depend on the recursive modules could be made safe, and there are traces of attempts to do that in the compiler’s code, but currently it’s rejected.
If you have a use-case for a recursive functor, I would encourage you to post an issue about it. I can think of a few ways to actually implement it, so if there is no strong disagreement it might end up being accepted.

Well, I thought I had a use-case when I posted this question, but I’ve since realized there is a simpler way to do what I want. So I probably won’t go ahead and post an issue right now, although I might change my mind again later. Thanks!

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.

Interestingly, you’ve ran into two of the three main issues of recursive modules: the semantics of initialization and the double-vision problem (the last one issue being the type-checking of recursive signatures).

For Foo4, the error comes from the lack of double-vision in OCaml: if a type is abstract in the signature of a recursive module, it is not identified with its definition in the code during the typechecking of the code – it can only be used as abstract. In the following example:

module rec X : sig type t end = struct
  type t = int
  (* knows t = int, but not X.t = int neither X.t = t *)
  let x : t = 42 (* works *)
  let y : X.t = 43 (* fails *)
  let z : t -> X.t = fun x -> x (* fails *)
end

It was described and solved by Dreyer (RTG), solved in the context of Mixin Modules and an OCaml solution was also proposed, but sadly never implemented.

Details

The way it works in current OCaml is that t and X.t are basically independent until the very last moment, when the inferred signature of X is strengthened (all abstract types are replaced by pointers to themselves) before being compared against the user-provided signature.

For Foo2 and Foo5, its the backpatch-semantics that is limited for your use-case. It would be nice to have a more complex system, and even some type-system safety guarantees for initialization (right now there are none). I don’t understand why functors should always be unsafe, it seems to me that their memory footprint could be known from their type (excluding abstract signatures).

For Foo5, could you also move the recursivity inside the functor, to get something like:

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

(but I don’t know if it fits in your real example)

I think that the main reason is that nobody bothered to implement it, but it’s not trivial either: if you allow a functor to have a valid (i.e. type-safe) implementation that just raises when it’s called, then you quickly run into recursive definitions that work just fine today but that will start throwing exceptions because now the functor is used too early.

In general, “safe” recursive modules behave badly (can’t track their fields properly, can raise exceptions if used too eagerly) so it’s better to make as many definitions unsafe as possible if it doesn’t prevent the code from compiling.

1 Like