是什么导致此Standard-ML类型错误？

Question

我试图让这个非常简单的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 

有给出了两个错误。后者在这里似乎不那么重要，后缀的两个子句之间不匹配。第一个是我不明白的。我注释说第一个参数的类型是'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 

Answer 1

我不知道SML ，但另一种功能语言F＃在这种情况下给出警告。给出一个错误可能有点苛刻，但它是有道理的：如果程序员引入了一个额外的类型变量'b，并且'b必须是类型'列表，那么函数可能不像程序员想要的那样通用，值得报道。

Answer 2

当您使用类型的变量，比如'a和'b，这意味着'a和'b可以设置为什么，独立。因此，例如，如果我决定'b是int和'a是float;但显然这在这种情况下是无效的，因为事实证明'b必须是'a list。

Answer 3

这工作：

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的类型系统非常简单（据我所知）它永远不会是不可判定的，所以显式类型注释永远不应该是必需的。你为什么想把它们放在这里？