Was verursacht diesen Standard-ML-Typfehler?

Question

Ich habe versucht, eine tail-rekursive Version dieser sehr einfachen SML-Funktion zu erstellen:

fun suffixes [] = [[]]
  | suffixes (x::xs) = (x::xs) :: suffixes xs;

Dabei habe ich Typanmerkungen zu den Parametern verwendet.Der folgende Code zeigt dies und verursacht einen Typfehler (siehe unten). Wenn ich hingegen einfach die Typanmerkungen entferne, akzeptiert SML dies problemlos und gibt der gesamten Funktion dieselbe Signatur wie der einfacheren Funktion oben.

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;

Fehler:

$ 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

Es sind zwei Fehler angegeben.Letzteres scheint hier weniger wichtig zu sein, eine Diskrepanz zwischen den beiden Klauseln von suffixes_helper.Das erste ist das, was ich nicht verstehe.Ich kommentiere, um anzugeben, dass der erste Parameter vom Typ ist 'a:list und dass der zweite Parameter vom Typ ist 'b:list.Sollte der Inferenzalgorithmus vom Typ Hindley-Milner, der nach meinem Verständnis auf der allgemeinen Vereinheitlichung basiert, nicht in der Lage sein, zu vereinheitlichen? 'b:list mit 'a:list list, mit einer Substitution von 'b ---> 'a list?

BEARBEITEN:Eine Antwort deutet darauf hin, dass es möglicherweise etwas damit zu tun hat, dass der Typinferenzalgorithmus abgeleitete Typen nicht zulässt, die in gewissem Sinne strenger sind als die in den Typanmerkungen angegebenen.Ich würde vermuten, dass eine solche Regel nur für Anmerkungen zu Parametern und zu einer Funktion als Ganzes gelten würde.Ich habe keine Ahnung, ob das richtig ist.Auf jeden Fall habe ich versucht, die Typanmerkungen in den Funktionskörper zu verschieben, und ich erhalte die gleiche Fehlermeldung:

fun suffixes_helper [] acc = []::acc
    | suffixes_helper (x::xs) acc =
          suffixes_helper (xs:'a list) (((x::xs)::acc):'b list);

Der Fehler ist jetzt:

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

Bei SML bin ich mir nicht sicher, aber F#, eine andere funktionale Sprache, gibt in solchen Situationen eine Warnung aus.Einen Fehler anzugeben mag etwas hart sein, aber es macht Sinn:Wenn der Programmierer eine zusätzliche Variable vom Typ „b“ einführt und „b vom Typ „a“ sein muss, ist die Funktion möglicherweise nicht so allgemein wie vom Programmierer beabsichtigt, was einen Bericht wert ist.

Answer 2

Das funktioniert:

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

Wie Joh und newacct sagen, ist 'b list zu verlieren. Wenn Sie die explizite Typanmerkung geben

fun suffixes_helper (_ : 'a list) (_ : 'b list) = ...

es wird implizit als

quantifiziert

fun suffixes_helper (_ : (All 'a).'a list) (_ : (All 'b).'b list) = ...

und offensichtlich 'b = 'a list kann nicht wahr (All a') und (All b') gleichzeitig.

Ohne die explizite Typanmerkung, Typinferenz kann das Richtige tun, die die Art zu vereinen ist. Und wirklich, SML des Typ-System ist einfach genug, dass (soweit mir bekannt), ist es nie unentscheidbar, so explizit Typenannotationen sollen niemals erforderlich sein. Warum wollen Sie sie hier setzen wollen?

Answer 3

Wenn Sie Typvariablen wie 'a und 'b verwenden, das bedeutet, dass 'a und 'b können auf alles unabhängig . So zum Beispiel sollte es funktionieren, wenn ich entscheiden, dass 'b war int und 'a war float; aber offensichtlich, dass in diesem Fall nicht gültig, da es stellt sich heraus, dass 'b 'a list werden muss.