要在类型中发生要统一的类型变量 [英] Type variable to be unified occurs in type

查看:195
本文介绍了要在类型中发生要统一的类型变量的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

我有一个函数从2列表重建树。我返回所有分支上的列表,但我得到一个错误,我不明白。



错误是:

 无法统一一个与一个列表(类型变量要统一发生在类型中)发现附近recon 
(::( preoH,preoT),::( inoH,。 ..))
异常 - 失败静态错误(pass2)引发

错误发生在函数定义的标题 fun recon(preoH :: preoT,inoH :: inoT)=



这个错误是什么意思,为什么会发生?

 (*预订列表*)
fun recon(preoH :: preoT,inoH :: inoT)=
(*情况0:叶达到*)
如果
preoT = [] andalso inoT = [] andalso preoH = inoH
then
[preoH]
else
let
(*将节点列表分成左侧的节点和节点
right of preoH; ST代表子树*)
val(inoLST,inoRST)= splitat(inoH :: inoT,preoH)
val(preoLST,preoRST)= splitafter (inoLST))
in
(*情况1:遇到一元分支,使preoH成为
子树的父节点,并结合左右前置和后续列表*)
if
length(inoLST)<>长度(preoLST)
然后
[preoH,recon(preoLST @ preoRST,inoLST @ inoRST)]
(*情况2:遇到二进制分支,正常进行*)
else
[recon(preoLST,inoLST),preoH,recon(preoRST,inoRST)]
end;


解决方案

对于等于那个东西的变量。例如,我们可以统一一些简单的东西(我将使用三等于意味着两个项必须相等):

  a === int 

统一的结果是一个值, c $ c> a for。在这种情况下,我们可以用 int 替换 a ,方程式将成立(它类似于求解数学方程组):

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

或者我们可以统一一个稍微复杂的方程:

  a  - > int === bool  - > b 

这里,我们需要找到需要替换的值 a b ,以使等式成立。这些 bool 代表 a int $ c> b :

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

我希望你现在有了想法。在你的情况下,编译器必须统一这个:

  a ===列表

好吧,''a ,而不是 / code>在您的错误消息,但我们可以忽略了一会儿。事情是因为 a 出现在两边,方程不是统一的,因此错误消息中的提示(强调我)类型变量统一在类型中发生。如果我们说 a 必须列表并替换 a 两边我们会得到这个:

 一个列表===一个列表



我们没有删除 a 解决和我们不会很快的任何时间。这就是为什么编译器barfs,它导致一个无限循环和一个简单的检查,变量不出现在方程的两边是一个很好的方法,以避免该循环。



为什么会发生在您的情况?简短的版本是,你试图使用嵌套列表来表示一个树,SML的类型系统不能处理它。您在列表中建立的树看起来类似于:

  [[a],a,[a ]] 

其中 a 变量。列表是同类容器,它们只能包含单个类型的值,这意味着 [a] a 是相同类型,即:

  a === a list 

我已经解释过为什么会导致错误。



解决方案是使用用于表示树的递归数据类型,例如:

  datatype' a tree = 
Leaf
|节点{value:'a,left:'a tree,right:'a tree}

因为它允许我们递归地定义它,即叶子的类型是 tree 本身。您的 recon 函数应该有'一个树作为其返回类型。



希望现在有一点清楚。


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;

解决方案

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.

这篇关于要在类型中发生要统一的类型变量的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!

查看全文
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆