GADT 上的模式匹配失败

我更多地使用 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;

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

我找到了答案（我认为）到一个同等的问题 https://stackoverflow.com/questions/10210269/pattern-matching-and-constructors。对于第二部分，答案似乎是忽略构造函数的绑定类型。 ReasonML 中也可能有同样的情况吗？

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

P.p.s.：我知道我可以通过显式输入来解决最初的问题x但我真的很喜欢fun语法，因为它很有趣。

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

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

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

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

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

因此，您需要告诉类型检查器您打算匹配类型的值t(a)对于任何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 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.
}

这里有一个歧义，因为在分支内部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.