ML 无法将 'a 与 int 统一起来

Question

练习是在 ML 中编写一个从二叉搜索树中删除元素的函数。 代码如下：

datatype 'a tree = Lf | Br of 'a * 'a tree * 'a tree;

fun deleteTop (Br(_, Lf, t2)) = t2
  | deleteTop (Br(_, t1, Lf)) = t1
  | deleteTop (Br(_, Br(v, u1, u2), t2)) =
    Br(v, deleteTop (Br(v, u1, u2)), t2);

fun delete (Lf, k : string) = Lf
  | delete (Br((a,b),t1,t2), k) =
    if a=k then deleteTop(Br((a,b),t1,t2))
    else if k<a then Br((a,b),delete(t1,k),t2)
            else Br((a,b),t1,delete(t2,k));

当我将它加载到 Poly/ML 中时，它会警告我 deleteTop 中的模式匹配不完整，但这并不重要，因为 delete 只会传递 deleteTop 一个分支。

val deleteTop = fn: 'a tree -> 'a tree
val delete = fn: (string * 'a) tree * string -> (string * 'a) tree

我创建了一个 (string * int) 树并运行

> delete(a,"they");
Error-Type error in function application.
   Function: delete : (string * 'a) tree * string -> (string * 'a) tree
   Argument: (a, "they") : (string * int) tree * string
   Reason:
      Can't unify (string * 'a) tree with (string * int) tree
      (Different type constructors)
Found near delete (a, "they")
Static Errors

让我重申其中的一行：

Can't unify (string * 'a) tree with (string * int) tree

为什么 ML 不能统一 'a 和 int？

Answer 1

如果您在定义 a 后在顶层重新定义了 tree 和 delete，您会收到类似的消息。它抱怨 a 中的 tree 与 delete 中的 tree 不同。

例如

> datatype 'a t = T of 'a;
datatype 'a t = T of 'a
> val x = T 1;
val x = T 1: int t
> datatype 'a t = T of 'a;
datatype 'a t = T of 'a
> val T y = x;
Pattern and expression have incompatible types.
   Pattern: T y : 'a t
   Expression: x : int t
   Reason: Can't unify 'a t with int t (Different type constructors)
Found near val T y = x
Static Errors
>