Тип, подлежащий объединению, имеет тип

Question

У меня есть функция восстановления дерева из 2 списков. Я возвращаю список во всех ветвях, но я получаю сообщение об ошибке, которое я не понимаю. Но я предполагаю, что это связано с типами возврата.

Ошибка заключается в следующем:

Can't unify ''a with ''a list (Type variable to be unified occurs in type) Found near recon 
(::(preoH, preoT), ::(inoH, ...)) 
Exception- Fail "Static errors (pass2)" raised 

Линия ошибка происходит в то заголовок определения функции fun recon (preoH::preoT, inoH::inoT) =

Что это означает, что ошибка именно и почему это происходит?

(* Reconstruts a binary tree from an inorder and a preorder list. *) 
fun recon (preoH::preoT, inoH::inoT) = 
    (* Case 0: Leaf reached*) 
    if 
     preoT = [] andalso inoT = [] andalso preoH = inoH 
    then 
     [preoH] 
    else 
     let 
     (* split the list of nodes into nodes to the left and nodes to the 
     right of preoH; ST stands for subtree *) 
     val (inoLST, inoRST) = splitat (inoH::inoT, preoH) 
     val (preoLST, preoRST) = splitafter (preoT, last(inoLST)) 
     in 
     (* Case 1: Unary branch encountered, make preoH the parent node of the 
     subtree and combine the left and right preorder and inorder lists*) 
     if 
       length(inoLST) <> length(preoLST) 
     then 
      [preoH, recon (preoLST@preoRST, inoLST@inoRST)] 
     (* Case 2: Binary branch encountered, proceed as normal *) 
     else 
       [recon (preoLST, inoLST), preoH, recon (preoRST, inoRST)] 
     end; 

Answer 1

Унифицировать переменную с чем-то означает найти значение для переменной, которая равна чему-то. Например, мы можем объединить что-то простое, как (я буду использовать тройной равно означает, что оба условия должны быть равны):

a === int 

Результатом объединения является значением, которое мы можем заменить a для. В этом случае мы можем заменить int для a и уравнение будет держать (это похоже на решение систем уравнений в области математики):

a: int 
----------- 
int === int 

Или мы можем унифицировать несколько более сложное уравнение:

a -> int === bool -> b 

Здесь нам нужно найти значения, которые необходимо заменить на a и b, чтобы это уравнение выполнялось. Это bool для a и int для b:

a: bool 
b: int 
--------------------------- 
bool -> int === bool -> int 

Я надеюсь, что вы получили эту идею сейчас. В вашем случае, компилятор должен унифицировать это:

a === a list 

Ну, это ''a вместо того, чтобы просто a в сообщении об ошибке, но можно пренебречь, что на данный момент. Дело в том, что, поскольку a появляется с обеих сторон, уравнение не унифицируется, поэтому подсказка в сообщении об ошибке (выделение мое) «Тип переменная будет унифицирована встречается в типе». Если мы скажем, что a должен быть a list и заменить a с этим с обеих сторон мы получим следующее:

a list === a list list 

Мы не удалили переменную a, что нам нужно решить, и мы не будем в ближайшее время. Вот почему компилятор barfs, это приводит к бесконечному циклу, и простая проверка того, что переменная не встречается с обеих сторон уравнения, является хорошим способом избежать этого цикла.

Почему это происходит в вашем случае? Краткая версия заключается в том, что вы пытаетесь представить дерево с помощью вложенных списков, и система типов SML не может справиться с этим. Дерево вы пытаетесь построить в терминах списков выглядит сродни этому:

[[a], a, [a]] 

Где a это некоторые общие переменную типа.Списки являются однородными контейнеры, они могут содержать только значения одного типа, что означает, что [a] и a должны быть того же типа, т.е .:

a === a list 

И я уже объяснил, почему это приводит к ошибке.

Решение использовать рекурсивную datatype для представляющих деревьев, таких, как это:

datatype 'a tree = 
    Leaf 
| Node of { value : 'a, left: 'a tree, right: 'a tree } 

Это работает, потому что позволяет определить рекурсивно, то есть, тип листьев являются tree сами. Ваша функция recon должна иметь ''a tree в качестве возвращаемого типа.

Надеюсь, теперь это немного яснее.

Answer 2

1. Йонут дал исчерпывающее объяснение того, как работает объединение типа, так вот подсказка:

   [preoH, recon (preoLST@preoRST, inoLST@inoRST)] 
   

   Первый элемент имеет тип «а и второй элемент имеет тип » список.

   [recon (preoLST, inoLST), preoH, recon (preoRST, inoRST)] 
   

   Второй элемент имеет тип «а и первый и третий элемент имеет тип » список.

2. Когда вы проверяете списки на наличие пустого места, подумайте об использовании null preoT или обработайте случай, используя соответствующий шаблон.