多态变体上的通配符模式覆盖子类型约束 [英] Wildcard pattern overriding subtype constraint on polymorphic variant

问题描述

给出这些类型

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

和此功能

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

应用类型为a的值可以正常工作，如预期:

applying a value of type a works without issue, as expected:

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

但是，如果将功能修改为包含通配符模式

However, if the function is modified to include a wildcard pattern

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

即使其他所有内容保持不变，它现在也会产生以下错误(在let _ = pp a上):

even though everything else remains the same, it now yields the following error (on let _ = pp a):

该表达式的类型为b->字符串，但是期望表达式的类型为a->'a Type b = [`A | `B]与类型a = [`A]不兼容.第二种变体类型不允许标签'B

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

问题:

1. 为什么它不再能够接受子类型?我知道通配符意味着它现在可以接受超类型，但这并不意味着必须.
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 .

is infered as [> `A| `B] -> string and not as [< `A| `B | ... ] -> string (where ... stands for any constructor). The answer is that is a design choice and a question of compromise between false positive and false negative : https://www.math.nagoya-u.ac.jp/~garrigue/papers/matching.pdf .

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

More precisely, the second type was deemed too weak since it was too easy to lose the information that `A and `B were present in pp. For instance, consider the following code where `b is a spelling mistake and should have been `B:

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

当前，此代码失败

错误:此表达式的类型为[< `A | `b]，但期望表达 类型[>`A | `B]
第一种变体类型不允许标签'B

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 |..]，则对偶类型将被无声地限制为[`A] -> unit * string，没有机会捕获此错误.而且，在当前键入的情况下，如果`b不是拼写错误，则完全有可能通过添加一些强制性来使dual有效

At this point, if `b was a spelling mistake, it becomes possible to catch the mistake here. If pp had been typed [< `A|`B |..], the type of dual would have been restricted to [`A] -> unit * string silently, with no chance of catching this mistake. Moreover, with the current typing, if `b was not a spelling mistake, it is perfectly possible to make dual valid by adding some coercions

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

非常明确地说明restrict和pp可在不同的多态变体集上工作.

making it very explicit that restrict and pp works on different sets of polymorphic variants.

这篇关于多态变体上的通配符模式覆盖子类型约束的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！