6

鉴于这些类型

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"
           | _ -> "?"

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

此表达式的类型为 b -> 字符串，但预期的表达式类型为 a -> 'a Type b = [ `A | `B ] 与类型 a = [ `A ] 不兼容 第二个变体类型不允许标记 `B

问题：

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

2 回答 2

7

根本的问题是为什么类型

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。例如，考虑以下代码 where`b是拼写错误并且应该是`B：

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

目前，此代码失败

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

在这一点上，如果`b是拼写错误，就可以在这里发现错误。如果pp是[< `A|`B |..]type 的话，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适用于不同的多态变体集。

于 2017-11-10T09:39:49.260 回答
1

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

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

于 2017-11-09T22:02:17.143 回答