I’m curious if it’s possible to write a module signature similar to the following:
module type Foo = sig
val expand : [ a | b ] list -> a list
Basically each module that wants to fulfill
Foo must provide two polymorphic variant types
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
b could be anything, e.g.
int). Is there any way to annotate
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
Sure, just make it
[ `A of a | `B of b ] list -> a list
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.
[ 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
val expand : a_or_b list -> a list
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
Then there’d need to be type inference so the compiler can infer the previous statement from
[ a | b ].
Does that make sense?
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.