ML не может объединить 'с 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

Я создал (строка * 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 не может объединить с int?

Answer 1

Вы можете получить подобное сообщение, если у вас есть переопределенное дерево и вы удалите его на верхнем уровне, так как вы определили a. Жалуется, что дерево в не совпадает с деревом в удалении.

Например

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