On Tue, Dec 13, 2011 at 11:35 PM, Dario Teixeira <[email protected]> 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
