1

Momentan bereite ich mich auf meine Prüfungen vor und das ist etwas über Haskell, das ich nie wirklich verstanden habe.Wie finde ich den Typ einer Haskell-Funktion heraus?

Die Art der Regel ist die folgenden

"und" Mittel "und" in deutscher Sprache.

So sind die gegebenen Funktionen sind

f :: ([a] -> b) -> a -> [b] 
g :: c -> Int -> c 

Und jetzt muss ich (f g) die Art bestimmen, indem die Art der Regel oben. Kann mir jemand erklären, wie ich an dieser Stelle vorgehen soll?

+0

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. –

+3

@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 '. –

Antwort

4

Nur um schnell zu überprüfen, wissen wir, diese Fakten:

  1. Wenn s :: sigma -> tau
    und t :: rho
    und gamma(sigma) = gamma(rho)
    dann s t :: gamma(tau).
  2. f :: ([a] -> b) -> a -> [b]
  3. 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]] 
Verwandte Themen