How to convert 'module type' with 'non-generic type' to 'module type' with 'generic type' by destructive substitution?

Question

I have a module type with three non-generic types:

module type LAYER = sig
  type cytoplasm_t
  type nucleus_t
  type t

  val cytoplasm        : int -> t -> cytoplasm_t
  val nucleus          : int -> t -> nucleus_t 

  val add_cytoplasm    : int -> cytoplasm_t -> t -> t
  val add_nucleus      : int -> nucleus_t -> t -> t
  val remove_cytoplasm : int -> t -> t
  val remove_nucleus   : int -> t -> t
end

I want to convert it to a module type with a generic nested type that has two type parameters instead of two non-generic types as it is in the source module type:

module type LAYER' = sig
  type ('cytoplasm, 'nucleus) t

  val cytoplasm        : int -> ('c, 'n) t -> 'c
  val nucleus          : int -> ('c, 'n) t -> 'n 

  val add_cytoplasm    : int -> 'c -> ('c, 'n) t -> ('c, 'n) t
  val add_nucleus      : int -> 'n -> ('c, 'n) t -> ('c, 'n) t
  val remove_cytoplasm : int -> ('c, 'n) t -> ('c, 'n) t
  val remove_nucleus   : int -> ('c, 'n) t -> ('c, 'n) t
end

I tried to do that by 'include' with ':=' but failed:

module type LAYER' = sig
  type ('c, 'n) t
  
  include LAYER 
     with type t := ('c, 'n) t
      and type nucleus_t := 'n
      and type cytoplasm_t := 'c
end 

Error: The type variable 'c is unbound in this type declaration

As I expected, destructive substitution doesn't work like replacement. I have a long list of functions in my real-life example, and this feature would be helpful for me. Is it possible to do that?

Answer 1

No, this is not possible. You cannot replace a type of a given arity with an implementation of another arity.

Why not becomes clearer when we make the arities and the binders of type variables more explicit than in basic ML syntax, where they are left implicit.

With some made-up syntax, your first signature then becomes:

module type LAYER =
sig
  type t : 0
  type cytoplasm_t : 0
  type nucleus_t : 0
  val cytoplasm : int -> t -> cytoplasm_t
  val add_cytoplasm : int -> cytoplasm_t -> t -> t
  ...
end

while your second is:

module type LAYER' =
sig
  type t : 2
  type cytoplasm_t = ???
  type nucleus_t = ???
  val cytoplasm : forall ('c, 'n). int -> ('c, 'n) t -> 'c
  val add_cytoplasm : forall ('c, 'n). int -> 'c -> ('c, 'n) t -> ('c, 'n) t
  ...
end

If the replacement you want was allowed: (1) what would the binders for 'c and 'n in types cytoplasm_t and nucleus_t be? (2) where would the forall for them come from for value cytoplasm? And (3), why is it correct to assume that all occurrences of t for add_cytoplasm share the same arguments — it could just as well become one of these:

val add_cytoplasm : forall ('c1, 'n1, 'c2, 'n2). int -> 'c1 -> ('c1, 'n1) t -> ('c2, 'n2) t
val add_cytoplasm : forall ('c1, 'n1, 'c2, 'n2). int -> 'c2 -> ('c1, 'n1) t -> ('c2, 'n2) t

---

Now to answer your question practically, the only solution is to do it the other way round: the original signature must anticipate the most polymorphic usage. Then you can make it less polymorphic by replacement. For example:

module type LAYER' =
sig
  type ('c, 'n) t
  type ('c, 'n) cytoplasm_t
  type ('c, 'n) nucleus_t
  val cytoplasm : int -> ('c, 'n) t -> 'c
  val add_cytoplasm : int -> 'c -> ('c, 'n) t -> ('c, 'n) t
  ...
end

module type LAYER =
sig
  type t
  include LAYER'
    with type ('c, 'n) t := t
    with type ('c, 'n) cytoplasm_t := 'c
    with type ('c, 'n) nucleus_t := 'n
end

This way, you make explicit where all the binders are, and the replacement later just makes some of them redundant.