Re: [Caml-list] Generalized Algebraic Datatypes

[Dario Teixeira <darioteixeira@yahoo.com>]

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