OCaml function over polymorphic variants not sufficiently polymorphic?

Question

OCaml gives function `A -> 1 | _ -> 0 the type [> `A] -> int, but why isn't that [> ] -> int?

This is my reasoning:

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

Note: I am not looking for workarounds, I'd just like to to know the logic behind this behavior.

On a related note, function `A -> `A | x -> x has type ([>`A] as 'a) -> 'a, and while that is also a restrictive open type for the parameter, I can understand the reason. The type should unify with 'a -> 'a, [>` ] -> 'b, 'c -> [>`A]; the only way to do it seems to be ([>`A] as 'a) -> 'a.

Does it exist a similar reason for my first example?

Kutzer

Answer 1

A possible answer is that the type [> ] -> int would allow an argument (`A 3) but this isn't allowed for function `A -> 1 | _ -> 0. In other words, the type needs to record the fact that `A takes no parameters.

Revelatory

Good reason, thanks. But as a side effect of "recording", this still causes good-looking expressions like (function `A -> 1 | _ -> 0) ((fun x -> (match x with `B -> ()); x) `B) to fail to type-check. Might there be a deeper reason? I'll wait a little bit more before accepting your answer. – Kutzer

What type would you propose for function `A k -> k | _ -> 0? – Revelatory

gariguejej answered that below. – Kutzer

Answer 2

The reason is a very practical one:
In older versions of OCaml the inferred type was

[`A | .. ] -> int

which meant that A takes no argument but may be absent.

However this type is unifiable with

[`B |`C ] -> int

which results in `A being discarded without any kind of check.

It makes easy introducing errors with misspellings.
For this reason variant constructors must either appear in an upper or a lower bound.

Unpleasant

Thank you for the complete answer. Unfortunately I have no reputation to vote. – Kutzer

Oh, you are Jacques Garrigue. Keep up the good work! Just to tell you that I thought of this problem while reading the OCaml manual, section "Advance use". An complicated instance of this problem appears there, doesn't it. I read a blog somewhere which called that manual example "a major problem", so I just decided to ask. – Kutzer

Answer 3

The typing of (function `A -> 1 | _ -> 0) is reasonable, as explained by Jeffrey. The reason why

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

fails to type-check should be explained, in my opinion, by the latter part of the expression. Indeed the function (fun x -> (match x with `B -> ()); x) has input type [< `B] while its parameter `B has type [> `B ]. The unification of both types gives the closed type [ `B ] which is not polymorphic. It cannot be unified with the input type [> `A ] that you get from (function `A -> 1 | _ -> 0).

Fortunately, polymorphic variants do not only rely on (row) polymorphism. You can also use subtyping in situations, such as this, one where you want to enlarge a closed type: [ `B ] is a subtype of, for example, [`A | `B] which is an instance of [> `A ]. Subtyping casts are explicit in OCaml, using the syntax (expr :> ty) (casting to some type), or (expr : ty :> ty) in case the domain type cannot be inferred correct.

You can therefore write:

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

which is well-typed.

According

Yes, I know, and I made up the example with exactly that in mind. The problem is, in my opinion, that [>`A] is too restrictive than one would hope. But ok, since it isn't possible to express [>] constraint `A takes no arguments, there's nothing we can do. – Kutzer