caml-list - the Caml user's mailing list
 help / Atom feed
From: Oleg <>
Subject: Re: [Caml-list] Question on the covariance of a GADT (polymorphic
Date: Wed, 7 Oct 2020 22:17:32 +0900
Message-ID: <20201007131732.GA4915@Melchior.localnet> (raw)
In-Reply-To: <>

> As far as I understand Oleg's solutions, they all boil down to the
> same idea, which I have considered, but is only half satisfactory:
> that is, to publish a covariant abstract type +'a t which internally
> is implemented as an abbreviation for an unparameterized type u. (See
> the food/wine/fridge example, rewritten in this style, below.)
Good summary!

> The reason why this solution is only half satisfactory is that inside the
> abstraction barrier, we have an unparameterized type u that does not express
> the desired data invariant, so we cannot exploit the invariant to prove that
> certain branches in the code are dead.

Indeed. That was the `imperfection' that I have referred to in my
message. I have two comments: first, there is the second solution,
which does exploit the invariant. Second, there may be more than one
abstraction barrier... That is, many implementations of the wine_food
signature may be in terms of some `more basic' signature -- or just
the same signature, if we are talking about term transformations (as I
have just replied to Josh Berdine).  Eventually we have to implement
the `most basic signature', and indeed we have to drop the indices and
fall into the `untyped' universe, so to speak. One hopes though that
this `security kernel' is really `most basic' and its operations are
few and primitive, so the correctness could be relatively easily

> Also, the user cannot perform case analysis, since the type 'a t is
> abstract.  This is not a problem for me, but could be a problem in
> other situations.

When I first mentioned tagless-final, in passing at a some conference
in Oxford a decade ago, an old Oxford professor (one of fathers of
SML) exclaimed: ``Isn't it bloody obvious that you cannot do
pattern-matching in this style!?''. I liked his phrase. Now I like to
say that pattern-matching in tagless-final style is not bloody, is not
obvious and is not impossible.

That it is always possible was proven by Boehm and Berarducci (their
proof was one inspiration for the development of Coq, as I heard).
Although their general method works always, often one may design
simpler methods for particular pattern-matching tasks.

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

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20201007131732.GA4915@Melchior.localnet \ \ \ \

* 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

AGPL code for this site: git clone public-inbox