GADT上的模式匹配失败 [英] Pattern matching on a GADT fails

问题描述

我在使用ReasonML进行了更多操作，并从以下示例中发现type t上的模式匹配无法正常工作

I was playing around a bit more with ReasonML and found pattern matching on type t from the following example to not be working with the error

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

Error: This pattern matches values of type t(float) but a pattern was expected which matches values of type t(int) Type float is not compatible with type int

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

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

从某种程度上来说，如果这与函数的返回类型有关，那么这对我来说很有意义.

Now on some level this makes sense to me if this was about the return type of a function.

我找到了一个答案(我认为)一个等效问题.对于第二部分，答案似乎是有点忽略构造函数的绑定类型.在ReasonML中是否可能相同?

I found an answer (I think) to an equivalent question. For the second section the answer seems to be to kinda ignore the bound type of the constructor. Is the same possible in ReasonML?

P.s .:请对术语进行书呆子的纠正，我仍在学习什么.

P.s.: please correct me pedantically on terminology, I'm still learning what's what.

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

P.p.s.: I know I could work around the original problem by explicitly typing x but I really like the fun syntax because it's fun.

推荐答案

简单的答案是GADT使得类型系统的表现力太强而无法完全推断出来. 例如，在您的情况下，以下两个函数都是合计的(aka它们处理输入的所有可能值

The brief answer is that GADTs make the type system too expressive to be fully inferred. For instance, in your case, the following functions are both total (aka they handle all possible values of their input

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

您可以通过在OCaml语法中添加显式的反驳子句来检查它们的总和(原因语法尚未更新为包括这些子句):

You can check that they are total by adding an explicit refutation clause in OCaml syntax (Reason syntax has not yet be updated to include those):

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

在这里，点.表示该子句左侧描述的模式在语法上是有效的，但由于某些类型约束而未引用任何实际值.

Here the dot . means that the pattern described on the left-hand side of the clause is syntactically valid, but does not refer to any actual value due to some type constraints.

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

Consequently, you need to tell the type checker that you intend to match of a value of type t(a) for any a, this needs to be done with locally abstract types:

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

使用此局部抽象注释，类型检查器知道不应将其替换为全局具体类型的变量(c5)(aka应该认为局部a是某种未知的抽象类型)，但可以匹配GADT时在本地进行优化.

With this locally abstract annotation, the type checker knows that it is not supposed to replace this variable a by a concrete type globally (aka it should consider that locally a is some unknown abstract type), but it can refine it locally when matching a GADT.

严格来说，仅在模式上需要注释，因此您可以编写

Strictly speaking, the annotation is only needed on the pattern, thus you can write

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

请注意，对于带有GADT的递归函数，您可能需要使用完全显式的多态局部抽象类型表示法:

Note that for recursive functions with GADTs, you may need to go for the full explictly polymorphic locally abstract type notations:

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 .

where the difference is that eval is recursively polymorphic. See https://caml.inria.fr/pub/docs/manual-ocaml-4.09/polymorphism.html#sec60 .

注释返回类型

为避免可怕的此类型将逃脱其作用域"，通常需要使用另一个注释，即在保留模式匹配时添加一个注释. 一个典型的例子是函数:

Another annotation that is often needed to avoid the dreaded "this type would escape its scope" is to add an annotation when leaving a pattern matching. A typical example would be the function:

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

这里有一个歧义，因为在分支One中，类型检查器知道int=a，但是在离开此上下文时，它需要选择方程式的一侧或另一侧. (在这种特定情况下，类型检查器将(0: int)留在自己的设备上，因为0是整数，并且该类型未与本地抽象类型a进行任何接触，因此它决定了逻辑上的结论. )

There is an ambiguity here because inside the branch One, the typechecker knows that int=a but when leaving this context, it needs to choose one side of the equation or the other. (In this specific case, left at its own device the typechecker decides that (0: int) is the more logical conclusion because 0 is an integer and this type has not been in contact in any way with the locally abstract type a .)

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

This ambiguity can be avoided by using an explicit annotation, either locally

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.

这篇关于GADT上的模式匹配失败的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！