通配符模式覆盖多态变体的子类型约束

Question

鉴于这些类型

type a = [ `A ]
type b = [ a | `B  | `C ]

和这个函数

let pp: [< b] -> string =
  function | `A -> "A"
           | `B -> "B"
           | `C -> "C"

应用 a 类型的值没有问题，正如预期的那样：

let a: a = `A
let _ = pp a

但是，如果函数被修改为包含通配符模式

let pp: [< b] -> string =
  function | `A -> "A"
           | `B -> "B"
           | _ -> "?"

即使其他一切都保持不变，它现在会产生以下错误（在 let _ = pp a 上）：

This expression has type b -> string but an expression was expected of type a -> 'a Type b = [ `A | `B ] is not compatible with type a = [ `A ] The second variant type does not allow tag(s) `B

问题：

为什么它不再能够接受子类型？我知道通配符意味着它现在可以接受超类型，但这不应该意味着它必须。
有什么办法可以解决这个问题，避免列举一百万左右不相关的变体吗？

Answer 1

pp第二个版本的类型是[< b > `A `B ] -> string。换句话说，`A 和 `B 必须出现在类型中。我想这似乎是合理的，如果你想将一个值与 `B 进行比较，那么 `B 应该出现在值的类型中。

你可以写pp (a :> b).

Answer 2

根本的问题是为什么

let pp= function
| `A -> "A"
| `B -> "B"
| _ -> "?"

被推断为 [> `A| `B] -> string 而不是 [< `A| `B | ... ] -> string （其中 ... 代表任何构造函数）。答案是这是一种设计选择，也是假阳性和假阴性之间折衷的问题：https://www.math.nagoya-u.ac.jp/~garrigue/papers/matching.pdf。

更准确地说，第二种类型被认为太弱了，因为它太容易丢失 `A 和 `B 出现在 pp 中的信息。例如，考虑以下代码，其中 `b 是一个拼写错误，应该是 `B:

let restrict (`A | `b) = ()
let dual x = restrict x, pp x

目前，此代码失败

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

在这一点上，如果 `b 是一个拼写错误，就可以在这里发现错误。如果 pp 被键入 [< `A|`B |..]，dual 的类型将被静默地限制为 [`A] -> unit * string，没有机会捕捉到这个错误。此外，对于当前的打字，如果 `b 不是拼写错误，则完全有可能通过添加一些强制转换

使 dual 有效

let dual x = restrict x, pp (x:[`A]:>[>`A]);;
(* or *)
let dual x = restrict x, (pp:>[`A] -> _) x

非常明确地表明 restrict 和 pp 适用于不同的多态变体集。

通配符模式覆盖多态变体的子类型约束

Wildcard pattern overriding subtype constraint on polymorphic variant

ocaml

types

type-inference

subtyping

polymorphic-variants