caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: "David Allsopp" <dra-news@metastack.com>
To: "'Oleg'" <oleg@okmij.org>, <francois.pottier@inria.fr>
Cc: <caml-list@inria.fr>
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$@metastack.com> (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:
> 
>         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


      parent reply	other threads:[~2020-10-07  8:11 UTC|newest]

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:05 ` [Caml-list] Question on the covariance of a GADT (polymorphic Oleg
2020-10-06 16:45   ` François Pottier
2020-10-06 19:04   ` Josh Berdine
2020-10-06 19:18     ` [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) François Pottier
2020-10-06 20:10       ` Josh Berdine
2020-10-07 13:17       ` [Caml-list] Question on the covariance of a GADT (polymorphic Oleg
2020-10-07 13:17     ` Oleg
2020-10-07  8:10   ` David Allsopp [this message]

Reply instructions:

You may reply publicly 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='000001d69c81$60341ab0$209c5010$@metastack.com' \
    --to=dra-news@metastack.com \
    --cc=caml-list@inria.fr \
    --cc=francois.pottier@inria.fr \
    --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

This inbox may be cloned and mirrored by anyone:

	git clone --mirror http://inbox.vuxu.org/caml-list
	git clone --mirror https://inbox.ocaml.org/caml-list

	# If you have public-inbox 1.1+ installed, you may
	# initialize and index your mirror using the following commands:
	public-inbox-init -V1 caml-list caml-list/ http://inbox.vuxu.org/caml-list \
		caml-list@inria.fr
	public-inbox-index caml-list

Example config snippet for mirrors.
Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.caml-list


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