OCaml GADTs - 模式匹配匹配错误类型的参数

Question

我必须使用广义代数数据类型实现完美平衡的二叉树（或简称 PBT）。我已经了解 GADT 的一般工作方式以及为了使其在 OCaml 中工作而必须使用的（有点难看的）语法。然后我必须实现一些与它一起工作的功能。现在，我遇到一个函数的问题，该函数采用两个 PBT，它们的节点中存储了整数，returns 一个 PBT，它在其节点中存储每个对应节点的总和。好的。听起来很容易。这是我为 PBT 数据类型编写的代码：

(*Important in order to define the index of the level of our perfectly 
balanced tree*)
(*Natural numbers, Peano style (now with GADTs)*)
type zero = Zero
type _ succ = Succ : 'natural -> 'natural succ

(*Implementing the perfectly balanced binary tree - or PBTree - with GADTs*)
(*'a -> type of tree | _ -> index of level*)

type ('a, _) pbtree =
(*Base case: empty tree - level 0, rock-bottom*)
EmptyTree : ('a, zero) pbtree
(*Inductive case: regular PBTree - tree on the left, value, tree on the 
right*)          
| PBTree : ('a, 'natural) pbtree * 'a * ('a, 'natural) pbtree -> ('a, 
'natural succ) pbtree

到目前为止一切正常。该类型可以编译，我什至设法实现了翻转功能（return PBT 的镜像）。现在真正的问题来自于这个小家伙：

let rec add : type int natural. 
(int, natural) pbtree -> (int, natural) pbtree -> (int, natural) pbtree =
function
| EmptyTree, EmptyTree -> EmptyTree
| PBTree(left1, value1, right1), PBTree(left2, value2, right2) -> 
PBTree((add left1 left2), value1 + value2, (add right1, right2))

在我为空树做模式匹配的地方，它给了我以下错误：

| EmptyTree, EmptyTree -> EmptyTree

Error: This pattern matches values of type 'a*'b
       but a pattern was expected which matches values of type
         (int, natural) pbtree

如果我让函数采用一对树，我可以解决这个问题。它最终会稍微改变归纳案例，函数看起来像这样：

let rec add : type int natural. (int, natural) pbtree * (int, natural)         
pbtree -> (int, natural) pbtree =
function
| EmptyTree, EmptyTree -> EmptyTree
| PBTree(left1, value1, right1), PBTree(left2, value2, right2) -> 
PBTree((add (left1, left2)), value1 + value2, (add (right1, right2)))

然而，这不是我应该做的。我的函数需要接受两个参数。即使进行了解决 pair 类型难题的修改，也会出现以下错误：

Error: This pattern matches values of type int/1805
        but an expression was expected of type int/1

所以我采用的第一种方法是我能做的最好的。我的问题是：为什么模式匹配在明显不存在的情况下检测到一对？为什么它不能像通常那样检测到两个参数？这是我编写检测该模式的函数的方式吗？

如果我假设在创建函数时使用第二种方法（将一对 PBT 作为参数而不是两个参数 - 两个 PBT），那么为什么它不能识别整数值 I我试图给它计算？可能是因为它的工具太多而无法使用？

我不明白这里出了什么问题，如果我试图修改类型以缓解这种语法限制，那么我冒着创建一个违反其自身定义的 PBT 的风险，仅仅是因为该类型允许不相等的分支尺寸。

那么，我再问一次：为什么模式匹配无法识别我在我提供的案例中提供的正确值类型？

Answer 1

您遇到的最后一个错误：

Error: This pattern matches values of type int/1805
       but an expression was expected of type int/1

是说有两种不同的 int 类型不兼容，并为您提供了它们的内部 ID，以便您可以区分它们。发生此错误是因为 type int natural. 创建了两个作用域为函数的新本地抽象类型，这将隐藏该作用域内具有这些名称的任何其他类型。只需不创建名为 int 的本地抽象类型即可解决此错误。然后它将类型变量限制为实际的 int 类型，如预期的那样。

其他错误：

Error: This pattern matches values of type 'a*'b
       but a pattern was expected which matches values of type
         (int, natural) pbtree

出现是因为 EmptyTree, EmptyTree 实际上是匹配一对的模式。在 OCaml 中，如果元组以其他方式分隔，则不需要括号。因此，例如，这是 (int * int) list 类型的有效（且极其混乱）文字：[1, 2; 3, 4; 5, 6].

function 也仅限于一个参数，因此为了匹配多个参数，您需要使用 fun a b -> match a, b with...。或者你可以 add 直接取一个元组。

然后最后你会得到一个错误，因为你在 add right1, right2 中使用逗号分隔函数参数，这将再次被解释为元组。应该是 add right1 right2.

最后的工作（或至少编译）add 函数是：

let rec add : type natural. 
(int, natural) pbtree -> (int, natural) pbtree -> (int, natural) pbtree =
fun a b -> match a, b with
| EmptyTree, EmptyTree -> EmptyTree
| PBTree(left1, value1, right1), PBTree(left2, value2, right2) -> 
PBTree((add left1 left2), value1 + value2, (add right1 right2))

OCaml GADTs - 模式匹配匹配错误类型的参数

OCaml GADTs - pattern matching matches wrong type of argument

pattern-matching

ocaml

gadt