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

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

[Yaron Minsky]

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

For some reason, 1st-class modules have more restrictive "with" syntax,
which turns out to be a practical problem.

The main constraint is that with constraints do not seem to be able to refer
to sub-modules.  Consider the following code snippet:

>     module type Foo = sig type t end
>     module type Bar = sig module Foo : Foo end
>
>     (* compiles *)
>     let g (type a) (m : (module Foo with type t = a)) = ()
>
>     (* fails to compile with a syntax error *)
>     let f (type a) (m : (module Bar with type Foo.t = a)) = ()

Of course, ordinary modules have no such constraint.  Any thoughts as to
what is going on here, and whether it can be fixed?  This has really
restricted designs I've been using, forcing me to flatten out structures
that are more naturally nested.

y

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

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

[Jacques Le Normand]

first post! let's see if anyone can do better...

module type Foo = sig type t end
module type Bar = sig type foo_t module Foo : Foo type t = foo_t   end

      (* compiles *)
let g (type a) (m : (module Foo with type t = a)) = ()

    (* fails to compile with a syntax error *)
let f (type a) (m : (module Bar with type foo_t = a)) = ()


On Tue, Sep 20, 2011 at 3:36 AM, Yaron Minsky <yminsky@gmail.com> wrote:
> For some reason, 1st-class modules have more restrictive "with" syntax,
> which turns out to be a practical problem.
>
> The main constraint is that with constraints do not seem to be able to refer
> to sub-modules.  Consider the following code snippet:
>
>>     module type Foo = sig type t end
>>     module type Bar = sig module Foo : Foo end
>>
>>     (* compiles *)
>>     let g (type a) (m : (module Foo with type t = a)) = ()
>>
>>     (* fails to compile with a syntax error *)
>>     let f (type a) (m : (module Bar with type Foo.t = a)) = ()
>
> Of course, ordinary modules have no such constraint.  Any thoughts as to
> what is going on here, and whether it can be fixed?  This has really
> restricted designs I've been using, forcing me to flatten out structures
> that are more naturally nested.
>
> y
>

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

[Yaron Minsky]

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

I agree this works around the limitation, but it does beg the question: why
is the limitation there in the first place?

On Tue, Sep 20, 2011 at 4:00 PM, Jacques Le Normand <rathereasy@gmail.com>wrote:

> first post! let's see if anyone can do better...
>
> module type Foo = sig type t end
> module type Bar = sig type foo_t module Foo : Foo type t = foo_t   end
>
>      (* compiles *)
> let g (type a) (m : (module Foo with type t = a)) = ()
>
>    (* fails to compile with a syntax error *)
> let f (type a) (m : (module Bar with type foo_t = a)) = ()
>
>
> On Tue, Sep 20, 2011 at 3:36 AM, Yaron Minsky <yminsky@gmail.com> wrote:
> > For some reason, 1st-class modules have more restrictive "with" syntax,
> > which turns out to be a practical problem.
> >
> > The main constraint is that with constraints do not seem to be able to
> refer
> > to sub-modules.  Consider the following code snippet:
> >
> >>     module type Foo = sig type t end
> >>     module type Bar = sig module Foo : Foo end
> >>
> >>     (* compiles *)
> >>     let g (type a) (m : (module Foo with type t = a)) = ()
> >>
> >>     (* fails to compile with a syntax error *)
> >>     let f (type a) (m : (module Bar with type Foo.t = a)) = ()
> >
> > Of course, ordinary modules have no such constraint.  Any thoughts as to
> > what is going on here, and whether it can be fixed?  This has really
> > restricted designs I've been using, forcing me to flatten out structures
> > that are more naturally nested.
> >
> > y
> >
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

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

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

[Alain Frisch]

On 09/20/2011 03:36 AM, Yaron Minsky wrote:
> For some reason, 1st-class modules have more restrictive "with" syntax,
> which turns out to be a practical problem.
>
> The main constraint is that with constraints do not seem to be able to
> refer to sub-modules.  Consider the following code snippet:
>
>>      module type Foo = sig type t end
>>      module type Bar = sig module Foo : Foo end
>>
>>      (* compiles *)
>>      let g (type a) (m : (module Foo with type t = a)) = ()
>>
>>      (* fails to compile with a syntax error *)
>>      let f (type a) (m : (module Bar with type Foo.t = a)) = ()
>
> Of course, ordinary modules have no such constraint.  Any thoughts as to
> what is going on here, and whether it can be fixed?

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! 
Similarly, one could allow "with type t :=" constraints in addition to 
"with type t =".  Is there a need for that?  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!).



-- Alain

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

[Jacques Le Normand]

For all of you wondering how unification works with package types:

(module Foo with type t1 = tau1 and type t2 = tau2 and ... and tn =
taun) unifies with (module Foo' with type t1' = tau1' and type t2' =
tau2' and ... and tn' = taun')

if and only if

n = n' and Foo = Foo' and t1 = t1'  and t2 = t2' and ... and tau1
unifies with tau1' and tau2 unifies with tau2' ...
and t1...tn are all abstract types in Foo

Right now t1...tn are all strings, but they might as well be paths
(which would give the behaviour you need)



On Tue, Sep 20, 2011 at 11:03 AM, Alain Frisch <alain.frisch@lexifi.com> wrote:
> On 09/20/2011 03:36 AM, Yaron Minsky wrote:
>>
>> For some reason, 1st-class modules have more restrictive "with" syntax,
>> which turns out to be a practical problem.
>>
>> The main constraint is that with constraints do not seem to be able to
>> refer to sub-modules.  Consider the following code snippet:
>>
>>>     module type Foo = sig type t end
>>>     module type Bar = sig module Foo : Foo end
>>>
>>>     (* compiles *)
>>>     let g (type a) (m : (module Foo with type t = a)) = ()
>>>
>>>     (* fails to compile with a syntax error *)
>>>     let f (type a) (m : (module Bar with type Foo.t = a)) = ()
>>
>> Of course, ordinary modules have no such constraint.  Any thoughts as to
>> what is going on here, and whether it can be fixed?
>
> 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! Similarly,
> one could allow "with type t :=" constraints in addition to "with type t =".
>  Is there a need for that?  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!).
>
>
>
> -- Alain
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

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

[Yaron Minsky]

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

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: 3091 bytes --]

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

[Yaron Minsky]

[-- 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 --]