```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/
```

```next             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,

Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

switches of git-send-email(1):

git send-email \
--to=francois.pottier@inria.fr \
--cc=caml-list@inria.fr \

https://kernel.org/pub/software/scm/git/docs/git-send-email.html

```

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