Re: [Caml-list] Question on the covariance of a GADT (polymorphic

[Oleg <oleg@okmij.org>]

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

> 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). 
        http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html
Although their general method works always, often one may design
simpler methods for particular pattern-matching tasks.