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

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):

此表达式具有类型b - >字符串,但表达式需要类型a - >'a Type b = [`A | `B]与类型a = [`A]不兼容第二种变体类型不允许标记`B

问题:

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

Answer 1

根本问题是为什么类型

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

目前,此代码失败了

错误:此表达式的类型为[<`A | `b]但是表达式的类型为[>`A | `B]
第一个变体类型不允许标记`B

此时,如果`b是拼写错误,就可以在这里发现错误.如果pp已输入[< `A|`B |..],则双重类型将被限制为[`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适用于不同的多态变体集.