Warum funktioniert (+) mit dem Typ (a -> b -> b)?

Question

Falzfunktion:

fold :: b -> (a -> b -> b) -> [a] -> b 
fold z f []  = z 
fold z f (x:xs) = f x (fold z f xs) 

von http://www.seas.upenn.edu/~cis194/spring13/lectures/04-higher-order.html genommen

Prelude> :t (+) 
(+) :: Num a => a -> a -> a 

*Main> fold (0) (+) [1,2,3] 
6 

Was a -> a -> a für (+) Funktion mit Typ (a -> b -> b) Spiel nicht geben?

Da die Falzdefinition den Funktionstyp (a -> b -> b) akzeptiert, bedeutet dies, dass die ersten beiden Parameter (a -> b) von verschiedenen Typen sein müssen?

Answer 1

Nein, heißt es nur, dass a und bkönnen unterschiedlich sein, aber es ist nicht zwingend für sie, anders zu sein. In deinem Fall ist es dasselbe.

data SomeType a b = Test a b deriving (Show) 

Jetzt in ghci:

Answer 2

Sie denken, in umgekehrter Richtung

Ein viel einfacheres Beispiel den Punkt zu vermitteln. Sie müssen nicht prüfen, ob + identisch ist oder übereinstimmt a -> b -> b, möchten Sie die Art der + von a -> b -> b eine Spezialisierung sein und diese Sie die Typen zu vereinigen müssen, um zu überprüfen.

Vereinheitlichung bedeutet, dass Sie sehen wollen, ob die Art der + und die Art a -> b -> b kann durch Umbenennen der Typvariablen gleich gemacht werden.

Also + hat Typ Num x => x -> x -> x. Lassen Sie uns jetzt die Klassenbeschränkung ignorieren und sehen wir, ob wir die funktionalen Typen zuordnen können. Die Typen werden x -> x -> x und a -> b -> b. In der Tat ist es besser, wenn wir sie so betrachten, wie sie wirklich sind, ohne Assoziativität zu verwenden: x -> (x -> x) und a -> (b -> b).

Der -> ist ein Typ Ersteller. I.e. Es ist eine Funktion, die eine bestimmte Anzahl von Typen einem anderen Typ zuordnet. In diesem Fall ordnet der Konstruktor -> zwei Typen t_1 und t_2 dem Funktionstyp (->) t_1 t_2 zu (der üblicherweise mit t_1 -> t_2 bezeichnet wird).

So x -> (x -> x) der Typ ist eigentlich (->) x ((->) x x) die der Typkonstruktor ist -> angewendet x und an den Typkonstruktor -> angewendet x und x. Der andere Typ ist (->) a ((->) b b).

Bei der Vereinheitlichung berücksichtigen Sie den äußersten Typkonstruktor für die beiden Typen (-> für beide in diesem Fall). Wenn dies nicht übereinstimmt, können Sie nicht vereinheitlichen. Andernfalls müssen Sie die Argumente des Konstruktors vereinheitlichen.

Also müssen wir x mit a vereinheitlichen. Sie sind beide Typ Variablen, so können wir einer von ihnen umbenennen. Nehmen wir an, dass wir a mit x umbenennen. Nun wenden wir die Umbenennung auf die Typen an, erhalten: (->) x ((->) x x) und (->) x ((->) b b) und Sie sehen, dass x und x jetzt übereinstimmen.

Betrachten wir das zweite Argument. Es ist keine Typvariable, daher müssen wir den Typkonstruktor anpassen, und dies ist wiederum -> für beide. Wir gehen also rekursiv auf die Argumente ein.

Wir möchten x und b entsprechen. Sie sind beide Typvariablen, daher können wir eine davon umbenennen. Nehmen wir an, wir benennen x in b um. Wir wenden diese Ersetzung auf die Typen an und erhalten: (->) b ((->) b b) und (->) b ((->) b b). Jetzt passt alles zusammen. Daher vereinheitlichen sich die beiden Typen.

In Bezug auf die Klasse Einschränkung, wenn wir umbenennen x mit b wir die Substitution der Einschränkung angewendet zu so wurde Num xNum b und die beiden letzten Arten sind beide Num b => b -> b -> b.

Ich hoffe, dies gab Ihnen ein besseres Verständnis darüber, wie die Typen funktionieren und wie die Typen überprüft werden.

---

Seitennotiz: Dies ist, was Harkell bei der Durchführung von Typ-Inferenz tut. Er weist einer unbekannten Funktion zunächst eine neue Typvariable t zu. Dann verwendet es Vereinheitlichung, um den Typ des Ausdrucks zu erhalten, der es definiert, und zu prüfen, welcher Typ mit t verknüpft wurde, und dies ist der Typ der Funktion.