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

["François Pottier" <francois.pottier@inria.fr>]

On 06/10/2020 at 21:04, Josh Berdine wrote:
 > Francois, your examples is way better than mine!:-)

Thanks :-)

As far as I understand Oleg's solutions, they all boil down to the same 
idea,
which I have considered, but is only half satisfactory: that is, to 
publish a
covariant abstract type +'a t which internally is implemented as an
abbreviation for an unparameterized type u. (See the food/wine/fridge 
example,
rewritten in this style, below.)

As far as the user is concerned, this works: the relaxed value restriction
works, so in my example, "meat" receives a polymorphic type, and I am happy.

The reason why this solution is only half satisfactory is that inside the
abstraction barrier, we have an unparameterized type u that does not express
the desired data invariant, so we cannot exploit the invariant to prove that
certain branches in the code are dead.

Also, the user cannot perform case analysis, since the type 'a t is 
abstract.
This is not a problem for me, but could be a problem in other situations.

Certainly, this is better than nothing, so I may end up adopting this 
approach
(thanks again Oleg!).

I am still curious, though, to know why my original type +'a t is not
recognized as covariant by the OCaml type-checker...

--
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

module T : sig

   type +'a t

   val wine: [> `Wine ] t
   val food: [> `Food ] t
   val box: 'a t * 'a t -> 'a t
   val fridge: [< `Wine | `Food ] t -> [> `Fridge ] t

end = struct

   type u =
     | Wine: u
     | Food: u
     | Box : u * u -> u
     | Fridge: u -> u

   type 'a t = u

   let wine = Wine
   let food = Food
   let box (t1, t2) = Box (t1, t2)
   let fridge t = Fridge t

end

open T

let food() = food
let meat = food()              (* the relaxed value restriction works *)
let _ = box(meat, fridge wine) (* place the meat beside a fridge *)
let _ = fridge meat            (* meat can still be put into fridge *)