Write type constraint for polymorphic variants with generic type parameters

Question

Background: I was trying to create something as described in the paper, Data Type à la Carte - but trying to see if OCaml's polymorphic variants could lead to a clean ReasonML implementation.

My code here is in ReasonML syntax, but the question is equally applicable to OCaml.

I start by defining two modules for a Val and a Add, both implementing an fmap - making them a haskel-style functor.

module type Functor = {
  type t('a);
  let fmap: ('a => 'b, t('a)) => t('b);
};

module Val = {
  type t('e) = [ | `Val(int)];
  let fmap = _ =>
    fun
    | `Val(x) => `Val(x);
};

module Add = {
  type t('e) = [ | `Add('e, 'e) ];

  let fmap = f =>
    fun
    | `Add(x, y) => `Add((f(x), f(y)))
};

I can fairly easily create an Algebra data type that combines these two modules into one, with a really simple fmap implementation.

module Algebra = {
  type t('t) = [ Val.t('t) | Add.t('t)];

  let fmap = (f, x) =>
    switch (x) {
    | #Val.t as v => Val.fmap(f, v)
    | #Add.t as o => Add.fmap(f, o)
    };
};

This compiles and works in a larger context where I can evaluate an expression consisting of both Val and Add values.

However, as a programmer who would like to avoid writing boiler-plate code, my next step would be to create a functor (OCaml functor) that can generate such a module from any two compatible modules.

My first attempt is this:

module JoinAlgebra = (A1: Functor, A2: Functor) => {
  type t('t) = [ A1.t('t) | A2.t('t)];

  let fmap = (f, x) =>
    switch (x) {
    | #A1.t as v => Val.fmap(f, v)
    | #A2.t as o => Add.fmap(f, o)
    };
};

But this doesn't work. As the A1.t and A2.t can be anything, I cannot combine them as a polymorphic variant.

Error: The type A1.t('t) is not a polymorphic variant type

I tried adding a type constraint to the Functor module type:

module type Functor = {
  type t('a) = 'a constraint [> ] = 'a;
  let fmap: ('a => 'b, t('a)) => t('b);
};

module JoinAlgebra = (A1: Functor, A2: Functor) => {
  type t('t) = [ A1.t('t) | A2.t('t)]; // This line fails
}

Now I get the compiler error

Error: The type A1.t([> ]) is not a polymorphic variant type

Is there any way I can create a module-functor that automatically based on the two modules?

A note about OCaml versions: I am using bucklescript v. 5 here, which uses the OCaml 4.02 compiler. But solutions that require 4.06 are also welcome (support should be coming to Bucklescript)

Del Del · Accepted Answer · 2019-04-25T07:51:42

Your Functor signature defines an abstract type 'a t. As you correctly point out, "as the A1.t and A2.t can be anything, I cannot combine them as a polymorphic variant." To solve the problem that 'a t in Functor is abstract, you try to make it a polymorphic variant by doing:

module Functor = struct
  type 'a t = 'a constraint 'a = [< ]
end

However, the 'a type variable no longer stands for the wrapped value, but rather the polymorphic variant constraint. This is certainly not what you want. You get the error Error: The type A1.t([> ]) is not a polymorphic variant type because you can only substitute "exact variant types" into polymorphic variants:

The first case is an exact variant type: all possible tags are known, with their associated types, and they can all be present. Its structure is fully known.

...

In all three cases, tags may be either specified directly in the `tag-name [of typexpr] form, or indirectly through a type expression, which must expand to an exact variant type, whose tag specifications are inserted in its place.

(https://caml.inria.fr/pub/docs/manual-ocaml/types.html#polymorphic-variant-type)

You don't need polymorphic variants for your JoinAlgebra. Just do:

module JoinAlgebra (A1 : Functor) (A2 : Functor) = struct
  type 't t = Left of 't A1.t | Right of 't A2.t

  let fmap f x =
    match x with
    | Left v -> Left (A1.fmap f v)
    | Right o -> Right (A2.fmap f o)
end

The benefit is that the 'a t in Functor remains abstract and the code works for Functor modules that do not define polymorphic variants.

Write type constraint for polymorphic variants with generic type parameters

1 Answers