Re: [Caml-list] First class modules aliases

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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