see below On Sat, Dec 4, 2010 at 2:41 PM, Lukasz Stafiniak <lukst...@gmail.com> wrote: > 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
having type 'a t = Foo of 'a : 'b t creating a constructor of type forall 'a. 'a -> 'a t is really confusing since the user explicitly gave the return type of the constructor as 'b 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
