caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: "François Pottier" <francois.pottier@inria.fr>
To: OCaML Mailing List <caml-list@inria.fr>
Subject: [Caml-list] Question on the covariance of a GADT (polymorphic variants involved)
Date: Tue, 6 Oct 2020 13:57:05 +0200
Message-ID: <29c64a17-6bda-89eb-49c9-e986116d8e70@inria.fr> (raw)


Dear all,

I have a problem convincing OCaml that a GADT is covariant in one of its
parameters.

Here is a simplified version of what I am trying to do:

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

The lower bounds >`Wine and >`Food and >`Fridge are used to keep track 
of the
basic objects that are (transitively) contained in a box. The Box 
constructor
takes the conjunction of these lower bounds. The Fridge constructor imposes
the upper bound <`Wine|`Food, thereby forbidding a fridge to appear
(transitively) inside a fridge.

You may be wondering why I am using an algebraic data type whose index is
constrained by abusing polymorphic variants, instead of using polymorphic
variants directly. The answer is that is the real type definition I am 
working
with is more complex than this: it has more parameters and it is actually a
(real) GADT in these other parameters, so (I think) I cannot turn it into a
polymorphic variant.

Now, the problem is, the OCaml type-checker does not recognize that the type
'a t is covariant in 'a.

Intuitively, it seems clear that this type is covariant in 'a: the
constructors Wine, Food, Fridge impose lower bounds on 'a only, and the
constructor Box uses 'a in a covariant position (if one admits, inductively,
that 'a t is covariant in 'a).

I would like OCaml to accept the fact that t is covariant in 'a because 
I have
several functions (smart constructors) that produce values of type 'a t. 
When
an application of such a function produces a result of type _'a t, I would
like it to be generalized, so as to obtain 'a t. Currently, this does not
work.

This lack of generalization is not just a minor inconvenience. It leads to
pollution (that is, lower bounds and upper bounds bearing on the same type
variable, when they should normally bear on two distinct type 
variables). For
instance, if an object whose type has not been generalized is once placed
*beside* a fridge, then it can no longer be put *inside* a fridge:

   let food() = Food
   let meat = food()              (* weak type variable appears *)
   let _ = Box(meat, Fridge Wine) (* place the meat beside a fridge *)
   let _ = Fridge meat            (* meat can no longer be put into 
fridge *)
                  ^^^^
Error: This expression has type [> `Food | `Fridge ] t
        but an expression was expected of type [< `Food | `Wine ] t
        The second variant type does not allow tag(s) `Fridge

An explanation of why OCaml cannot recognize that this type is 
covariant, or a
suggestion of a workaround, would be very much appreciated. Thanks!

--
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

             reply	other threads:[~2020-10-06 11:57 UTC|newest]

Thread overview: 9+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-10-06 11:57 François Pottier [this message]
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

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=29c64a17-6bda-89eb-49c9-e986116d8e70@inria.fr \
    --to=francois.pottier@inria.fr \
    --cc=caml-list@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