Type variable to be unified occurs in type

问题:

I have a function to reconstruct a tree from 2 lists. I return a list on all branches, but I am getting an error that I don't understand. But I assume it has to do with the return types.

The error is this:

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

The line the error occurs at is the headline of the function definition fun recon (preoH::preoT, inoH::inoT) =

What does that error mean exactly and why does it occur?

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

回答1:

To unify a variable with something means to find a value for the variable that equals that something. For example, we can unify something simple like (I'll use a triple equal to mean that the two terms must be equal):

a === int

The result of the unification is a value that we can substitute a for. In this case we can substitute int for a and the equation will hold (it's similar to solving systems of equations in mathematics):

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

Or we can unify a slightly more complicated equation:

a -> int === bool -> b

Here, we need to find the values that need to be substituted for a and b so that the equation holds. These are bool for a and int for b:

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

I hope you've got the idea by now. In your case, the compiler has to unify this:

a === a list

Well, it's ''a instead of just a in your error message, but we can neglect that for the moment. The thing is that because a appears on both sides, the equation is not unifyable, hence the hint in the error message (emphasis mine) "Type variable to be unified occurs in type". If we'd say that a must be a list and replace a with that on both sides we'd get this:

a list === a list list

We haven't removed the a variable that we need to solve for and we won't anytime soon. That's why the compiler barfs, it leads to an infinite loop and a simple check that the variable doesn't occur on both sides of the equation is a good way to avoid that loop.

Why does it happen in your case? The short version is that you're trying to represent a tree using nested lists and SML's type system can't handle that. The tree you're trying to build in terms of lists looks akin to this:

[[a], a, [a]]

Where a is some generic type variable. Lists are homogeneous containers, they can only contain values of a single type, which means that [a] and a must be of the same type, i.e.:

a === a list

And I've already explained why this leads to an error.

The solution is to use a recursive datatype to representing trees, such as this:

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

This works because it allows us to define it recursively, i.e., the type of the leaves are tree themselves. Your recon function should have ''a tree as its return type.

Hopefully, it's a little clearer now.

回答2:

1. Ionut gave a comprehensive explanation of how type unification works, so here is a hint:

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

   The first element has type 'a and the second element has type 'a list.

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

   The second element has type 'a and the first and third element have type 'a list.

2. When you check lists for being empty, consider using null preoT, or handle the case using pattern matching.