Polymorphic variant type annotation

Learning
1

Hi,

I’m curious if it’s possible to write a module signature similar to the following:

module type Foo = sig
  type a
  type b
  val expand : [ a | b ] list -> a list
end

Basically each module that wants to fulfill Foo must provide two polymorphic variant types a and b and a function that takes a list of variants from either type and expands all variants from type b into variants from type a. My version doesn’t work because neither type can expand into a polymorphic variant (since a and b could be anything, e.g. string or int). Is there any way to annotate a and b to ensure they are polymorphic variant types?

Currently I’m working around the problem by instead requiring a function val expand : b -> a list and calling that function and flatmapping the result in the functor that uses Foo.

1 Like
2

Sure, just make it

[ `A of a | `B of b ] list -> a list
3

Well, yes, but having to prefix each polymorphic variant with some Tag kind of kills the readability. Additionally people would have to know which type each variant belongs to which is not ideal in my case.

4

The [ a | b ] syntax only works with statistically known types, you cannot really use it in this case.
One option is to update your signature to

module type Foo = sig
  type a
  type a_or_b
  val expand : a_or_b list -> a list
end
5

Would it theoretically be possible to add support for this to OCaml? Or is there some reason why such a program could not be type checked?

What would need to be done (as far as I can tell, and I’m really not that skilled in type theory) is adding support for restricting abstract types to some subset of all types, right? Basically making it possible to state “There is some type a that must be a polymorphic variant type that has no variant conflicts with some type b and there is some type b that must be a polymorphic variant type that has no variant conflicts with some type a.”

Then there’d need to be type inference so the compiler can infer the previous statement from [ a | b ].

Does that make sense?

6

A lot of things are theoretically theoretically possible. A more interesting question would be what new interesting programs can be well typed? And at what cost? In your example, every functions that could be typed with the [ a | b ] type, can be be typed with simple abstract types.