[Caml-list] Narrowing a signature with a constrained type

[Caml-list] Narrowing a signature with a constrained type

[Philippe Veber]

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

Dear camlers,

Out of curiosity, I'd be happy to understand why the following definition
is rejected:

# module type T = sig type 'a format end;;
module type T = sig type 'a format end
# module F(X : T with type 'a format = 'a list constraint 'a = < .. >) =
struct end;;
File "", line 1, characters
13-67:
Error: In this `with' constraint, the new definition of format does not
match its original definition in the constrained
signature:
Type declarations do not match: type 'a format = 'a0 list is not included
in type 'a
format
       Their constraints differ.

Would it be unsound to allow it?

Cheers,

ph.

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

Re: [Caml-list] Narrowing a signature with a constrained type

[Jacques Garrigue]

On 2013/07/26, at 22:32, Philippe Veber <philippe.veber@gmail.com> wrote:

> Dear camlers,
> 
> Out of curiosity, I'd be happy to understand why the following definition is rejected:
> 
> # module type T = sig type 'a format end;;
> module type T = sig type 'a format end
> # module F(X : T with type 'a format = 'a list constraint 'a = < .. >) = struct end;;
> File "", line 1, characters 13-67:                                                                                           Error: In this `with' constraint, the new definition of format does not match its original definition in the constrained signature:                                  
> Type declarations do not match: type 'a format = 'a0 list is not included in type 'a format                                                            
>        Their constraints differ.
> 
> Would it be unsound to allow it?

Well, to ensure the coherence of the with constraints, we require that
the new signature be a subtype of the original one (as a module, not as an object).
This is where your code gets rejected.

Now why is it deemed unsafe to allow a constrained type definition to be a subtype of 
an unconstrained one?
Actually, I don't know.
The unconstrained type does not enforce the invariants of the constrained one,
but they will be checked as soon as you try to unify the two.
So it may be possible to lift this restriction.

However, there are technical difficulties in comparing a constrained definition
with an unconstrained one, so this might just be the main reason.
This would also have an impact on the invariants of types through abstraction.

Jacques

Re: [Caml-list] Narrowing a signature with a constrained type

[Philippe Veber]

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

Thanks for the explanation Jacques!

To be honest I was expecting the difficulty to lie in comparing two
constrained definitions (in my example, that would mean that type 'a format
would already be constrained and I'd be trying to narrow it further with
another constrained type). I thought the particular case where the original
type is unconstrained would be easier, but yeah, this is certainly more
difficult than it looks!

ph.


2013/7/27 Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>

> On 2013/07/26, at 22:32, Philippe Veber <philippe.veber@gmail.com> wrote:
>
> > Dear camlers,
> >
> > Out of curiosity, I'd be happy to understand why the following
> definition is rejected:
> >
> > # module type T = sig type 'a format end;;
> > module type T = sig type 'a format end
> > # module F(X : T with type 'a format = 'a list constraint 'a = < .. >) =
> struct end;;
> > File "", line 1, characters 13-67:
>                                                     Error: In this `with'
> constraint, the new definition of format does not match its original
> definition in the constrained signature:
> > Type declarations do not match: type 'a format = 'a0 list is not
> included in type 'a format
> >        Their constraints differ.
> >
> > Would it be unsound to allow it?
>
> Well, to ensure the coherence of the with constraints, we require that
> the new signature be a subtype of the original one (as a module, not as an
> object).
> This is where your code gets rejected.
>
> Now why is it deemed unsafe to allow a constrained type definition to be a
> subtype of
> an unconstrained one?
> Actually, I don't know.
> The unconstrained type does not enforce the invariants of the constrained
> one,
> but they will be checked as soon as you try to unify the two.
> So it may be possible to lift this restriction.
>
> However, there are technical difficulties in comparing a constrained
> definition
> with an unconstrained one, so this might just be the main reason.
> This would also have an impact on the invariants of types through
> abstraction.
>
> Jacques

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

Re: [Caml-list] Narrowing a signature with a constrained type

[Arnaud Spiwack]

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

>
> Well, to ensure the coherence of the with constraints, we require that
> the new signature be a subtype of the original one (as a module, not as an
> object).
> This is where your code gets rejected.
>
> Now why is it deemed unsafe to allow a constrained type definition to be a
> subtype of
> an unconstrained one?
> Actually, I don't know.
> The unconstrained type does not enforce the invariants of the constrained
> one,
> but they will be checked as soon as you try to unify the two.
> So it may be possible to lift this restriction.
>

It sounds pretty unlikely. If I have a functor taking a T in argument and I
pass it a T with constraints, it's likely to be inconsistent.

May I wonder, though, about the reason why T with blah should be a subtype
of T? I must confess I fail to see the point.


Arnaud

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