caml-list - the Caml user's mailing list
 help / Atom feed
From: Josh Berdine <>
To: caml-list <>
Subject: [Caml-list] Subtyping of phantom GADT indices?
Date: Sun, 21 Jun 2020 17:10:26 +0100
Message-ID: <> (raw)

I wonder if anyone has any suggestions on approaches to use GADTs with a type parameter that is phantom and allows subtyping.

(My understanding is that the approach described in 
"Gabriel Scherer, Didier Rémy. GADTs meet subtyping. ESOP 2013"
hasn't entirely been settled on as something that ought to be implemented in the compiler. Right? Is there anything more recent describing alternatives, concerns or limitations, etc.?)

As a concrete example, consider something like:
type _ exp =
  | Integer : int -> [> `Integer] exp
  | Float : float -> [> `Float] exp
  | Add : ([< `Integer | `Float] as 'n) exp * 'n exp -> 'n exp
  | String : string -> [> `String] exp
The intent here is to use polymorphic variants to represent a small (upper semi-) lattice, where basically each point corresponds to a subset of the constructors. The type definition above is admitted, but while the index types allow subtyping:
let widen_index x = (x : [`Integer] :> [> `Integer | `Float])
this does not extend to the base type:
# let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);;
Line 1, characters 18-67:
1 | let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);;
Error: Type [ `Integer ] exp is not a subtype of
         ([> `Float | `Integer ] as 'a) exp 
       The first variant type does not allow tag(s) `Float

This makes sense since `type _ exp` is not covariant. But trying to declare it to be covariant doesn't fly, yielding:
Error: In this GADT definition, the variance of some parameter
       cannot be checked

I'm not wedded to using polymorphic variants here, but I have essentially the same trouble using a hierarchy of class types (with different sets of `unit` methods to induce the intended subtype relation) to express the index lattice. Are there other options?

I also tried using trunk's injectivity annotations (`type +!_ exp = ...`) on a lark since I'm not confident that I fully understand what happens to the anonymous type variables for the rows in the polymorphic variants. But that doesn't seem to change things.

Is this sort of use case something for which there are known encodings? In a way I'm trying to benefit from some of the advantages of polymorphic variants (subtyping) without the drawbacks such as weaker exhaustiveness and less compact memory representation by keeping the polymorphic variants in a phantom index. Is this approach doomed?

Cheers, Josh

             reply index

Thread overview: 2+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-06-21 16:10 Josh Berdine [this message]
2020-06-27 15:33 ` Oleg

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

* 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