Ocaml destructive substitution error

Question

type ('a, 'r) loop
type 'e task
type ('a, 'e) tmpl'

module type COMPONENT =
sig
    type t
    type event
    type r

    val update : t -> event -> r
    val view : (t, event) tmpl'
end

module type MAIN_COMPONENT =
sig
    type t
    type event
    type r

    include COMPONENT
        with type t := t
        with type event := event
        with type r := (t * event task option, r) loop
end

I'm getting this error while trying to substitute the type r:

Error: Only type constructors with identical parameters can be substituted.

However, this works:

module type MAIN_COMPONENT =
sig
    type t
    type event
    type r
    type r' = (t * event task option, r) loop

    include COMPONENT
        with type t := t
        with type event := event
        with type r := r'
end

Why ?

How can i get rid of the r' type ?

Answer 1

This is a limitation of the destructive substitution - you can substitute only with a type constructor that has syntactically the same type parameters, not with arbitrary type expression. It is not a fundamental limitation, as you can easily work around it, as you have shown in your example.

There is, however, some sort of a code repetition there, that you can get rid of by using an abstraction (on the type level). In OCaml, you can use functors to create type-level abstractions, i.e., functions that take types and return types. The syntax is a little bit heavy, but with the properly chosen names and signatures, it can be fine.

Let's write the Loop abstraction, that will construct type (t1 * t2 task option, t3) loop from the provided types t1, t2, and t3:

module type T3 = sig type t1 type t2 type t3 end

module Loop(T : T3) = struct
  type t = (T.t1 * T.t2 task option, T.t3) loop
end

Given this definition, we can use the destructive substitution, as F(T).t is a type constructor without parameters, e.g.,

 module type MAIN_COMPONENT = sig
    type t
    type event
    type r

    module Types : T3 with type t1 = t
                       and type t2 = event
                       and type t3 = r

    include COMPONENT
        with type t := t
        with type event := event
        with type r := Loop(Types).t
end

The drawback is that you need to define the Types module since you can't construct modules directly in the functor application in a module signature.

Of course, in your case, the solution is much bigger, than what you proposed, so, probably, it is better to use yours. But in case if you definitions are big, you can use functors.