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

So, wir haben letztes Mal nicht mehr geschafft. Eine Sache, die wollte ich jetzt noch ganz kurz

nachtragen und zwar haben wir den vollen Hindley-Mellner Typinferenz-Algorithmus angeschrieben,

aber kein Beispiel gerechnet und da das auch in den Übungen so direkt nicht vorkommt, sollten wir

vielleicht mal aufnehmen in Zukunft. Wollte ich jetzt gerne hier ein Beispiel

noch mal vorgerechnet haben. Das ist dieses hier.

Jawoll.

Also der Hindley-Müllner-Algorithmus oder eben Algorithmus W.

Ach ja, eine konkrete Sache die da stand war, dass ich zu viele Abkürzungen von

Wörtern verwende, wie zum Beispiel hier ALG für Algorithmus, das natürlich

dieselbe Abkürzung ist wie die, die ich gelegentlich für Algebra verwende. Wenn

Sie eine Abkürzung nicht verstehen, fragen Sie ruhig. So, algorithmus W.

Ich erinnere noch mal an diese beiden neuen Klauseln in der rekursiven

Definition dieser Constraintmenge, die wir ausrechnen im Laufe des Algorithmus.

Das war einmal dieses hier.

So, das ist also einmal der Fall für eine Variable. Also wir versuchen zu typisieren

eine Variable x im Kontext Gamma mit einem Typ, der auf einen Typ Kleingamma

matcht. Und x hat im Kontext, also in Gamma,

einen Typ Schema, all quantifiziert über Variablen a1 bis ak und mit Typ

drunter alpha. So, und das war so.

So, da kommt raus eine Gleichung und zwar nur eine, weil wir jetzt hier

praktisch am Ende der Herleitung angekommen sind. Und diese Gleichung sagt,

gut, wir müssen halt so substituieren, dass dieser Typ alpha den x hat,

all quantifiziert über a1 bis ak, dass der gleich Gamma wird. Und wir substituieren

jetzt aber für diese a1 bis ak, die da vorkommen, frische Variablen. Das ist

das eine, das habe ich noch nicht angeschrieben. Also, das stimmt nicht mit

deinen Notizen überein, weil hier vermutlich ein Tippfehler ist. Habe ich das

letztes Mal korrekt so angeschrieben? Oder habe ich den Tippfehler angeschrieben?

Also es fehlte konkret hier, also in meinen Notizen fehlt das gleiche Gamma.

Also ich meine, es ist unsinn, weil es dann keine Gleichung ist. Steht da? Okay, ja.

Ja, umso besser, wenn man nicht in seine Notizen guckt. So, das ist also das

eine, was wir machen müssen. Wir müssen also sehen, dass wir bei Variablen jetzt

den Typ hier noch, ja, hier praktisch die Polymorphie des Typschemas, den das x

im Kontext hat, ausnutzen. Und die Umbenennung in frische Variablen dient

eben dazu, uns alle Freiheit zu belassen bei weiteren Instanzierungen dieser

Polymorphenvariable x, wo wir dann also andere Dinge einsetzen können für die

a1 bis ak, weil wir eben nicht gezwungen sind, hier nachher diese a1 Strich alle

gleich zu belegen, weil die eben jedes Mal frisch belegt werden, also

jedes Mal frisch gewählt werden. So, und das andere war

in der Fall dieses neuen Let-Konstrukts, das ein Typ alpha bekommen soll in

Kontext Gamma nach geeigneter Substitution für die Typvariablen. So, und

dazu müssen wir erst mal rekursiv diese Constraintmenge für dieses Teilproblem

hier, also für das S ausrechnen und dann aber tatsächlich lösen, weil wir an die

Substitution ran müssen. Das heißt, wir rechnen wirklich jetzt mal aus, den MGU

von der Constraintmenge für Gamma S und B, jetzt für ein frisches B und unter

Zuhilfenahme dieses ausgerechneten MGU definieren wir das als die

Constraintmenge jetzt für diesen rechten Teil T, aber unter dieser schon

ausgerechneten Substitution Sigma.

Das braucht noch mehr Platz. So, und hier diesen Kontext, den müssen wir

selbstverständlich vergrößern, weil der Typ von dem T ja hier von dem X wiederum