[Caml-list] First class modules aliases

[Caml-list] First class modules aliases

[Christophe Troestler]

Hi,

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)

That's unfortunate because one may want to use the shortcut “IA” to
constraint various module types and still expect to be able to use the
general functions for “int a” on those.

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

This problem makes modularity more difficult.

Are the above problems that one has to learn to live with when using
first class modules or may we expect the type checker to be able to
cope with them in the future?

Best,
C.

Re: [Caml-list] First class modules aliases

[Alain Frisch]

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

Re: [Caml-list] First class modules aliases

[Jacques Garrigue]

On 2014/02/14 17:57, Alain Frisch wrote:

> 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.

Moscow ML uses this relaxed equality, and this does not seem to be a problem.
However, this requires some care when handling free variables.

>> 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.  

This is already done in trunk.

Jacques Garrigue

Re: [Caml-list] First class modules aliases

[Alain Frisch]

On 02/14/2014 10:08 AM, Jacques Garrigue wrote:
 > On 2014/02/14 17:57, Alain Frisch wrote:
>>    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.
>
> This is already done in trunk.

Are you sure?  I don't see it.  We're talking about keeping equations 
for module type declarations, not for module declarations, right?

-- Alain

Re: [Caml-list] First class modules aliases

[Alain Frisch]

On 02/14/2014 09:57 AM, Alain Frisch wrote:
>  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.

Another example which is fixed by this patch is the following (reported 
by my colleague David Waern):

==============================================
module M =
   struct
     module type T = sig type t end
     type t = (module T)
   end

module type X =
   sig
     module K: sig type t end
   end

module Make(A : sig type t end)(X: X with type K.t = A.t) = struct end

module Z = Make(M)(struct module K = M end)
==============================================


-- Alain

Re: [Caml-list] First class modules aliases

[Jacques Garrigue]

On 2014/02/14 18:22, Alain Frisch wrote:

> On 02/14/2014 10:08 AM, Jacques Garrigue wrote:
> > On 2014/02/14 17:57, Alain Frisch wrote:
>>>   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.
>> 
>> This is already done in trunk.
> 
> Are you sure?  I don't see it.  We're talking about keeping equations for module type declarations, not for module declarations, right?

Sorry, I got confused.
What trunk does is allowing to use aliases of module types in first class modules.
This was not allowed before.
What you suggest is also introducing aliases in place of copying for module types when using include.
This would be useless without the previous change, but makes sense with it.

	Jacques

Re: [Caml-list] First class modules from C

[Alain Frisch]

On 2/15/2014 3:23 PM, Christophe Troestler wrote:
> When passing a packed module to a C function, do we access its values
> as if it was a record (in the order of the signature) or is it more
> complicated?  A description in the user manual would be nice!

Yes, currently, this is how a first-class module is represented, and you 
need to know exactly what in the signature count for one slot.  But this 
representation is not specified, and not guaranteed to remain like that 
in future  versions (in particular, it might very well be the case that 
first-class modules would receive an extra unique identifier field, to 
be used by the generic hash/compare functions).  It seems more robust to 
access components from an OCaml function (called from C, if needed, or 
applied before/instead passing the packed module to C).


-- Alain