It's very interesting.

First, I'm curious of the "historical" aspects of this work : where does it
come from ? Apparently there is work from you and Jacques Garrigue, but it's
hard to tell. Is it new, or a long-running experiment ?

In your "intuition" section (btw. there is a typo here, it should be (type
s) (x : s t)), you seem to present GADT as directly related to the new (type
s) construct. It's a bit surprising because it's difficult to know the
difference between this and classic type variables. I suppose it is because
only (type s) guarantee that the variable remains polymorphic, and you use
that to ensure that branch-local unifications don't "escape" to the outer
level ? Could you be a bit more explicit on this ?

It's also a bit difficult to know what's the big deal about "exhaustiveness
checks". As I understand it, you remark that with GADTs some case cannot
happen due to typing reasons, but the exhaustive check doesn't know about
it. Could you be a bit more explicit about what the exhaustiveness checker
does :
- is it exactly the same behavior as before, ignoring GADT specificities ?
(ie. you haven't changed anything)
- if not, what have you changed and how can we try to predict its reaction
to a given code ?
- what can we do when it doesn't detect an impossible case ? I suppose we
can't a pattern clause for it, as the type checker would reject it.

I'm not sure I understand the example of the "Variance" section.
Why is the cast in that direction ? It seems to me that even if we could
force t to be covariant, this cast (to a less general type) shouldn't work :

  # type +'a t = T of 'a;;
  # let a = T (object method a = 1 end);;
  # (a :> < m : int; n : bool > t);;
  Error: Type < a : int > t is not a subtype of < m : int; n : bool > t

Again, you "Objects and variants" and "Propagation" subsections are a bit
vague. Could you give example of code exhibiting possible problems ?

Finally, a few syntax trolls, in decreasing order of constructivity :

- is it a good idea to reproduce the "implicit quantification" of ordinary
types ? It seems it could be particularly dangerous here.
  for example, changing
    type _ t = Id : 'a -> 'a t
  to
    type 'a t = Id : 'a -> 'a t | Foo of 'a
  introduce, if I'm not mistaken, a semantic-changing variable captures.
  (I thought other dark corners of the type declarations already had this
behavior, but right now I can't remember which ones)

- if I understand it correctly, (type a . a t -> a) is yet another syntax
for type quantification. Why ? I thought (type a) was used to force
generalization, but ('a . ...)-style annotation already force polymorphism
(or don't they ?). Is it a semantic difference with ('a . 'a t -> 'a), other
than its interaction with gadts ? Can we use (type a . a t -> a) in all
places where we used ('a . 'a t -> 'a) before ?

- is there a rationale for choosing Coq-style variant syntax instead of just
adding a blurb to the existing syntax, such as
    | IntLit of int : int t
  or
    | IntList of int return int t
  ?


Thanks.

On Mon, Oct 25, 2010 at 10:39 AM, Jacques Le Normand <rathereasy@gmail.com>
 wrote:

> Dear Caml list,
>
> I am pleased to announce an experimental branch of the O'Caml compiler:
> O'Caml extended with Generalized Algebraic Datatypes. You can find more
> information on this webpage:
>
> https://sites.google.com/site/ocamlgadt/
>
>
> And you can grab the latest release here:
>
> svn checkout https://yquem.inria.fr/caml/svn/ocaml/branches/gadts
>
>
>
> Any feedback would be very much appreciated.
>
> Sincerely,
>
> Jacques Le Normand
>
>
> _______________________________________________
> 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
>
>