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

Question

我试图为这个非常简单的 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 替换 ---> '列表？

编辑：一个答案表明它可能与不允许推断类型的类型推断算法有关，从某种意义上说，推断类型比类型注释给出的类型更严格。我猜想这样的规则仅适用于参数和整个函数的注释。我不知道这是否正确。无论如何，我尝试将类型注释移至函数体，但我得到了同样的错误：

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

这有效：

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 不能为 true (All a') and (All b') 同时进行。

如果没有显式类型注释，类型推断可以做正确的事情，即统一类型。实际上，SML 的类型系统非常简单（据我所知），它永远不会是不可判定的，因此显式类型注释永远都不是必要的。为什么要把它们放在这里？

Answer 2

当您使用 'a 和 'b 等类型变量时，这意味着 'a 和 'b 可以是设置为任意，独立。例如，如果我确定 'b 是 int 且 'a 是 float，那么它应该可以工作；但显然在这种情况下这是无效的，因为事实证明 'b 必须是 'a list。

Answer 3

我不确定 SML，但另一种函数式语言 F# 在这种情况下会发出警告。给出错误可能有点苛刻，但这是有道理的：如果程序员引入了额外的类型变量 'b，并且 'b 必须是 'a 列表类型，则该函数可能不会像程序员预期的那样通用，这值得报道。