Re: [Caml-list] PV-GADTs
On Tue, Dec 13, 2011 at 21:56, Jacques Garrigue wrote: > In your example, how do you know in a pattern-matching that `Foo comes from > t2? > Type inference could be used, but I'm afraid it would be very fragile, > and not easy to use. > So at this point there is no plan to add GADT PVs. > > An alternative design would be to have extensible GADTs, where you would be > able > to add new cases, like for exn. > I think this would be useful, and cover some uses that are not > possible even with PVs. I really like using PVs for defining extensible, recursive DSLs. If it were possible to use GADTs in a similar way, that would be an awesome feature. But I wonder how this could be done cleanly. I agree that type inference would be impractical when combining PVs and GADTs, since PV constructors are not tied to a specific type. It seems you have something in particular in mind when you speak of extensible GADTs. Wouldn't such a feature require that GADTs have the same runtime representation as PVs, i.e. using the hash value of the variant name? Not sure what the GADT representation is right now anyway, but maybe this should be determined carefully before the next release if we want to add extensibility later. Regards, Markus -- Markus Mottl http://www.ocaml.info markus.mo...@gmail.com -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] PV-GADTs
On Tue, Dec 13, 2011 at 11:35 PM, Dario Teixeira wrote: > Hi, > I wonder, is there any theoretical reason why GADTs cannot be associated with > polymorphic variants? As an example, consider the two type declarations > below. > The first is your run-of-the-mill GADT, supported by the current SVN trunk. > The > second is a PV-GADT, which is not accepted. But is this just a present > limitation > or a fundamental one? > > type _ t1 = Foo: int t1 | Bar: float t1 > > type _ t2 = [ `Foo: int t2 | `Bar: float t2 ] Actually, Jacques Le Normand didn't directly answer your question. He just explained why we cannot currently combine polymorphic variants and GADTs in the same pattern-matching. This could be improved if the need is clear. However what you are asking for is different: you want indexed polymorphic variants. But there the problem is more fundamental. The strength of polymorphic variants is that you don't have to define them. But if you don't relate the constructors to a specific type, there is no way you can constrain the index. In your example, how do you know in a pattern-matching that `Foo comes from t2? Type inference could be used, but I'm afraid it would be very fragile, and not easy to use. So at this point there is no plan to add GADT PVs. An alternative design would be to have extensible GADTs, where you would be able to add new cases, like for exn. I think this would be useful, and cover some uses that are not possible even with PVs. Jacques Garrigue -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] PV-GADTs
Hi, > The way GADTs are handled is that local constraints are generated when > patterns are typed and then those constraints are used in the body of > the associated clause. To generate the constraints, we need to > propagate typing information. From my understanding, we can't do this > with polymorphic variants because it would change the typing > algorithm. In other words, with polymorphic variants the type of the > pattern is infered independently of the context. > > From my understanding, Jacques Garrigue has good reasons to reject > propagation in such a case. Personally, I'd like to see a flag, say > -unsafepropagation, to let people use polymorphic variants and GADTs > at their own risk, knowing that the behaviour of the typing algorithm > may not satisfy some expected theoretical properties. Thanks for the clarification. Mind you, my question did not stem from any actual need for PV-GADTS; it was pure curiosity... Cheers, Dario -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] PV-GADTs
The way GADTs are handled is that local constraints are generated when patterns are typed and then those constraints are used in the body of the associated clause. To generate the constraints, we need to propagate typing information. From my understanding, we can't do this with polymorphic variants because it would change the typing algorithm. In other words, with polymorphic variants the type of the pattern is infered independently of the context. >From my understanding, Jacques Garrigue has good reasons to reject propagation in such a case. Personally, I'd like to see a flag, say -unsafepropagation, to let people use polymorphic variants and GADTs at their own risk, knowing that the behaviour of the typing algorithm may not satisfy some expected theoretical properties. On Tue, Dec 13, 2011 at 9:35 AM, Dario Teixeira wrote: > Hi, > I wonder, is there any theoretical reason why GADTs cannot be associated with > polymorphic variants? As an example, consider the two type declarations > below. > The first is your run-of-the-mill GADT, supported by the current SVN trunk. > The > second is a PV-GADT, which is not accepted. But is this just a present > limitation > or a fundamental one? > > type _ t1 = Foo: int t1 | Bar: float t1 > > type _ t2 = [ `Foo: int t2 | `Bar: float t2 ] > > > Thanks in advance for your input! > Cheers, > Dario Teixeira > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] PV-GADTs
Hi, I wonder, is there any theoretical reason why GADTs cannot be associated with polymorphic variants? As an example, consider the two type declarations below. The first is your run-of-the-mill GADT, supported by the current SVN trunk. The second is a PV-GADT, which is not accepted. But is this just a present limitation or a fundamental one? type _ t1 = Foo: int t1 | Bar: float t1 type _ t2 = [ `Foo: int t2 | `Bar: float t2 ] Thanks in advance for your input! Cheers, Dario Teixeira -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
