是什么原因导致这个标准-ML类型的错误?
-
13-09-2019 - |
题
我试图使这个非常简单的SML功能的尾递归版本:
fun suffixes [] = [[]]
| suffixes (x::xs) = (x::xs) :: suffixes xs;
在这个过程中,我使用的PARAMATERS类型的注释。下面的代码显示这一点,并导致一种类型的误差(以下给出),而如果我只需卸下类型注释,SML没有问题接受它,从而整体功能相同的签名与上述较简单的功能。
fun suffixes_tail xs =
let
fun suffixes_helper [] acc = []::acc
| suffixes_helper (x::xs:'a list) (acc:'b list) =
suffixes_helper xs ((x::xs)::acc)
in
suffixes_helper xs []
end;
错误:
$ sml typeerror.sml
Standard ML of New Jersey v110.71 [built: Thu Sep 17 16:48:42 2009]
[opening typeerror.sml]
val suffixes = fn : 'a list -> 'a list list
typeerror.sml:17.81-17.93 Error: operator and operand don't agree [UBOUND match]
operator domain: 'a list * 'a list list
operand: 'a list * 'b list
in expression:
(x :: xs) :: acc
typeerror.sml:16.13-17.94 Error: types of rules don't agree [UBOUND match]
earlier rule(s): 'a list * 'Z list list -> 'Z list list
this rule: 'a list * 'b list -> 'Y
in rule:
(x :: xs : 'a list,acc : 'b list) =>
(suffixes_helper xs) ((x :: xs) :: acc)
/usr/local/smlnj-110.71/bin/sml: Fatal error -- Uncaught exception Error with 0
raised at ../compiler/TopLevel/interact/evalloop.sml:66.19-66.27
有给出两个错误。后者似乎不那么重要的位置,suffixes_helper的两个分句之间的不匹配。首先是一个我不明白。我注释声明,所述第一参数是类型'a:list
的,并且第二参数是类型'b:list
的。不应将辛德米尔纳类型推理算法,其被构建为我理解一般统一顶的,能够统一与'b:list
'a:list list
,使用'b ---> 'a list
的取代?
编辑:的回答表明,它可能有一些做的类型推理算法不允许推断类型,其在某种意义上是不是通过类型注释给出的那些更加严格。我猜想,这样的规则只适用于注解参数和功能为一体。我不知道这是否是正确的。在任何情况下,我试图转移到功能体移动的类型的注释,我也得到相同的排序错误的:
fun suffixes_helper [] acc = []::acc
| suffixes_helper (x::xs) acc =
suffixes_helper (xs:'a list) (((x::xs)::acc):'b list);
现在的错误是:
typeerror.sml:5.67-5.89 Error: expression doesn't match constraint [UBOUND match]
expression: 'a list list
constraint: 'b list
in expression:
(x :: xs) :: acc: 'b list
解决方案
我不知道SML,但F#,另一种功能性语言,给出了这种情况的警告。给了一个错误可能有点苛刻,但它是有道理的:如果程序员引入了额外的类型变量“B,如果” B必须是类型列表”,该功能可能不会像一般的程序员预期,这值得报告。
其他提示
此工作的:
fun suffixes_tail xs =
let
fun suffixes_helper [] acc = []::acc
| suffixes_helper (x::xs:'a list) (acc:'a list list) =
suffixes_helper xs ((x::xs)::acc)
in
suffixes_helper xs []
end
如荷兰Joh和newacct说,'b list
太松。当你给了明确的类型注释
fun suffixes_helper (_ : 'a list) (_ : 'b list) = ...
它是隐式定量为
fun suffixes_helper (_ : (All 'a).'a list) (_ : (All 'b).'b list) = ...
和明显'b = 'a list
不可能是真的(All a')
和强> (All b')
同时
如果没有明确的类型注释,类型推断可以做正确的事情,这是统一类型。真的,SML的类型系统非常简单,(据我所知),这是从来没有不可判定的,所以显式类型注释不应该是必要的。你为什么要把他们会在这里?
当您使用的类型变量像'a
和'b
,这意味着'a
和'b
可以被设置为任何,独立地。因此,例如,它应该工作,如果我决定'b
是int
和'a
是float
;但很明显,因为事实证明,'b
必须'a list
不是在这种情况下有效。