On Sat, Dec 4, 2010 at 10:06 PM, Jacques Le Normand <rathere...@gmail.com> wrote: > in this case, yes, but if you have constraints then it is different. consider: > > type 'a term = > | Ignore of 'a : int term > | Embed of 'a > constraint 'a = int > > this is different from: > > type 'a term = > | Ignore of 'a : int term > | Embed of 'a : 'a term > constraint 'a = int > > (in fact, an error is flagged on the second one) > > Also, it can save the user some typing.
I don't think that it is very different. Standard-language constraints are outside of implications, so they apply to each branch. It already behaves this way in the standard language, basically restricting the type family to "int term". So I don't see why > | Embed of 'a : 'a term > constraint 'a = int shouldn't mean that Embed is "basically" Embed of int : int term. My position is that if a type variable should be treated as local to a branch, it should be explicitly quantified (using the dot notation, for example "Ignore of 'a. 'a : int term", without any exceptions to "existential" variables). And that the patterns type X = | Branch of Y and type X = | Branch of Y : X should be equivalent (where X could for example be 'a term). I would accept concessions to my general outlook on the grounds of being conservative over standard OCaml programmer intuitions and conciseness of code... when they apply... _______________________________________________ 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