caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Oleg <oleg@okmij.org>
To: 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 01:05:19 +0900
Message-ID: <20201006160519.GA2217@Melchior.localnet> (raw)
In-Reply-To: <29c64a17-6bda-89eb-49c9-e986116d8e70@inria.fr>



> 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.


  reply	other threads:[~2020-10-06 16:01 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 ` Oleg [this message]
2020-10-06 16:45   ` [Caml-list] Question on the covariance of a GADT (polymorphic 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

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=20201006160519.GA2217@Melchior.localnet \
    --to=oleg@okmij.org \
    --cc=caml-list@inria.fr \
    --cc=francois.pottier@inria.fr \
    /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