Hi! Just a quick answer for now. On Sat, Dec 4, 2010 at 8:25 PM, Jacques Le Normand <rathere...@gmail.com> wrote: > Dear caml-list, > I would like to start a constructive discussion on the syntax of GADT > constructors of the ocaml gadt branch, which can be found at: > > https://sites.google.com/site/ocamlgadt/ > > There are two separate issues: > > 1) general constructor form > > option a) > > type _ t = > TrueLit : bool t > | IntLit of int : int lit > > option b) > > type _ t = > TrueLit : bool t > | IntLit : int -> int lit > > I'm open to other options. The branch has used option b) from the > start, but I've just switched to option a) to see what it's like
I like option (a) for consistency with the existing OCaml syntax, and while I like option (b) for its conformance to standard notation, I don't like your reasons for liking (b) ;-) > I slightly prefer option b), because it makes it clear that it's a > gadt constructor right from the start. This is useful because the type > variables in gadt constructors are independent of the type parameters > of the type, consider: > > type 'a t = Foo of 'a : 'b t > > this, counter intuitively, creates a constructor Foo of type forall 'd > 'e. 'd t -> 'e t. I think that the scope should propagate, i.e. that somehow the 'a should really be bound, giving Foo : forall 'a . 'a t -> 'a t > 2) explicit quantification of existential variables I don't even like the problem formulation. I think that existential variables should not be differentiated from universal variables. (So I think I like what you don't like about the Haskell solution). > > option a) > > leave existential variables implicitly quantified. For example: > > type _ u = Bar of 'a t : u > or > type _ u = Bar : 'a t -> u > > option b) > > specifically quantify existential variables. For example: > > type _ u = Bar of 'a. 'a t : u > or > type _ u = Bar : 'a. 'a t -> u > > Currently, the branch uses option a). For me, it is a question for _all_ variables whether be implicitly or explicitly quantified... > I) the scope of the explicitly quantified variable is not clear. For > example, how do you interpret: > > type _ u = Bar of 'a. 'a : 'a t > or > type _ u = Bar : 'a. 'a -> 'a t > > In one interpretation bar has type forall 'a 'b. 'a -> 'b t and in > another interpretation it has type forall 'a. 'a -> 'a t. Of course the "forall 'a. 'a -> 'a t" as far as I'm concerned! > II) > > In the example of option b), the 'a variable is quantified as a > universal variable but, in patterns, it is used as an existential > variable. This is something I found very confusing in Haskell where > they actually use the 'forall' keyword. It often happens in logic! You have two sides of the turnstyle... I'm sorry if I sounded harsh, not my intention! Best Regards. _______________________________________________ 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
