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

Sie denken in umgekehrter Richtung. Sie müssen nicht überprüfen, ob + identisch ist oder mit a -> b -> b übereinstimmt, Sie möchten, dass der Typ von + eine Spezialisierung von a -> b -> b ist und Sie dies überprüfen müssen > vereinheitliche die Typen.

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

So + hat den Typ Num x => x -> x -> x . Lassen Sie uns die Klassenbeschränkung für jetzt 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 Typkonstruktor . 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 funktionalen Typ (->) t_1 t_2 zu (was normalerweise mit t_1 -> t_2 bezeichnet wird).

Also ist der Typ x -> (x -> x) tatsächlich (->) x ((->) x x) , was der Typkonstruktor -> auf x und der Typkonstruktor -> auf x und x ist. Der andere Typ ist (->) a ((->) b b) .

Bei der Vereinheitlichung betrachten 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 Typvariablen, daher können wir umbenennen . Nehmen wir an, dass wir a mit x umbenennen. Nun wenden wir die Umbenennung auf die Typen an und 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 dem Typkonstruktor entsprechen, und dies ist wiederum -> für beide. Also verfahren wir rekursiv mit den Argumenten.

Wir möchten x und b zuordnen. Sie sind beide Typvariablen, daher können wir eine davon umbenennen. Angenommen, 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.

Wenn wir x mit b umbenennen, haben wir die Substitution auch auf die Bedingung angewendet, so dass Num x zu Num b wurde und die beiden letzten Typen beide Num b => b -> b -> b sind.

Ich hoffe, das hat Ihnen ein besseres Verständnis dafür gegeben, wie die Typen funktionieren und wie die Typen überprüft werden.

Seitennotiz: Dies ist, was harkell tut, wenn Typinferenz durchgeführt wird. 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 überprüft, welcher Typ mit t assoziiert wurde, und dies ist der Typ der Funktion.