RE: [Caml-list] Question on the covariance of a GADT (polymorphic

["David Allsopp" <dra-news@metastack.com>]

Oleg wrote:
> > type 'a t =
> >    | Wine: [> `Wine ] t
> >    | Food: [> `Food ] t
> >    | Box : 'a t * 'a t -> 'a t
> >    | Fridge: [< `Wine | `Food ] t -> [> `Fridge ] t
> >
> > In this definition, the type parameter 'a is a phantom parameter. It 
> > is not used to describe the type of a value; it is used only to 
> > restrict the set of values of type "t" that can be constructed.
> >
> > The goal here is to allow storing wine and food (and boxes 
> > containing boxes containing wine and food) in a fridge, but forbid 
> > storing a fridge in a fridge (or a fridge in a box in a fridge, etc.).
> 
> This is indeed a very `popular' problem. On June 21 this year Josh 
> Berdine posed almost the same question (without wine and food, alas).
> On 28 June 2020 I sent the reply with three solutions. Perhaps it 
> would be easier to point to the code, which also has many comments and
> explanations:
> 
>         http://okmij.org/ftp/tagless-final/subtyping.ml
> 
> The gist of the first two solutions is to exploit the fact that 
> tagless- final is sort of isomorphic to GADTs. That is, lots of things 
> that can be done with GADTs can be done without (or with GADTs hidden 
> away). That hiding has benefit of no longer bringing the problems with 
> variance. No GADTs (at least, not in the part facing the user), no 
> variance problems, at least, not for the end user. The library author 
> may use regular ADT, which are also non-problematic. A regular ADT 
> doesn't have the same typing guarantees -- but the typing is enforced 
> by the signature (at the module level), so there is no loss.
> 
> I was going to write an article for my web site explaining this and a 
> few earlier answers to the similar problems. Maybe I will eventually 
> get to it.

It is indeed popular - as are your historic answers, too :)
https://inbox.ocaml.org/caml-list/20130705102138.98516.qmail@www1.g3.pair.co
m/


--dra