Is OCaml function over polymorphic variants not polymorphic enough?

Question

OCaml gives function `A -> 1 | _ -> 0 function `A -> 1 | _ -> 0 type [> `A] -> int , but why is this not so: [> ] -> int ?

This is my reasoning:

• function `B -> 0 is of type [<`B] -> int . Adding the `A -> 0 branch to make it function `A -> 1 | `B -> 0 function `A -> 1 | `B -> 0 , weakens it to [<`A|`B] -> int . A function becomes more permissive in the type of argument that it can accept. It makes sense.
• function _ -> 0 is of type 'a -> int . This type is unified with [> ] -> int , and [> ] is already an open type (very permissive). Adding the `A -> 0 branch to make it function `A -> 1 | _ -> 0 function `A -> 1 | _ -> 0 , restricts the type [>`A] -> int . That doesn't make sense to me. Indeed, adding another branch `C -> 1 will make it [>`A|`C] -> int , further restricting the type. Why?

Note. I'm not looking for workarounds, I just wanted to know the logic of this behavior.

In a related note, function `A -> `A | x -> x function `A -> `A | x -> x is of type ([>`A] as 'a) -> 'a , and although this is also a limiting open type for the parameter, I can understand the reason. The type must be combined with 'a -> 'a , [>` ] -> 'b , 'c -> [>`A] ; the only way to do this seems to be ([>`A] as 'a) -> 'a .

Is there a similar reason for my first example?

Answer 1

A possible answer is that type [> ] -> int would allow an argument (`A 3) , but this is not allowed for function `A -> 1 | _ -> 0 function `A -> 1 | _ -> 0 . In other words, the type should record the fact that `A does not accept any parameters.

Answer 2

The reason is very practical:
In older versions of OCaml, the intended type was

 [`A | .. ] -> int 

which meant that A does not accept arguments, but may be absent.

However, this type is uniform with

 [`B |`C ] -> int 

which leads to the fact that `A is discarded without any verification.

This makes it easy to enter errors with errors.
For this reason, variant constructors must either appear at the upper or lower bounds.

Answer 3

Typing (function `A -> 1 | _ -> 0) is reasonable, as Geoffrey explained. Reason for which

 (function `A -> 1 | _ -> 0) ((fun x -> (match x with `B -> ()); x) `B) 

does not check the type, it should be explained, in my opinion, the last part of the expression. Indeed, the function (fun x -> (match x with `B -> ()); x) has an input type [< `B] , and its parameter `B has a type [> `B ] . Combining both types produces a private type [ `B ] that is not polymorphic. It cannot be unified with the input type [> `A ] that you get from (function `A -> 1 | _ -> 0) .

Fortunately, polymorphic variants not only rely on (in-line) polymorphism. You can also use subtyping in situations where you want to increase the private type: [ `B ] is a subtype, for example, [`A | `B] [`A | `B] , which is an instance of [> `A ] . Subtype assignment is explicit in OCaml using the syntax (expr :> ty) (casting for some type) or (expr : ty :> ty) if the domain type cannot be correctly inferred.

You can write:

 let b = (fun x -> (match x with `B -> ()); x) `B in (function `A -> 1 | _ -> 0) (b :> [ `A | `B ]) 

which is well typed.