pattern-matching - OCaml GADTs - pattern matching matches wrong type of argument

Question

I have to implement a perfectly balanced binary tree (or PBT for short) using generalized algebraic data types. I have understood how GADTs work in general and the (somewhat ugly) syntax that I have to use in order for it to work in OCaml. Then I have to implement some functions that work with it. Right now, I am having a problem with a function that takes two PBTs that have integers stored in their nodes and returns a PBT which stores in its nodes the sum of each of its corresponding nodes. Ok. Sounds easy enough. This is the code that I have written for the PBT data type:

(*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

It worked so far. The type compiles and I even managed to do a flip function (return the mirror image of a PBT). Now the real issue comes from this little brat:

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))

Right where I do the pattern matching for the empty tree, it gives me the following error:

| 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

I can solve this if I make the function take a pair of trees. It would end up with the inductive case slightly changed and the function would look like this:

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)))

However, this is not what I am supposed to do. My function needs to take two arguments. Even with this modification that solves the pair type conundrum, it will give the following error:

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

So the first approach I took is the best I can do. My question is: why the pattern matching detects a pair when it is clearly not there? Why can it not detect two arguments like it normally should? Is it the way I wrote the function to detect that pattern?

If I, hypothetically, used the second approach in creating the function (the one where it took a pair of PBTs as an argument instead of two arguments - two PBTs), then why does it not recognise the integer value I am trying to give it to calculate? Is it maybe because it is too instrumented to work with?

I cannot understand what went wrong here and if I tried to modify the type to ease up on this syntactic restriction, then I risk creating a PBT that violates its own definition simply because of the type allowing branches which are unequal in size.

So again, I ask: why does pattern-matching fail to recognise the proper value types that I am giving it in the cases I presented?

标签： pattern-matchingocamlgadt

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))