caml-list - the Caml user's mailing list
 help / Atom feed
From: François Pottier <francois.pottier@inria.fr>
To: Josh Berdine <josh@berdine.net>, Oleg <oleg@okmij.org>
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] Question on the covariance of a GADT (polymorphic variants involved)
Date: Tue, 6 Oct 2020 21:18:44 +0200
Message-ID: <c98df8d5-6288-25fe-aa7a-61928096395f@inria.fr> (raw)
In-Reply-To: <FEA35C98-1E7A-402E-9B5D-9585371E4009@berdine.net>


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 *)

  reply index

Thread overview: 9+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-10-06 11:57 François Pottier
2020-10-06 16:01 ` [Caml-list] Question on the covariance of a GADT (polymorphic Oleg
2020-10-06 16:45   ` François Pottier
2020-10-06 19:05   ` Josh Berdine
2020-10-06 19:19     ` François Pottier [this message]
2020-10-06 20:11       ` [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) Josh Berdine
2020-10-07 13:13       ` [Caml-list] Question on the covariance of a GADT (polymorphic Oleg
2020-10-07 13:13     ` Oleg
2020-10-07  8:11   ` David Allsopp

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=c98df8d5-6288-25fe-aa7a-61928096395f@inria.fr \
    --to=francois.pottier@inria.fr \
    --cc=caml-list@inria.fr \
    --cc=josh@berdine.net \
    --cc=oleg@okmij.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

caml-list - the Caml user's mailing list

Archives are clonable: git clone --mirror https://inbox.ocaml.org/caml-list

AGPL code for this site: git clone https://public-inbox.org/ public-inbox