Subtyping of first-class module types

Subtyping of first-class module types

[Alain Frisch]

Dear caml-list,

During today's ocaml meeting, the question of whether first-class module 
types could support subtyping was asked. I'd like to give a more 
detailed answer here.

The explicit subtyping construction (e : t1 :> t2) could easily be 
extended to support subtyping of the form

    (module S with type t1 = ...) :> (module S)

that is, to forget some type annotations. One could also support 
subtyping of the form:

    (module S) :> (module S')

provided that S is a subtype of S' (as module types), and *moreover* 
that the coercion from S to S' is the identity. The only real use I 
could see for it is when S and S' refer to the equal module types but 
they are just different names (in which case (module S) and module 
(module S') cannot be unified). The reason to require the coercion S ~~> 
S' to be trivial is that the explicit subtyping construction is assumed 
to be a runtime no-op.

That said, it is not difficult to use subtyping of module types by hand 
as in:

    (module (val x : S) : S')

which works as soon as S is a subtype of S'. Concretly, the code 
generated for this piece of code is simply the coercion from module type 
S to module type S'. This also work to forget type annotations (in which 
case the coercion is the identity).

Given how simple this construction is, I don't think it is worth 
extending the ( :> ) relation to support module types in very limited cases.


Alain