OCaml函数超过多态变体不够多态？

Question

OCaml给出function `A -> 1 | _ -> 0了类型[> `A] -> int,但为什么不是这样[> ] -> int？

这是我的理由:

• function `B -> 0有类型[<`B] -> int.添加`A -> 0分支以使其function `A -> 1 | `B -> 0松散[<`A|`B] -> int.该函数在它可以接受的参数类型中变得更加宽松.这是有道理的.
• function _ -> 0有类型'a -> int.这种类型是统一的[> ] -> int,并且[> ]是一种已经开放的类型(非常宽松).添加`A -> 0分支以使其将类型function `A -> 1 | _ -> 0 限制为[>`A] -> int.这对我来说没有意义.实际上,添加另一个分支`C -> 1将成为它[>`A|`C] -> int,进一步限制类型.为什么？

注意:我不是在寻找解决方法,我只是想知道这种行为背后的逻辑.

在相关的说明中,function `A -> `A | x -> x有类型([>`A] as 'a) -> 'a,虽然这也是参数的限制性开放类型,但我可以理解其中的原因.该类型应该与统一'a -> 'a,[>` ] -> 'b,'c -> [>`A],这样做的唯一方法似乎是([>`A] as 'a) -> 'a.

我的第一个例子是否存在类似的原因？

Answer 1

一个可能的答案是类型[> ] -> int允许参数,(`A 3)但不允许这样做function `A -> 1 | _ -> 0.换句话说,类型需要记录`A不带参数的事实.

Answer 2

原因是非常实用的:
在旧版本的OCaml中,推断类型是

[`A | .. ] -> int

这意味着A不参与,但可能缺席.

但是这种类型是可以统​​一的

[`B |`C ] -> int

这会导致`A在没有任何检查的情况下被丢弃.

它很容易引入错误拼写错误.
因此,变体构造函数必须出现在上限或下限.