Re: [Caml-list] GADTs and parsers

[Gabriel Scherer <gabriel.scherer@gmail.com>]

> In this case the use of polymorphic variants for the type parameter comes
> in handy because there is a subtyping relation and the [> ] declaration
> allows for useful mixing

Precisely, your example does *not* use subtyping (it's easy to see: in
OCaml, subtyping is explicit, you have to use (e :> t) casts. If there
are none, you're not using subtyping). [> `Link ] is actually a
shortcut for something like [ `Link | 'r ], where 'r is a polymorphic
row variable that stands for any number of additional cases. So going
from [> `Link ] to [> `Link | `Nolink ] is not subtyping, only
instantiation of 'r into (`Nolink | 'r2) for a fresh 'r2.

So it may be the case that your previous example also could work with
the parameter invariant. I haven't looked at it deeply enough to tell.

On Sun, Jul 15, 2012 at 11:58 AM, Dario Teixeira
<darioteixeira@yahoo.com> wrote:
> Hi,
>
> And thanks for the prompt reply!
>
>> I suspect the problem may be one of variance: you are using
>
>> polymorphic variants, but implicitly assuming that ([ `Nolink ]
>> inline_t) is a subtype of ([ `Nolink | `Link ] inline_t), which means
>> that "inline_t" is covariant in its first parameter. However, variance
>> of GADTs is currently very strict, and your inline_t definition is in
>> fact considered invariant (to check that, replace "type _ inline_t" by
>> "type (+'a) inline_t" and watch the error), so this conversion does
>> not pass. On the contrary, with a phantom type definition, the
>> parameter is inferred to be irrelevant (any variance is accepted), so
>> you can do whatever you want inside the abstraction boundary.
>
> Ah, indeed.  And on a related note: is there a way to get the compiler
> to spill out the variance it infers?  I'm assuming that 'ocamlc -i' does
> not include inferred variance because it is generally "obvious" and
> not something you usually have to worry about unless you want to
> make a type abstract.  However, in a case like this it would help.
> (Or does the compiler *always* assume invariance with GADTs?)
>
>
>> (For more information on GADTs and variance, see the previous thread
>> on this on the mailing-list; the summary is that it's complicated, but
>> I still hope we could get something finer in the future. It would
>> probably not work with polymorphic variant instances, anyway.)
>
> In this case the use of polymorphic variants for the type parameter comes
> in handy because there is a subtyping relation and the [> ] declaration
> allows for useful mixing:
>
> # let x1 = Text "ola";;
> val x1 : [> `Nonlink ] inline_t = Text "ola"
>
> # let x2 = Link "lnk";;
> val x2 : [> `Link ] inline_t = Link "lnk"
>
> # let xs = [x1; x2];;
> val xs : [> `Link | `Nonlink ] inline_t list = [Text "ola"; Link "lnk"]
>
> Cheers,
> Dario