From: Oleg <firstname.lastname@example.org> To: email@example.com Cc: firstname.lastname@example.org 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: <email@example.com> > 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.
next prev 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 ` 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 \ --firstname.lastname@example.org \ --email@example.com \ --firstname.lastname@example.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