dieser audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert

Un reflecting the void

OK. Ich erinnere noch mal

an das Ende vom letzten Mal

an das Ende vom letzten Mal unser Typ-Inferenz-Algorithmus.

Algorithmus W heißt er. Okay, nochmal Disclaimer, ja ich weiß, dass der eigentliche

Algorithmus W eine stärkere Sprache kann als dieser hier.

Also, der Algorithmus kriegt...

Also, der Algorithmus kriegt als Input im allgemeinen Fall ein Trippel, einen Kontext,

einen Term und einen Typ.

So, und der Witz an dem Algorithmus ist, dass er als Output eine allgemeinste Lösung dieses

Problems hier liefert, das heißt eine allgemeinste Typ-Substitution, sodass wenn ich die hier

auf Gamma und Alpha anwende, auf T kann ich sie nicht anwenden, da da keine Typen vorkommen,

ein herleitbares Typ-Urteil rauskommt.

Etwas genauer...

So, dazu berechnet der Algorithmus zunächst mal was völlig anderes.

Der Algorithmus berechnet eine Menge von Gleichungen zwischen Typen.

Die schreiben wir so, PT wie Principle Type und die drei Argumente schreiben wir durch

Semikola getrennt dazwischen, deswegen Semikola, weil die Variablen im Kontext ja schon durch

Kommata getrennt sind.

So, und diese Gleichungsmängel berechnen wir rekursiv.

So, rekursiv heißt durch primitive Rekursion über das mittlere Argument, den Term.

Es gibt also drei Fälle, weil es für Terme nur eine Grammatik mit eben drei Alternativen

gibt.

So, wir fangen an, wir wollen eine Gleichung zwischen Typen hinschreiben, die eben möglichst

allgemein ist und garantiert, dass x in diesem Kontext Gamma Typ Alpha hat.

Nun, das geht sicher nur dann, wenn x überhaupt in diesem Kontext erwähnt wird, dann kriegt

es ein Typ Beta und da man x nur mit diesem im Kontext angegebenen Typ Beta typisieren

kann, muss man eben dafür sorgen, dass dieser Typ Beta gleich Alpha wird.

Also nimmt man diese Gleichung dazu, Beta gleich Alpha.

Dann, der nächste Fall in der Grammatik ist also eine Applikation, t angewendet auf s.

Gut, dann müssen wir wohl herleiten, dass das t irgendeinen Funktionstyp hat und wir

wissen aber noch nicht, was der Definitionsbereich dieser Funktion ist.

Das muss ja nachher matchen, also hier der Definitionsbereich von dem t muss der Typ

von dem s sein, aber wir kennen den noch nicht, wir suchen ihn noch.

Also nehmen wir irgendeine Typvariable a und zwar natürlich eine frische, das heißt eine,

die nicht bisher schon verwendet worden ist, damit wir da eben für dieses a substituieren

können, ohne irgendwas anderes kaputt zu machen.

So, natürlich nicht a, sondern a nach Alpha und dann muss das s eben passend typisierbar

sein.

Das heißt s wollen wir gerade mit diesem neuen Typ a typisieren.

Und letzter Fall, der letzte Fall in der Grammatik ist, dass wir eine Abstraktion vor uns haben.

Gut, und dazu müssen wir eben das, was unter dem Lambda steht, in einem größeren Kontext

typisieren.

Nämlich der, wo x jetzt einen Typ kriegt, der wohl dann in einem Funktionstyp, der

alpha gleich sein muss, die linke Seite darstellt.

Das heißt, wir vergrößern den Kontext um eine Typisierungsannahme für x, mit welchem

Typ wissen wir noch nicht.

Das heißt, wir nehmen uns wieder eine frische Typvariable a her.

In diesem Kontext typisieren wir jetzt t und der Typ, den kriegen muss, der t kriegen