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