ocaml - 为什么不能对超集进行多态变体的封闭子集类型检查？

Question

变体 [`A | `B]与 [`A | `B | `C] 这样的超集类型不兼容

我知道它们不能统一，除非 >被添加到子集或 <到超集，但我很好奇是否有一个例子接受这种类型的输入会导致不正确的程序。

像这样一个非常简单的用法:

let return_a : bool -> [ `A ] = fun _ -> `A

let foo : bool -> [ `A | `B ] = return_a

作为 foo 的声明类型，接受该实现似乎是完全安全的是实现类型(即 return_a 的类型)的严格超集。但是(如预期的那样)它不会进行类型检查:

Error: This expression has type bool -> [ `A ]
but an expression was expected of type bool -> [ `A | `B ]
The first variant type does not allow tag(s) `B

在我看来，它实际上是一种比

限制性更强的类型

let return_a : bool -> [ `A ] = fun _ -> `A

let foo : bool -> [< `A | `B ] = return_a

哪个做类型检查。

这种对多态变体使用的限制只是对类型推断工作方式的限制，还是有将第一个片段标记为错误类型的实际原因？

Answer 1

类型[`A | `B] 是 [`A | 的子类型`B | `C]。 OCaml 支持子类型化，但它必须是显式的。

# type abc = [`A | `B | `C];;
type abc = [ `A | `B | `C ]
# type ab = [`A | `B];;
type ab = [ `A | `B ]
# let f (x: abc) = 14;;
val f : abc -> int = <fun>
# let (x: ab) = `A;;
val x : ab = `A
# f x;;
Error: This expression has type ab but an expression was expected of type abc      
       The first variant type does not allow tag(s) `C
# f (x :> abc);;
- : int = 14
#