是什麼導致此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的類型系統非常簡單（據我所知）它永遠不會是不可判定的，所以顯式類型註釋永遠不應該是必需的。你爲什麼想把它們放在這裏？