Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Der Saal ist noch nicht besonders voll, da beginne ich mal mit ein bisschen Wiederholung.

Wir hatten zuletzt gesehen in der letzten Sitzung den Algorithmus zur Berechnung von Prinzipaltypen,

der rekursiv ausrechnet eine Menge von Gleichungen auf Typen,

deren allgemeinster Unifikator uns dann den Prinzipaltyp liefert.

Ich schreibe den Algorithmus nochmal an.

Der Algorithmus nimmt drei Argumente und läuft per primitiver Rekursion über das Mittlere.

Die drei Argumente sind ein Kontext von individuen Variablen mit gegebenen Typen,

den wir gegebenenfalls noch weiter instanzieren,

ein Term, von dem wir den allgemeinsten Typ ermitteln wollen

und ein Typ-Ausdruck, den wir diesem Term geben wollen, gegebenenfalls unter weiterer Spezialisierung.

Der einfachste und erste Fall ist der, dass wir eine Variable typisieren wollen.

Wir erinnern uns daran, dass per allgemeiner Konvention diese Variable bereits in dem Gamma vorkommt.

Sie hat also einen Typ in dem Gamma und wir wollen ihnen hier einen anderen Typ alpha verpassen.

Das heißt, was da rauskommt, ist eine einzige Gleichung, Beta gleich Alpha,

sodass x gerade Typ Beta in Gamma hat.

Wir müssen also so substituieren, dass Beta und Alpha gleich werden.

Dann nächster Fall der Grammatik.

Wir haben einen Lambda-Term vor uns, alles noch Wiederholung, kein Stress.

Da rechnen wir jetzt rekursiv die entsprechende Lösung für T aus.

Jetzt in einem erweiterten Kontext, wo wir der Variable x mal einen zunächst mal unspezifizierten Typ geben.

Das heißt, wir führen hier eine frische Typvariable A ein

und T bekommt einen zunächst ebenso unspezifizierten Typ B.

Aber das Alpha, was dann hier für Lambda x Punkt T rauskommt,

das muss dann natürlich gerade der Funktion Typ A nach B sein.

Also A und B sind noch mal ausdrücklich frische Typvariable.

Der letzte Fall ist der, dass wir eine Applikation vor uns haben.

Da haben wir eben dann das Problem, dass wir jetzt keine Vorstellung haben, was hier in der Mitte für ein Typ sitzt,

also welchen Typ S hat und welchen Typ dann gleichzeitig T als Argument erwartet.

Weil wir es nicht wissen, lassen wir es eben offen.

Das heißt, da kommt raus

diese Menge von Gleichungen, wo wir T versuchen zu typisieren als Funktion von,

also natürlich nach Alpha, denn Alpha soll nachher rauskommen,

und eben von diesem noch unbekannten Zwischentyp, für den wir deswegen eine Variable einführen.

Eine frische natürlich.

Dann muss natürlich das Argument S vom Typ Alpha sein.

Dann bekommen wir eben so eine Menge von Constraints, rechnen den MGU aus.

Wir fragen uns dann nach dem...

Was ist denn da mit dem Typ Alpha und dem Typ Alpha?

Gamma ist ja so ein Kontext bestehend aus Typzuweisungen zu Variablen.

Und zwar zu jeder Variable, in die vorkommt höchstens eine.

Per Konvention kommt X hier vor, weil nur solche erwähnt werden dürfen, die im Kontext vorkommen.

Und damit wissen wir, dass wir genau eine solche Typzuweisung X''n Gamma haben, und die nehmen wir uns.

Wenn wir jetzt spezieller den Prinzipaltyp von T und Gamma, weil im allgemeinen erst mal, oder typischerweise eher unspezifizierten Zieltyp ausrechnen wollen,

dann nehmen wir uns ein frisches A, nehmen das hier als den Zieltyp, rechnen diese Constraints aus, Pt von Gamma T und A,

bilden den MGU davon, das ist eine Substitution, und gucken danach, was die uns eben für dieses frische A ausrechnet für ein Typ.

Das ist der Prinzipaltyp.

Das Ganze, das ist also der sogenannte Hindley-Mirna-Algorithmus.

Wie gesagt, hatte ich letztes Mal schon gesagt, und den Herren Hindley und Milner, und eigentlich Curry muss man dazu sagen,

nicht unrecht zu tun, der Hindley-Mirna-Algorithmus ist komplizierter, weil er für eine ausdrucksstärkere Sprache und ein reicheres Typsystem funktioniert.