Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Subtyping of first-class module types
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2010-04-16 (18:22)
From: Alain Frisch <alain.frisch@l...>
Subject: Subtyping of first-class module types
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.