How to extend poly variants with functors?

In our app we have a need for a possible extension of module types using a functor. In this module, we have a “default” version of this poly variant.
With the help of this “default” and the lower bounds constraint, we define a “minimal” type.
We also define a functor and the type of this functor’s arguments.
And finally, we want to extend these minimal poly variant s via passing a set of “extension” poly variants.
To give you a better idea of what we are trying, here’s a short snippet that demonstrates our set-up and issue

    module Color = {
      type composite<'t> = {colors: 't}
      type defaultColor = [#Red | #Green | #Blue]

      type otherColor<'t> = [
        | #combined(composite<'t>)
        | #otherCombined(composite<'t>)
      ]

      type minimalColor<'a> = [> defaultColor] as 'a

      type rec default = [defaultColor | otherColor<default>]

      module type Config = {
        // Should require at least `defaultColor` to be passed to our `Make` functor
       type extension  = minimalColor<defaultColor>
      }
      module Make = (Config: Config) => {
        type color = [defaultColor | Config.extension]
        type rec t = [color | default]
      }
    }

    module Impl = {
      include Color.Make({
        /*
       	Signature mismatch:
      	...
      	Type declarations do not match:
        	type rec extension = [#Ext1 | #Ext2]
      	is not included in
        	type rec extension = Color.minimalColor<Color.defaultColor>
      	File "playground.res", line 16, characters 3-47: Expected declaration
      	File "playground.res", line 29, characters 4-36: Actual declaration
        */
        type extension = [#Ext1 | #Ext2]
      })
    }

Or here’s the same code in a simple playground.

Any and all advice are very welcome!

Unfortunately, it is not really possible to extend polyvariants with arbitrary cases within a functor.

I wish I had a better grasp on the fundamental issue here, but I know it’s related to the fact that functors require the output module signature to be fully-defined, while polyvariants cannot be universally quantified.

I’ll try to explain it to the best of my ability, but I know there are others here who understand this better than me. So if I make a mistake, please let me know!

For a polyvariant type to be fully defined (meeting the functor requirement), the entire polyvariant type, including the extension type, must be fully defined prior to its final definition in the output module. We cannot use a type variable to represent an arbitrary polyvariant type, where the final type is computed at the place where the functor is applied. This is because the polyvariant’s “constraints” must be fully defined in the module signature. Those constraints cannot be defined dynamically. More on “constraints” further down in this post.

E.g.:

let fun1: ('a) => [ defaultColor | 'a ] = ...

You should see a syntax error here. 'a cannot be included in the polyvariant type because it cannot be assumed to be a polyvariant at all. It could be anything.

let fun2: type a. (a) => [ defaultColor | a ] = ...

This uses “universal quantification.” (The type a. part defines a “universally quantified type” a, which is like saying "for all possible types a".) You should get a compile error saying type a is not a polymorphic variant. This is because polyvariants cannot be universally quantified.

type purplePlus<'a> = [> #Purple] as 'a;
let fun3: (minimalColor<'a>) => [ minimalColor<'a> | purplePlus<'a> ] as 'a = ...

The 'a here is not a “type variable”, but rather a “unification variable” that is known to be a polyvariant that must meet all the constraints implied by each type that uses it. This includes minimalColor<'a>, which constrains type 'a to include "at least [ #Red | #Green | #Blue ]". But type 'a is also constrained by the definition of purplePlus<'a>, which requires it to include "at least [ #Purple ]".

The final, “unified” type denoted by 'a must adhere to all of those constraints, so it will look like [> | #Red | #Green | #Blue | #Purple ]. The nice thing is that the unification variable 'a can be determined at the function call site. I think this might help you achieve the kind of “type extension” that you want.

For related reading, see this discussion in the OCaml forum: https://discuss.ocaml.org/t/polymorphic-variant-being-generalised/6083/3

It’s also worth mentioning “extensible variants.” It’s a more complicated kind of variant that can be arbitrarily extended at any point in your code. But it is also subject to restrictions when used within functors.

The syntax for extensible variants looks like this:

type t += ..

type t +=
  | Red
  | Green
  | Blue

// ...further down in the code...
type t +=
  | Purple

// Now we have added the `Purple` case to type `t`

This is an advanced technique. It tends to add unnecessary complexity, and it’s usually not worth it. I recommend staying away from extensible variants unless you have a really solid use case.

4 Likes

Hello and thank you very much for your extensive answer!

We’ve went over our use-case and decided to head in a different way since this approach seems to be a bit too problematic. Your answer definitely helped us a lot in the decision process!