Re: [Caml-list] GADT constructor syntax

[bluestorm <bluestorm.dylc@gmail.com>]

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

I'm not sure I see the point of this long discussion between Lukasz and
Jacques.

It seems everybody agree that it is a good idea to explicitely quantify the
constructor-specific type variables.

The question Jacques raised is wether, when we write (| Foo of 'a . S : T)
or (| Foo : 'a . S -> T), the 'a is quantified on S only, or on both S and
T.

It think we all agree that, for semantical reasons, quantification should be
scoped over both S and T. However, the (of S : T) syntax does not make it
very obvious, and this should be rightfully considered as a defect of this
syntax.

I'm under the impression that your intense debate is about the edge case
where :
1. we don't use explicit quantification of constructor-specific variables
2. we reuse the type parameter variables in the type of a GADT constructor
(so they're implicitly shadowed by the implicit quantifications, or maybe
not)

If we reject possibly 1. (and ask for explicit quantification), all is well.
If you want to consider option 1., then I think the edge case 2. is evil and
shoud result in a warning.


On Sun, Dec 5, 2010 at 9:25 AM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:

> On Sun, Dec 5, 2010 at 9:10 AM, Lukasz Stafiniak <lukstafi@gmail.com>
> wrote:
> >
> > shouldn't mean that Embed is "basically" Embed of int : int term. My
> > position is that if a type variable should be treated as local to a
> > branch, it should be explicitly quantified (using the dot notation,
> > for example "Ignore of 'a. 'a : int term", without any exceptions to
> > "existential" variables). And that the patterns
> >
> > type X =
> >  | Branch of Y
> >
> > and
> >
> > type X =
> >  | Branch of Y : X
> >
> > should be equivalent (where X could for example be 'a term).
>
> To clarify again: modulo variable capture! That is, the pattern
>
> > type X =
> >  | Branch of 'a. Y : X
>
> will be different (unless 'a is not used in Y nor X).
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> 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: 3263 bytes --]