caml-list - the Caml user's mailing list
 help / Atom feed
From: "David Allsopp" <>
To: "'Oleg'" <>, <>
Cc: <>
Subject: RE: [Caml-list] Question on the covariance of a GADT (polymorphic
Date: Wed, 7 Oct 2020 09:10:53 +0100
Message-ID: <000001d69c81$60341ab0$209c5010$> (raw)
In-Reply-To: <20201006160519.GA2217@Melchior.localnet>

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


      parent reply index

Thread overview: 9+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-10-06 11:57 [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) 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     ` [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) François Pottier
2020-10-06 20:11       ` 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 [this message]

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:

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

  git send-email \
    --in-reply-to='000001d69c81$60341ab0$209c5010$' \ \ \ \ \

* 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

AGPL code for this site: git clone public-inbox