Ja, herzlich willkommen an die Leute, die trotz Berg heute noch aufgetraut sind.

Ich wiederhole vorab nochmal mein Appell vom letzten Mal, wer sich irgendwie berufen fühlt,

hinsichtlich Leuntutorium nächstes Semester möge, sich bitte bei uns melden. Wir haben schon eine

Zusage bekommen, freuen wir uns sehr drüber. Weitere sind jederzeit gerne gesehen.

Ich erinnere daran, wir haben zurzeit am Wickel den einfach getypten Lambda-Kalkül,

kurz denotiert in dieser sehr abgekürzten Form Lambda-Pfeil. Sein entscheidendes Feature

sind eben diese Funktionstypen, das heißt wir haben ein Typ-Universum und einen, im Wesentlichen

nur einen Typ-Konstruktor, denjenigen Konstruktor, der uns halt den Typ der Funktionen von einem Typ

Alpha in einen anderen Typ Beta angibt. Und wir haben einen Haufen Typ-Regeln gesehen, zum Beispiel

diese hier. Zum Beispiel diese hier, alle Typ-Regeln betreffen sogenannte Typisierungsurteile,

Typing-Judgments, die immer anfangen mit einem Kontext bestehend aus getypten Variablen,

also dieses Gamma, das ist sowas wie eine Liste von getypten Variablen, gut, streng genommen nicht

eine Liste, sondern eine Menge, in der jede Variable nur einmal vorkommen darf. Dieser Gamma

ist also praktisch eine Liste von Typisierungsannahmen. Wir nehmen an x1 hätte Typ Alpha 1 und so weiter,

xn hätte Typ Alpha n. So und in so einem Typisierungskontext weisen wir Termen Typen zu

und jetzt in meiner Beispieltyp-Regel ist der Term, der hier jetzt kommt, eine Lambda-Abstraktion,

Lambda x Punkt t und gut, der weise ich natürlich einen Funktionstyp zu und um das tun zu können,

muss ich in einem erweiterten Typ-Kontext, wo ich also schon annehme, dass diese Parameter-Variable

x hier den Typ hat, der hier als Eingabetyp rauskommen soll, also Alpha, jetzt den Typ

t typisiere und dann natürlich mit Typ Beta. So wenn ich schon mal dabei bin, schreibe ich die

anderen Regeln auch noch mal an, weil ich ohnehin gleich zeigen will, dass wir die Regeln auch umdrehen

können. Die zwei weiteren Regeln war diese hier, einmal eine Axiomenregel, die hat keine Prämissen,

nimmt an, wir hätten für Variable x einen Typ in unserem Typisierungskontext und die Regel erlaubt

uns dann dem Term x, also x ist ja nicht nur eine Variable, sondern als solche auch ein Term, dem Term

x Typ Alpha zuzuweisen und die letzte, die Eliminationsregel für den Funktionstyp,

die sagt uns, um eine Applikation t angewendet auf s, ts, einen Typ Beta zuzuweisen, muss ich

einmal t typen als eine Funktion von irgendeinem Eingabetyp Alpha in das

gegebene Beta und ich muss s typen dann mit diesem Typ Alpha.

So wir wollen heute los auf einen Algorithmus,

der uns gestattet Typ-Inferenz zu betreiben, das heißt gegeben irgendein Term soll uns dieser

Algorithmus ausrechnen, ob erstens ob der Term typisierbar ist und zweitens was sein Typ ist,

was die genaue Formulierung dieses Problems ist, das gucken wir uns gleich noch an. Nur mal vorweg,

also dieses Problem ist eben ein Problem, das in funktionalen Compilern tatsächlich zu lösen ist,

die machen das tatsächlich, der Haskell Compiler, der kann das ja auch, im Haskell Compiler schreibe

ich eben nicht typischerweise ausdrückliche Typen an meine Funktionen ran, sondern ich schreibe sie

schlicht und einfach hin und der Compiler inferiert dann den Typ und ist mir auf Nachfrage auch bereit,

ihn gegebenenfalls auszugeben und er verwendet auch tatsächlich bis auf Ausdrucksstärke des

Typsystems im Wesentlichen den Algorithmus, den wir nachher kennenlernen, den sogenannten

Hindley-Millner-Algorithmus. Auf dem Weg dahin kommt jetzt eben als erstes hier dieses sogenannte

Invertierbarkeitslämmer. Also die Frage ist ja, gut, wie sehe ich jetzt, ob überhaupt einem

Term mit Hilfe dieser Regeln ein Typ zugewiesen werden kann und ich hatte eingangs schon gesagt,

gut die Regeln sind syntaxgerichtet, deswegen ist irgendwie bei jedem Term, den ich vor mir habe,

klar, wie ich da vorgehen muss und das fangen wir jetzt noch mal ausdrücklich ein.

Und zwar zeigen wir eben praktisch für jede dieser drei Regeln, dass wir sie tatsächlich umdrehen

können. Das heißt also, dass jeweils ein Term der gegebenen Form nur mittels der passenden

Regel typisierbar ist. Also erstens stellen wir uns vor, wir könnten auf welchem Wege auch immer

einer Variable x ein Typ alpha zuweisen in Kontext gamma. Unser Invertierbarkeitslämmer sagt,

das geht nur, wenn tatsächlich ausdrücklich in gamma steht, das x Typ alpha hat. Es geht nicht

auf irgendwelchen merkwürdigen krummen Umwegen. Zweitens, zweitens, nehmen wir mal an, wir könnten

einer Applikation ts einen Typ beta zuweisen. Dann ist tatsächlich die einzige Möglichkeit,