Align polymorphic variant types between calling function and callback

Question

I'm trying to write an event handler that doesn't need to handle all known types of events, and am trying to model this with an OCaml polymorphic variant type (event.mli):

type 'events event =
  [< `click of int * int | `keypress of char | `quit of int ] as 'events

(* Main loop should take an event handler callback that handles 'less than' all known event types *)
val mainLoop : ('events event -> unit) -> unit

val handler : 'events event -> unit

An example implementation (event.ml):

type 'events event =
  [< `click of int * int | `keypress of char | `quit of int ] as 'events

let mainLoop handler =
  for n = 1 to 10 do
    handler begin
      if n mod 2 = 0 then `click (n, n + 1)
      else if n mod 3 = 0 then `keypress 'x'
      else `quit 0
    end
  done

let handler = function
  | `click (x, y) -> Printf.printf "Click x: %d, y: %d\n" x y
  | `quit code -> exit code

Unfortunately, this fails with the following error:

File "event.ml", line 1:
Error: The implementation event.ml
       does not match the interface event.cmi:
       Values do not match:
         val mainLoop :
           ([> `click of int * int | `keypress of char | `quit of int ] -> 'a) ->
           unit
       is not included in
         val mainLoop :
           ([< `click of int * int | `keypress of char | `quit of int ] event ->
            unit) ->
           unit
       File "event.ml", line 4, characters 4-12: Actual declaration

How can I get the implementation of mainLoop to be inferred as type ([< `click of int * int | `keypress of char | `quit of int ] -> unit) -> unit, i.e. as ('events event -> unit) -> unit?

Answer 1

Let's have some explanation of 'subtyping theory' in plain english, and a little bit of common sense.

In object oriented languages (like java or ocaml), the most general class you may define is the empty class, ie. the class which has no property nor method. Indeed any class may derive from it, and in term of types, any class type is a subtype of the empty class type.

Now, functions are said to be contravariant on their input, and covariant on their output.

If we look at how functions behave typewise we see that:

• you may pass to it a value of the type it accepts, or a value of any subtypes of that type. In the extreme case, if you define a function accepting an instance of the empty class, clearly that function will not be able to do anything with it. Hence, an instance of any other class will also do, as we know that the function will not expect anything of it.
• the result of a function may be a value of the type it is defined as returning, or a value of any subtype of that type.

Why do we use two different words for seemingly the same behaviour for input and output?

Well, consider now the usual type constructors in ML style type theory : products ( the * type constructor), sums (algebraic datatypes), and arrows (function types). Basically, if you define a type T using products or sums, specializing (using a subtype of) any of their argument will produce a specialization (subtype) of T. We call this feature covariance. As an example, the list constructor, which is made of sums, is covariant: if you have a list of class a, and b is derived from a, then the type b list is a subtype of a list. Indeed, for a function accepting a a list you may pass it a b list without errors.

If we look at the arrow -> constructor, the story is slightly different. A function f of type x -> y takes any subtype of x and returns any subtype of y. If we suppose x to be a function type, it means that f has actually type (u -> v) -> y, with x = u -> v. So far so good. How may u and v vary in this setting? it depends on what f might do with it. f knows that it can only pass a u or a subtype of u to that function, thus the most general value that f could pass is a u, which means that the actual function being passed may accept any supertype of u as it argument. In the extreme case, I could give f a function which accept the empty object as its argument and return something of type v. So all of a sudden, the set of types changed from 'type and subtypes' to 'type and supertypes'. So a subtype of the type u -> v is u' -> v' where v' is a subtype of v and u' is a supertype of u. This is why our arrow constructor is said to be contravariant on its input. The variance of a type constructor is how its subtypes/supertypes are determined according to the subtypes/supertypes of its arguments.

Next, we must consider polymorphic variants. If the type x is defined as [ `A | `B ], then what's the relationship with the type y = [ `A ] ? The main property of subtyping is that any value of a given type may be safely upcasted to a supertype (actually it's how subtyping is usually defined). Here, `A belongs to both types, and thus the cast is safe both ways, but `B is only present in the first type, and thus may not be casted to the second. So, a value of y may be casted to the first, but a value of x may not be casted to the second. the subtyping relation is clear : y is a subtype of x!

What about the [> ... ] and [< ...] notations? The first one represents a type and all its supertypes (there's an infinity of them), while the second means a type and all its subtypes (which is a finite set, comprising the empty type). Hence, the type naturally infered for a function which takes a polymorphic variant v will be on input that variant and all its subtypes, ie. [< v ], but an higher order function - a function taking a function as its argument - will see that argument variance flipped, and its input type will thus be something like ([> v ] -> _) -> _. The exact rule for variances in functions is expressed in the wikipedia page linked above.

Now you can probably see why the type you are aiming for - ([< _ ] -> _) -> _) - cannot be constructed. Our variances for arrows forbid it.

So, what can you do in your code? My guess is that what you really want to do, is what the inference algorithm will deduce from your sample code: ([> basic_event ] -> _) -> _). where the basic_event type would be the one covering exactly the 3 variants there.

type basic_event =
   [ `click of int * int | `keypress of char | `quit of int ]

(* Main loop should take an event handler callback that handles 'less than' 
   all known event types *)
val mainLoop : ([> basic_event ] -> unit) -> unit

val handler : [< `click of int * int | `quit of int ] -> unit

In your case, it's probably better not to include a lower or upper bound in the type, and use these bounds in the function signatures, as outlined in the above code.

Answer 2

I think the problem is in your type definition, I understand you want your type to contains at most this three events (first of all why 'at most' and not 'at least' ?) but in this case with this signature of mainLoop you cannot presice your type.

For example look at type of x:

let (x : [< `A | `B]) = `A
val x : [< `A | `B > `A ] = `A

and [< ... >] is not the same thing as [< ...]. Its means that even if you cast mainLoop you will have an error:

let mainLoop (handler :
              [< `click of int * int | `keypress of char | `quit of int ]
              event -> unit) = ...

       Values do not match:
         val mainLoop :
           ([ `click of int * int | `keypress of char | `quit of int ] event ->
            unit) ->
           unit
       is not included in
         val mainLoop :
           ([< `click of int * int | `keypress of char | `quit of int ] event ->
            unit) ->
           unit

But is it really a problem? Why not to change type 'events event = [< ... to type 'events event = [ ... ?

And in my opinion it's even better to use lower bounds rather than upper:

type 'events event =
  [> `click of int * int | `keypress of char | `quit of int ] as 'events

val mainLoop : ('events event -> unit) -> unit

val handler : 'events event -> unit

let mainLoop handler =
  for n = 1 to 10 do
    handler (
      if n mod 2 = 0 then `click (n, n + 1)
      else if n mod 3 = 0 then `keypress 'x'
      else `quit 0
    )
  done

let handler = function
  | `click (x, y) -> Printf.printf "Click x: %d, y: %d\n" x y
  | `quit code -> exit code
  | _ -> ()