ML型错误？
我试图对这个非常简单的SML函数做一个尾递归版本：
fun suffixes [] = [[]]
| suffixes (x::xs) = (x::xs) :: suffixes xs;
在此过程中，我在参数中使用了类型注释。 下面的代码显示了这一点，并导致了一个类型错误（下面给出），而如果我只是删除类型注释，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 。 我不知道Hindley-Milner类型推理算法是否可以将统一'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 。
上一篇: ML type error?