GADT 上的模式匹配失败

Question

我在 ReasonML 上玩了更多，发现type t以下示例中的模式匹配无法处理错误

错误：此模式匹配 t(float) 类型的值，但预期模式匹配 t(int) 类型的值 类型 float 与类型 int 不兼容

  type t('a) =
    | One: t(int)
    | Two: t(float);

  let x =
    fun
    | One => None
    | Two => None;

现在在某种程度上，如果这是关于函数的返回类型，这对我来说是有意义的。

我找到了一个等价问题的答案（我认为）。对于第二部分，答案似乎是忽略构造函数的绑定类型。在 ReasonML 中是否可能相同？

Ps：请在术语上迂腐地纠正我，我还在学习什么是什么。

Pps：我知道我可以通过显式键入来解决原始问题，x但我真的很喜欢fun它的语法，因为它很有趣。

Answer 1

简短的回答是 GADT 使类型系统的表现力太强而无法完全推断。例如，在您的情况下，以下函数都是总计的（也就是它们处理其输入的所有可能值

let one = (One) => None
let two = (Two) => None

您可以通过在 OCaml 语法中添加显式反驳子句来检查它们是否总计（原因语法尚未更新以包含这些）：

let one = function
| One -> None
| _ -> .

这里的点.表示子句左侧描述的模式在语法上是有效的，但由于某些类型限制而不指代任何实际值。

因此，您需要告诉类型检查器您打算匹配t(a)any类型的值a，这需要使用本地抽象类型来完成：

let x (type a, (x:t(a))) = switch(x){
| One => None
| Two => None
}

有了这个局部抽象注解，类型检查器就知道它不应该a全局地用具体类型替换这个变量（也就是它应该考虑局部a是某种未知的抽象类型），但它可以在匹配 GADT 时在局部细化它。

严格来说，注解只需要在模式上，这样你就可以写

let x (type a) = fun
| (One:t(a)) => None
| Two => None

请注意，对于带有 GADT 的递归函数，您可能需要使用完整的显式多态局部抽象类型符号：

type t(_) =
| Int(int): t(int)
| Equal(t('a),t('a)):t(bool)

let rec eval: type any. t(any) => any = fun
| Int(n) => n
| Equal(x,y) => eval(x) = eval(y)

不同之处在于 eval 是递归多态的。请参阅https://caml.inria.fr/pub/docs/manual-ocaml-4.09/polymorphism.html#sec60。

编辑：注释返回类型

另一个通常需要避免可怕的“这种类型会超出其范围”的注释是在离开模式匹配时添加注释。一个典型的例子是函数：

let zero (type a, (x:t(a)) = switch (x){
| One => 0
| Two => 0.
}

这里有一个歧义，因为在 branch 内部One，类型检查器知道，int=a但是当离开这个上下文时，它需要选择等式的一侧或另一侧。（在这种特定情况下，类型检查器自行决定这(0: int)是一个更合乎逻辑的结论，因为它0是一个整数，并且该类型没有以任何方式与本地抽象类型联系a。）

可以通过在本地使用显式注释来避免这种歧义

let zero (type a, (x:t(a))) = switch (x){
| One => ( 0 : a )
| Two => ( 0. : a )
}

或在整个功能上

let zero (type a): t(a) => a = fun
| One => 0
| Two => 0.