Ich versuche zu verstehen, warum die Funktion
%Vor%hat den Typ
%Vor%Wie kann "filter fst" funktionieren, wenn der Filter eine Funktion erhalten muss, die einen Bool-Typ zurückgibt und fst nur das erste Element eines Tupels zurückgibt?
%Vor%Kann mir jemand das erklären? Danke;)
Wie kann "filter fst" funktionieren, wenn der Filter eine Funktion erhalten muss, die einen Bool-Typ zurückgibt und fst nur das erste Element eines Tupels zurückgibt?
In gewissem Sinne haben Sie Ihre eigene Frage beantwortet! Lass es uns aufteilen:
filter muss eine Funktion erhalten, die einen Bool-Type
zurückgibt
OK, also schauen wir uns an, was Sie weitergeben: fst
. Ist fst
eine Funktion? Ja, ist es, also haben wir den ersten Teil runter. Gibt es Bool
zurück? Nun, schauen wir uns an, was es macht:
fst gibt nur das erste Element eines Tupels zurück
Wenn also das erste Element eines Tupels ein Bool
ist, dann gibt es ja ein bool! Wenn das erste Element eines Tupels etwas anderes als Bool
ist, wird die Typprüfung jedoch nicht ausgeführt und wird auch nicht ausgeführt.
Sehen wir uns noch einmal die Typen an, die Sie aufstellen. Ich werde die Namen der Typvariablen ändern, nur um die Dinge klarer zu machen:
%Vor% fst
nimmt eine (b, c)
und gibt eine b
zurück, und der Filter erwartet eine Funktion, die eine a
und eine Bool
zurückgibt. Wir geben fst
weiter, also muss a
über (b, c)
sein, da dies der erste Parameter von fst
ist. Der Rückgabewert der Funktion, die wir in filter
übergeben, muss ein Bool
sein, also muss b
oben ein Bool
sein. Und c
kann alles sein, weil es überhaupt nicht vom Filter verwendet wird. Durch Einsetzen der Werte für a
und b
erhalten wir einen endgültigen Typ für filter fst
von:
Schließlich ist der Typ von map
:
(Auch hier habe ich die Typvariablen umbenannt, nur um sie von den oben genannten Typen zu unterscheiden, aber denken Sie daran, dass es nicht wirklich wichtig ist, wie sie heißen, solange sie konsistent sind Umfang der Typ Annotation)
map (filter fst)
übergibt den oben definierten filter fst
als ersten Parameter an map
. Wenn wir den Parameter für d
und das Ergebnis für e
ersetzen, können wir sehen, dass diese Funktion [(Bool, c)] -> [(Bool, c)]
sein muss, mit anderen Worten, sowohl d
als auch e
sind (Bool, c)
. Wenn wir diese in die Funktion einbinden, gelangen wir zum endgültigen Typ:
Aber wir könnten auch Typvariablen für fst
austauschen, um:
Also hat das erste Argument von filter
den Typ a -> Bool
, während fst
selbst (c,b) -> c
ist. Jetzt versuchen wir, dies zu kombinieren (ich glaube, das wird Vereinigung genannt):
Daraus können wir schließen, dass c
Bool
sein muss (da die rechte Seite gleich sein muss) und erhalten:
Aus dem Obigen folgern wir, dass a
(Bool,b)
sein muss, und erhalten:
Und wir sind fertig.
Da ich dies bereits geschrieben habe, bevor danielpwrights Antwort gepostet wurde, poste ich es trotzdem. Ich gehe gerade meinen Denkprozess für den Typ von filter fst
durch.
Schreiben Sie zuerst die Typ-Signaturen auf (ändern Sie fst, damit seine Variablennamen nicht mit denen des Filters kollidieren):
%Vor% Übereinstimmung (a -> Bool)
mit ((b, c) -> b)
:
b
muss Bool
sein, was bedeutet, dass a
(Bool,c)
Durch die Spezialisierung von filter
mit dieser Information wird es:
was zu
führt %Vor%Sie müssen wirklich nur einige Gleichungen lösen. Fangen wir an:
%Vor% Daher ist filter fst :: [a] -> [a]
wobei a
die Lösung der folgenden Gleichung ist:
was impliziert
%Vor%was impliziert
%Vor% Daher filter fst :: [(Bool, c)] -> [(Bool, c)]
.
Jetzt haben wir:
%Vor% Also, map (filter fst) :: [a] -> [b]
, wobei a
und b
durch die folgende Typgleichung gegeben sind:
was impliziert
%Vor% Daher map (filter fst) :: [[(Bool, c)]] -> [[(Bool, c)]]
.
Wie andere getan haben, möchte ich hier die Typgleichungen lösen; aber ich möchte sie auf eine visuellere Weise aufschreiben, damit die Ableitung auf eine automatische Weise durchgeführt werden kann. Mal sehen.
%Vor%Rein mechanisches Zeug. :) Damit,
%Vor%Die Typvariablen im letzten Typ können zur besseren Lesbarkeit frei umbenannt werden (in einer konsistenten Art und Weise).
Das einzige, was meine Antwort zu dem, was bereits in anderen Antworten gezeigt wurde, hinzufügt, ist dieser Rat (den ich für wichtig halte): Wenn Sie dieser einfachen Disziplin folgen, eine Sache unter die andere zu schreiben wird es sehr einfach, diese Typ-Vereinheitlichungen sehr mechanisch und automatisch durchzuführen (wodurch die Möglichkeit von Fehlern verringert wird).
Für ein weiteres Beispiel, einschließlich eines eigentlichen Prolog-Programms zur Typableitung, siehe Haskell: wie man den Typ von ein Ausdruck manuell .
Tags und Links haskell functional-programming types type-inference unification