Re: [Caml-list] PV-GADTs

[Jacques Le Normand <rathereasy@gmail.com>]

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 <darioteixeira@yahoo.com> 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
>