Assuming I understand this syntax, the following currently valid type
definition would have two interpretations:

type 'a t = IntLit of 'a constraint 'a = int

One interpretation as a standard constrained ADT and one interpretation as a
GADT. We could use another token, other than constraint, for example:

type 'a t = IntLit of 'a : 'a = int

to which I have no objections. As you pointed out, though, the current
syntax is more concise.

cheers,
--Jacques

On Fri, Oct 29, 2010 at 10:32 AM, Dario Teixeira <darioteixeira@yahoo.com>wrote:

> Hi,
>
> > 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:
>
> I have a couple of questions regarding the syntax you've chosen for GADT
> declaration.  For reference, let's consider the first example you've
> provided:
>
> type _ t =
>  | IntLit : int -> int t
>  | BoolLit : bool -> bool t
>  | Pair : 'a t * 'b t -> ('a * 'b) t
>  | App : ('a -> 'b) t * 'a t -> 'b t
>  | Abs : ('a -> 'b) -> ('a -> 'b) t
>
>
> There's something "Haskellish" about this syntax, in the sense that type
> constructors are portrayed as being like functions.  While this does make
> sense in Haskell, in Ocaml it feels a bit out of place, because you cannot,
> for example, partially apply a type constructor.
>
> Also, note that in all the variant declarations the final token is 't'.
> Are there any circumstances at all where a GADT constructor will not end
> by referencing the type being defined?  If there are not, then this syntax
> imposes some syntactic salt into the GADT declaration.
>
> I know this is not the sole syntax that was considered for GADTs in Ocaml.
> Xavier Leroy's presentation in CUG 2008 shows a different one, which even
> though slightly more verbose, does have the advantage of being more
> "Camlish".
> Is there any shortcoming to the 2008 syntax that resulted in it being
> dropped
> in favour of this new one?
>
> Best regards,
> Dario Teixeira
>
>
>
>
>