Re: [Caml-list] First class modules aliases

[Alain Frisch <alain@frisch.fr>]

Hi Christophe,

On 02/14/2014 08:23 AM, Christophe Troestler wrote:
> I have encoutered several annoyances with module aliasing in the
> context of first class modules.  For example, if I declare
>
>      module type A = sig type t end
>      type 'a a = (module A with type t = 'a)
>      module type IA = A with type t = int
>      type ia = (module IA)
>
> then I expect the types “int a” and “ia” to be equivalent but this is
> not the case:
>
>      let f (a: int a) = (a : ia)
>
> gives the error
>
>      This expression has type int a = (module A with type t = int)
>      but an expression was expected of type ia = (module IA)

Indeed, two "package types" are equal (w.r.t. unification) if they have 
the same module type path (nominally, after expanding bare module type 
aliases) and the same list of constraints (modulo reordering).  In this 
case, module type paths are different (A and IA) and so are the lists of 
constraints (of respective length 1 and 0).

One could try to use a more relaxed definition of equality, based on 
actually comparing module type expressions.  At least for closed package 
types (i.e. for (module A with t = int) but not (module A with t = 'a)), 
this might be doable, although introducing a dependency between the 
unification algorithm and the equality check for module types might 
cause unexpected problems.

> Another example is:
>
>      module X = struct
>        module type T = sig type s end
>        type 'a t = (module T with type s = 'a)
>        let id (x: int t) = x
>      end
>
>      let f (x: int X.t) = x
>
>      module Y = struct
>        include X
>        let h x = f(id x)
>      end
>
> To make it work, I basically have to perform by hand the aliasing that
> “include X” should make:
>
>      module Y : sig type 'a t  val h : int t -> int t end = struct
>        type 'a t = 'a X.t
>        let h x = f(X.id x)
>      end

Here the problem is that "include X" copies the definition of the module 
type T, as if you had written:

   module T = sig type s end

and thus it introduces a new module type path.  Since package types use 
a nominal equality between module type paths, (module T) and (module 
X.T) are incompatible.   One way to fix it would be to tweak the 
"strengthening" algorithm which adds equalities to module types in order 
to turn a module type declaration to an alias to the original definition 
instead of copying it.  Concretely, one would change in 
Mtype.strengthen_sig:


   | Sig_modtype(id, decl) :: rem ->
       let newdecl =
         match decl.mtd_type with
           None ->
             {decl with mtd_type = Some(Mty_ident(Pdot(p, Ident.name id, 
nopos)))}
         | Some _ ->
             decl
       in
       ...

into:

   | Sig_modtype(id, decl) :: rem ->
       let newdecl =
             {decl with mtd_type = Some(Mty_ident(Pdot(p, Ident.name id, 
nopos)))}
       in
       ...

Since module type paths are interpreted nominally (for first-class 
modules), it could indeed make sense to keep the equation like that.

But maybe there are unfortunate consequences of doing so.  I hope that 
our usual experts of the type system will comment!



Alain