How to represent a function which can take the union of two sets of polymorphic variants

Learning
1

In my codebase I have two sets of events which can be generated by two different subsystems. It would be convenient for these to be dealt with by a single function at the point where the subsystems both feed in.

So I have the two sets of variants:

type foo = [`EventA | `EventB]
type bar = [`EventC]

What I want to do is to have a function who can take the union of these variants. Playing around I managed to get this code to compile:

let foobar : [foo | bar] -> unit = ...

The issue is on the application side. When I try something like:

let v : foo = ...
foobar v

I get a type error: saying that v does not have type `EventC

I can fix this by explicitly subtyping v: (v :> [foo | bar]) however this feels like it shouldn’t be necessary and that there should be something I can do to the signature of foobar to fix this?

(Things I’ve tried so far: [< ... ] doesn’t seem to work in that subsequent matches on those actions loose the typing information, [> ...] still has the same issues as [ ... ])

2

I believe what you want is to use [< foo | bar] instead of [foo | bar] in the definition of foobar. What problems do you see?

Best wishes,
Nicolás

2 Likes
4

When it comes to polymorphic variants (and objects) I think one must assume that one has to explicitly cast things. They’re add-ons to the ML type-system, and while I don’t know precisely what guarantees the type-inference mechanism gives for them, I sort of doubt that there’s any real guarantee of inference or most-general typings or anything.

Everywhere I’ve ever seen nontrivial use of polyvariants, it’s been with expliclt type-casts.

5

Inference seems to work perfectly for me:

# type foo = [`EventA | `EventB]
type bar = [`EventC];;

# let foobar = function
  | `EventA -> "EventA"
  | `EventB -> "EventB"
  | `EventC -> "EventC";;
val foobar : [< `EventA | `EventB | `EventC ] -> string = <fun>

# let v : foo = `EventA;;
val v : foo = `EventA

# foobar v;;
- : string = "EventA"
6

That was what I was also expecting to work, the issue is that if I have any type information attached to it, it seems to get lost.

type a = {v:int}
type b = {v:bool}

type foo = [ `EventA of a | `EventB of b ]

let foo : [< foo] -> string = function
| `EventA t -> Int.to_string t.v
| `EventB t -> Bool.to_string t.v

This fails to correctly type the first t as a and ends up typing it as b (I’m presuming that is because it is the most recent declaration with a t.v).

7

In summary, I’ve got something which works now: making they typing on the foobar function exact and letting its arguments expand. Its not exactly optimal (since now those arguments aren’t typed exactly) but it works (so long as I don’t do post processing on the arguments…).

8

I think you have the right diagnosis. Going a step further, it appears that the type-based disambiguation of the record field doesn’t work when given a closed variant type. Your example works fine if we write foo instead of [< foo] in the type of (the function) foo’s argument.

We see the same behavior in code like the following:

# module M = struct type t = M end;;
module M : sig type t = M end
# type t = [ `M of M.t ];;
type t = [ `M of M.t ]
# let f : [< t ] -> unit = function | `M M -> ();;
Line 1, characters 39-40:
Error: Unbound constructor M

I don’t know if this can be improved, but it might be good to make a GitHub issue just to see if it’s possible.

9

Made an issue for it: https://github.com/ocaml/ocaml/issues/9785

10

Note that polymorphic variant tags are not declared, but inferred, so in the body of foo, there is no constraint that `EventA is the same as the one mentioned in the declaration of type foo. So your example should require a type ascription in the pattern:

let foo : [< foo] -> string = function
  | `EventA (t : a) -> Int.to_string t.v
  | `EventB (t : b) -> Bool.to_string t.v

Edit: Though I do see your point in that disambiguation might helpfully be strengthened in cases like this where the type that could be inferred without the annotations will right afterward lead to a type failure.

1 Like
11

Out of interest why would removing the < make this work? Is it just in the case of [< that the variant tags are inferred?

12

I don’t know all the details, especially of how inference and disambiguation interact, but for polymorphic variant types that are not “fixed” (have a < or >) include an implicit type variable. This is because subtyping of polymorphic variants is implemented using row polymorphism. I expect that the presence of this implicit type variable, that can be unified during type inference, is involved in the difference with respect to disambiguation.

1 Like
13

Having poked at this a bit more, a nice way to avoid this is to supply the type info inside the match:

# module M = struct type t = M end;;
module M : sig type t = M end
# type t = [ `M of M.t ] ;;
type t = [ `M of M.t ]
# let f : [< t ] -> unit = function | (`M M : t) -> ();;
val f : t -> unit = <fun>

# type a = {v:int}
type b = {v:bool}

type foo = [ `EventA of a | `EventB of b ]

let foo : [< foo] -> string = function
  | (`EventA a : foo) -> Int.to_string a.v
  | (`EventB b : foo) -> Bool.to_string b.v
  ;;
type a = { v : int; }
type b = { v : bool; }
type foo = [ `EventA of a | `EventB of b ]
val foo : foo -> string = <fun>