Discussion: forward type declaration

[alainfrisch]

OCaml does not allow splitting a set of mutually recursive definitions in different compilation units. For recursive functions, one can use forward declarations (let f_fwd = ref (fun _ -> assert false), and later assign it the real function). I'd like to propose adding to stdlib a bit of (internally unsafe) magic to enable a similar solution for recursive (non-parameterized) types. This could be a sub-module of Stdlib.Type:

module FwdType() : sig
  type t
  val define: unit -> (t, 'a) eq (** Can only be called once. *)
end = struct
  type t
  let defined = ref false
  let define () : (t, 'a) eq =
    if !defined then invalid_arg "..."
    else (defined := true; Obj.magic Equal)
end

(in a real implementation, one would need to make this multicore-safe)

Before proposing a full PR, I wanted to check if there would be some interest for such an addition to the stdlib. (And ask a question, see below.)

The idea is to apply this generative functor to declare an abstract type corresponding to a type that will be defined "later" (possibly in a different compilation unit). For instance, if we want to define two mutually recursive types A.t and B.t, one could write:

module FwdB = FwdType()

module A = struct
  type t =
    | A of t
    | B of FwdB.t
    | C of int
end

module B = struct
  type t =
    | A of A.t
    | B of t
    | C of int

  let eq : (FwdB.t, t) Type.eq = FwdB.define ()
end

Then, one can open the equality witness to "close the loop":

let rec eval_a : A.t -> int = function
  | A.A a -> eval_a a
  | A.B b -> let Equal = B.eq in eval_b b
  | A.C c -> c

and eval_b : B.t -> int = function
  | B.A a -> eval_a a
  | B.B b -> eval_b b
  | B.C c -> c

(and one could imagine having each evaluator implemented in its own module, with a forward value declaration.)

Unfortunately, it does seem to be currently possible to open the equality witness at toplevel (for the rest of the module);

let Equal = B.eq

let rec eval_a = ...
and eval_b = ...

So, in addition to proposing the addition of FwdType, I'd like to ask our type-checking experts if they see a way to extend the support for GADTs to allow such "global" opening of a type witness.

[github-actions[bot]]

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.