Nur um schnell zu überprüfen, wissen wir, diese Fakten:
- Wenn
s :: sigma -> tau
und t :: rho
und gamma(sigma) = gamma(rho)
dann s t :: gamma(tau)
.
f :: ([a] -> b) -> a -> [b]
g :: c -> Int -> c
Wir möchten die Art der f g
lernen. Es sieht so aus, als ob Regel (1) uns sagen könnte, wenn wir s
, t
, sigma
, tau
, rho
und gamma
entsprechend wählen. Lassen Sie uns ein paar Vermutungen darüber anstellen, wie wir sie angemessen einsetzen können und sehen, wohin uns das führt.
- Seit dem Abschluss (1) sagt
s t :: ...
und wir wollen f g :: ...
wissen, sollten wir wahrscheinlich s = f
und t = g
wählen.
- Seit der Prämisse (1) sagt
s :: sigma -> tau
und wir haben s = f
gewählt und wissen f :: ([a] -> b) -> a -> [b]
aus (2), sollten wir wahrscheinlich wählen sigma = [a] -> b
und tau = a -> [b]
.
- Da die Prämisse von (1) sagt
t :: rho
und wir haben gewählt t = g
und wissen g :: c -> Int -> c
von (3), sollten wir wahrscheinlich rho = c -> Int -> c
wählen.
unsere Entscheidungen Zusammengefasst haben wir nun (1) in dieser Form umgewandelt:
Wenn f :: ([a] -> b) -> a -> [b]
und g :: c -> Int -> c
und gamma([a] -> b) = gamma(c -> Int -> c)
dann f g :: gamma(a -> [b])
.
Es gibt nur eine Variable aus (1), für die wir noch keinen Wert ausgewählt haben, nämlich gamma
.Die dritte Voraussetzung schränkt gamma
ein wenig, nämlich muß es genügen:
gamma([a] -> b) = gamma(c -> Int -> c)
Vermutlich gibt es eine implizite Annahme, dass es wie eine Substitution verhält, das heißt, Typ Strukturen Rekursion über und Variablen vom Typ ersetzt, so dass die vorherige Gleichheit Annahme ist dieser ein Äquivalent:
[gamma(a)] -> gamma(b) = gamma(c) -> Int -> gamma(c)
Für diese Gleichung wahr zu sein, wir alle diese Dinge haben muss:
gamma(c) = [gamma(a)]
gamma(b) = Int -> gamma(c) = Int -> [gamma(a)]
Wenn wir eine willkürliche Wahl für gamma(a)
treffen, sagen uns diese Gleichungen die Ergebnisse von gamma(b)
und gamma(c)
; Lass uns gamma(a) = a
wählen. Dann:
gamma(a) = a
gamma(b) = Int -> [a]
gamma(c) = [a]
Jetzt haben wir die Räumlichkeiten (1) erfüllt, und so lernen wir ihre Schlussfolgerung:
f g :: gamma(a -> [b])
f g :: gamma(a) -> [gamma(b)]
f g :: a -> [Int -> [a]]
Bitte etwas Kontext zu machen. Ein Link zu dem Dokument, wo Sie die Regel erhalten haben, usw. Im Moment ist es unklar, was Gamma bedeutet. –
@WillemVanOnsem Ich wette, dass Gamma eine Substitution ist, so dass \ gamma (\ sigma) = \ gamma (\ rho) bedeutet, dass es eine Möglichkeit gibt, den Typ von "t" mit dem Eingabetyp von 's zu vereinheitlichen '. –