Polymorphic variant --> GADT?

Question

I'm writing a Prolog system and I am using polymorphic variants to represent Prolog terms.

In particular, I use polymorphic variants (instead of regular ones) so I can do subtyping while ensuring OCaml's excellent exhaustiveness checks of matches on subtypes.

So far, so good!

On multiple occasions I have been reading about GADTs (on discuss.ocaml.org, and in realworldocaml.org). To me, GADTs appear to offer similar features, but with a smaller memory footprint: polymorphic variants with cases having more than one argument require an extra pointer that regular variants do not need.

So far, I have not been able to use GADTs successfully, so here's my question:

Is there a simple, straightforward way to convert code using polymorphic variants to GADTs? It this even possible in the general case?

Thank you in advance!

Have you tried anything that suggests it isn't possible? By using a polymorphic variant type as the type parameter and encoding the payload type in the constructor name to avoid collisions I think it should be possible in general. But certainly not pretty. — glennsl
Your question is a bit too general. The short answer is no, you can't "convert code using poly variants to GADTs" in the absolute. You can try to convert in some specific cases. In general, GADTs can do some of the stuff poly vars are used for, the same way you can bang a nail with a swiss army knife. — Drup

ivg ivg · Accepted Answer · 2020-11-11T15:41:25

Is there a simple, straightforward way to convert code using polymorphic variants to GADTs? Is this even possible in the general case?

No, because they, in general, serve completely different purposes.

Polymorphic variants provide subtyping for sum types. GADT enable constraints for sum type variants.

You can, however, use both techniques to partition a sum type into a quotient set of types that comprise your super type. You can even use phantom polymorphic variants as the witness type for each subset.

Let's do some coding, imagine we have a set of figures, which we would like to subdivide into two non-intersecting subsets of circles and rectangles.

Using the polymorphic variants,

  type circle = [ `circle of int]
  type rectangle = [`rectangle of int * int]
  type figure = [circle | rectangle]

and the same using GADT

  type circle = Is_circle
  type rectangle = Is_rectangle
  type _ figure =
    | Circle : int -> circle figure
    | Rectangle : int * int -> rectangle figure

Note, how the constraint is explicitly expressed with circle and rectangle type. We could even use polymorphic variants to witness the constraint. Anything will work, as long as the type checker could distinguish the two types in the constraint (i.e., abstract types won't work as their implementation might be equal).

Now let's make some operations that involve subtyping. Let's start with polymorphic variants

  let equal_circle (`circle r1) (`circle r2) = r1 = r2

  let equal_rectangle (`rectangle (x1,y1)) (`rectangle (x2,y2)) =
    x1 = x2 && y1 = y2

  let equal_figure x y = match x,y with
    | (#circle as x), (#circle as y) ->
      equal_circle x y
    | (#rectangle as x), (#rectangle as y) ->
      equal_rectangle x y
    | #rectangle, #circle
    | #circle, #rectangle -> false

So far so good. A small caveat is that our equal_circle and equal_rectangle functions are a bit too polymorphic, but that could be easily solved by adding a proper type constraint or having a module signature (we are always using module signatures, right?).

Now let's implement the same with GADT, slowly,

  let equal_circle (Circle x) (Circle y) = x = y

  let equal_rectangle (Rectangle (x1,y1)) (Rectangle (x2,y2)) =
    x1 = x2 && y1 = y2

Looks the same as the poly example, modulo small syntactic differences. The type is also looking nice and precise, val equal_circle : circle figure -> circle figure -> bool. No need for extra constraints, the type checker is doing our work for us.

OK, now let's try to write the super method, the first attempt will not work:

  (* not accepted by the typechecker *)
  let equal_figure x y = match x,y with
    | (Circle _ as x), (Circle _ as y) ->
      equal_circle x y
    | (Rectangle _ as x), (Rectangle _ as y) ->
      equal_rectangle x y

With GADT the type checker by default will pick a concrete type index, so instead of ascribing the 'a figure -> 'b figure -> bool type, the type checker will select arbitrary an index, in our case, it is circle and complain that rectangle figure is not a circle figure. No problem, we can explicitly say that we want to allow the comparison of arbitrary figures,

  let equal_figure : type k. k figure -> k figure -> bool =
    fun x y -> match x,y with
      | (Circle _ as x), (Circle _ as y) ->
        equal_circle x y
      | (Rectangle _ as x), (Rectangle _ as y) ->
        equal_rectangle x y

This type k says to the type checker: "generalize all occurrences of k". So we now have a method that has a slightly different typing than the corresponding method implemented with polymorphic variants. It can compare figures of an equal kind but not figures of different kinds, i.e., it has type 'a figure -> 'a figure -> bool. The thing that you can't express with polymorphic variants, indeed, the same implementation with polyvariants is non-exhaustive,

  let equal_figure x y = match x,y with (* marked as non-exhaustive *)
    | (#circle as x), (#circle as y) ->
      equal_circle x y
    | (#rectangle as x), (#rectangle as y) ->
      equal_rectangle x y

We can, of course, implement a more generic method that enables comparison of arbitrary figures using GADT, e.g., the following definition has type 'a figure -> 'b figure -> bool

  let equal_figure' : type k1 k2. k1 figure -> k2 figure -> bool =
    fun x y -> match x,y with
      | (Circle _ as x), (Circle _ as y) ->
        equal_circle x y
      | (Rectangle _ as x), (Rectangle _ as y) ->
        equal_rectangle x y
      | Rectangle _, Circle _
      | Circle _, Rectangle _ -> false

We immediately see that for our purposes GADT is a more powerful tool that gives us more control on the constraints. And given that we can use polymorphic variants and object types as type indices for expressing constraints, we can have the best from the two worlds - fine-grained constraints and subtyping.

To be honest, you can achieve the same result as with GADT but without GADT, using the tagless-final style. But this is an implementation detail, which sometimes is important in practice. The main issue with GADT is that they are not serializable. Indeed, you can't store the phantom type.

To conclude, no matter if you're using GADT or Tagless-Final Style, you have much more control over the type constraints and can express your intent more clearly (and let the type checker enforce it). We are using it a lot in BAP to express the complex constraints off well-formed programs, e.g., that bitvector operations are applied to the vectors of the same length. This enables us to disregard ill-formed programs in our analysis and saves us a few lines of code and a few hours of debugging.

The answer, even with that simple example, has already grown too big so I have to stop. I would suggest you visiting discuss.ocaml.org and search for GADT and Polymorphic Variants there. I remember that there were a few more thorough discussions there.

Polymorphic variant --> GADT?

1 Answers

Some deeper discussions from dicuss.ocaml.org