Was verursacht diesen Standard-ML-Typfehler?
-
13-09-2019 - |
Frage
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
Lösung
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.
Andere Tipps
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
quantifiziertfun 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?
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.