caml-list - the Caml user's mailing list
 help / 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 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 ` 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: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

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

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