Re: [Caml-list] A limitation of "with type" declarations for first-class modules

[Yaron Minsky <yminsky@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2624 bytes --]

For anyone who is interested, here is the bug report:

   http://caml.inria.fr/mantis/view.php?id=5358

y

On Tue, Sep 20, 2011 at 6:07 PM, Yaron Minsky <yminsky@gmail.com> wrote:

> On Tue, Sep 20, 2011 at 5:03 PM, Alain Frisch <alain.frisch@lexifi.com>wrote:
>
>>
>> The important point is that package types (the ... in a type expression
>> (module ...) or in an expression (module M : ...)) are not module types.
>> Syntactically, they are indeed a subset of module types, but it is a strict
>> subset, and they obey different rules than module types.
>>
>> Package types live at the boundary between types and module types. In a
>> packing expression (module M : ...), the package type must produce a
>> well-typed module type. This is why you cannot write (module M : S with type
>> t = 'a), because "S with type t = 'a" is not a proper module type. But
>> (module S with type t = 'a) is a correct type.
>>
>> Package types must also support all operations on types, including
>> equality, unification, etc.  For instance, unifying (module S1 with type t =
>> 'a) and (module S2 with type t = 'b) is defined as checking than S1 and S2
>> are equivalent paths and unifying 'a and 'b. The fact that a package type
>> can also be seen as a module type is nowhere used in this definition. (Of
>> course, one must be careful when defining equality of package types that it
>> does not allow to cast a module from one module type to an incompatible
>> one.)
>>
>> There is some flexibility in both the definition of admissible package
>> types and the definition of equality between package types.
>>
>> For instance, I don't see any problem or difficulty in your proposal of
>> allowing constraints on types nested in sub-modules (but this should be
>> checked carefully). Feel free to open a feature request for this!
>
>
> Will do.
>
>
>> Similarly, one could allow "with type t :=" constraints in addition to
>> "with type t =".  Is there a need for that?
>
>
> I haven't seen one yet, but I'll keep my eyes out.
>
>
>>  One could also relax equality of package types (module S1 with ...) and
>> (module S2 with ...) by checking that S1 and S2 expand to structurally
>> equivalent module types (with the exact same ordering between value
>> components!).
>>
>
> Would that replace the dependence on paths that you describe above?  The
> use of paths has turned out to be pretty fragile in my experience, with
> module types that should have been the same showing up as different in the
> presence of rebinding of module signatures, which we would normally do as a
> way of improving concision and readability.
>
> y
>
>

[-- Attachment #2: Type: text/html, Size: 3740 bytes --]