Re: [Caml-list] Question on the covariance of a GADT (polymorphic variants involved)

[Josh Berdine <josh@berdine.net>]

> On Oct 6, 2020, at 8:18 PM, François Pottier <francois.pottier@inria.fr> wrote:
> 
> I am still curious, though, to know why my original type +'a t is not
> recognized as covariant by the OCaml type-checker...

Jacques helpfully gave a precise answer earlier:

> On Jun 22, 2020, at 8:39 AM, Jacques Garrigue <jacques.garrigue@gmail.com> wrote:
> 
> The best I can say is that this combination of GADTs and polymorphic variants is not supported.
> There are actually two distinct problems:
> * GADT indices must be invariant
> * refinement of row types (both polymorphic variants and object types) is only partially supported
>  (you can instantiate an existential row only once)
> 
> So I wouldn’t suggest investing time in trying to outsmart the type system in this direction.
> The best you could achieve would be discovering a soundness bug (which should of course be promptly reported).
> 
> If your goal is just to move the polymorphism from the type itself to its parameter, using normal phantom types (maybe combined with phantom types to allow pattern matching) could help you, even if it may leave a few runtime checks.
> 
> Otherwise, you may try to encode your domain in a proper GADT, not using polymorphic variants.
> There are ways to keep some degree of subsumption.
> 
> By the way, I’m not sure what you mean by “weaker exhaustiveness” of polymorphic variants.
> I agree that polymorphic variants give weaker typing, it that they infer the declarations, but at least closed pattern-mathcing on them do guarantee exhaustiveness.

Jacques, I am sorry that I failed to address this before. I did not mean to imply that there was a problem, by "weaker exhaustiveness" I only mean that for a pattern match that is missing an intended case, the type error involving the inferred type can end up "far away" from the point of the mistake in the code. One way around this is to add type more annotations so that an incompatibility cannot propagate as far. But this relies on programmer-discipline rather than being irrefutably enforced by the type system.

Cheers, Josh


> Jacques
> 
> P.S. Here is an example of specific domain encoding:
> 
> type ‘a number = Number of ‘a
> 
> type _ exp =
> | Integer : int -> int number exp
> | Float : float -> float number exp
> | Add : ‘a number exp * ‘a number exp -> ‘a number exp
> | String : string -> string exp
> 
> or
> 
> type number = Number
> 
> type _ exp =
> | Integer : int -> number exp
> | Float : float -> number exp
> | Add : number exp * number exp -> number exp
> | String : string -> string exp
> 
> Basically, you must choose between what is static and what is dynamic.
> 
> On 21 Jun 2020, at 18:10, Josh Berdine <josh@berdine.net> wrote:
>> 
>> I wonder if anyone has any suggestions on approaches to use GADTs with a type parameter that is phantom and allows subtyping.
>> 
>> (My understanding is that the approach described in 
>> "Gabriel Scherer, Didier Rémy. GADTs meet subtyping. ESOP 2013"
>> hasn't entirely been settled on as something that ought to be implemented in the compiler. Right? Is there anything more recent describing alternatives, concerns or limitations, etc.?)
>> 
>> As a concrete example, consider something like:
>> ```
>> type _ exp =
>> | Integer : int -> [> `Integer] exp
>> | Float : float -> [> `Float] exp
>> | Add : ([< `Integer | `Float] as 'n) exp * 'n exp -> 'n exp
>> | String : string -> [> `String] exp
>> ```
>> The intent here is to use polymorphic variants to represent a small (upper semi-) lattice, where basically each point corresponds to a subset of the constructors. The type definition above is admitted, but while the index types allow subtyping:
>> ```
>> let widen_index x = (x : [`Integer] :> [> `Integer | `Float])
>> ```
>> this does not extend to the base type:
>> ```
>> # let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);;
>> Line 1, characters 18-67:
>> 1 | let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);;
>>                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>> Error: Type [ `Integer ] exp is not a subtype of
>>        ([> `Float | `Integer ] as 'a) exp 
>>      The first variant type does not allow tag(s) `Float
>> 
>> ```
>> This makes sense since `type _ exp` is not covariant. But trying to declare it to be covariant doesn't fly, yielding:
>> ```
>> Error: In this GADT definition, the variance of some parameter
>>      cannot be checked
>> ```
>> 
>> I'm not wedded to using polymorphic variants here, but I have essentially the same trouble using a hierarchy of class types (with different sets of `unit` methods to induce the intended subtype relation) to express the index lattice. Are there other options?
>> 
>> I also tried using trunk's injectivity annotations (`type +!_ exp = ...`) on a lark since I'm not confident that I fully understand what happens to the anonymous type variables for the rows in the polymorphic variants. But that doesn't seem to change things.
>> 
>> Is this sort of use case something for which there are known encodings? In a way I'm trying to benefit from some of the advantages of polymorphic variants (subtyping) without the drawbacks such as weaker exhaustiveness and less compact memory representation by keeping the polymorphic variants in a phantom index. Is this approach doomed?
>> 
>> Cheers, Josh
>> 
>