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

Gut, wir schreiten fort beim Thema Lambda-Kalkül. Nachdem wir uns die letzten

Versitzungen angesehen hatten, den ungetübten Lambda-Kalkül, kehren wir zurück heute vorläufig

in die Welt der Zivilisation und reden über den einfach getübten Lambda-Kalkül.

Falls wir später nochmal kurz darauf zurückkommen wollen, ist das der Kalkül

Lambda-Pfeil benannt zu Ehren des einen Typkonstruktors, den er halt mitbringt.

Ja, Typen im einfach getübten Lambda-Kalkül sind also typischerweise von dieser Form hier,

Alpha-Pfeil Beta. Das bezeichnet also, jetzt intuitiv gesprochen, den Typ der Funktionen

von Alpha nach Beta, sprich Funktionen, die Argumente des Typs Alpha erwarten und

Werte vom Typ Beta wieder ausspucken. Nehmen wir uns mal eine ganz einfache Funktion vor,

Lambda x Punkt x, das ist also eine Funktion, die einfach den Wert, den sie eingegeben kriegt,

wieder ausspuckt. Für die würden wir hier herleiten, den Typ A nach A, wobei dieses

Typ A eine Typvariable ist. Das heißt, wir haben hier bis zum gewissen Grad so eine ganz

einfache Form von Polymorphie mit drin. Im Wesentlichen, wenn irgendwo ein Typ vorkommt,

dessen Natur uns nicht genauer interessiert, dann bezeichnen wir diesen Typ mit einer Typvariable.

Bei dieser Funktion ist das so, ob ich hier eine Liste auf sich selbst abbilde oder eine

Funktion auf sich selbst abbilde oder eine ganze Zahl auf sich selbst abbilde, ist völlig egal.

Ich kann die Funktion sogar meinetwegen in Haskell so uniform implementieren. Also in Haskell kann

ich das machen. Andere typische Beispiele, nicht die Funktion, wie was weiß ich, zwei Komponenten

eines Paares vertauscht oder sowas. Ist mir völlig egal, was in diesem Paar für Dinge drinstehen. Ich

muss nur zwei Zeiger umwiegen. Und in Haskell kann ich sowas tatsächlich auch alles genau so

implementieren. In Haskell bringt es sogar noch viel schlimmerhaftigere Formen von Polymorphie mit.

Das heißt, wenn wir die Syntax für die Typen bauen wollen, dann brauchen wir wohl wieder eine

Menge von Variablen. Das sollten der Sauberkeit halber nicht dieselben sein wie die, die wir für

unsere Ausdrücke verwenden. Das heißt, ich nenne das zwar auch v, aber ich mache da mal so ein

Unterstrich drunter, um anzudeuten, dass das also eine andere Menge von Variablen ist als die,

die in den Lambda-Termen vorkommen.

Und gegeben diese Menge von Typvariablen bauen wir jetzt eine neue syntaktische Kategorie. Die eine

syntaktische Kategorie kennen wir schon, das sind die Terme. Und jetzt definieren wir als nächstes

die Typen. Ja, wieder durch eine Grammatik. Allgemeine Meta-Variablen für Typen sind,

wie wir hier schon verwendet haben, alpha und beta und so weiter. So, ein Typ kann sein eine

Typvariable. Also a aus v. Aus technischen Gründen ist es manchmal hilfreich, Basistypen zu

unterstellen, um die von den Typvariablen zu unterscheiden, drücke ich sie mal dick.

Dickdrucken kann ich an der Tafel nicht, deswegen unterstreich ich sie. Also wenn Sie das bei Herrn

Gurin in den Übungen sehen, dann ist das dick gedruckt. Zum Beispiel, der Typ der Bullions oder

sowas. Den würde ich hier also mit einem Unterstrich schreiben und in den Übungen finden Sie es

dick gedruckt. Ja, oder ein Typ kann eben ein Funktionentyp sein. So, nicht? Dieser Unterstrich b

ist die Stamme aus einer Menge, Groß b von Basistypen und wie gesagt, die a stammen aus dem v. Ja,

das ist schon die ganze Grammatik.

Ja, dann entsteht wieder die Frage, danach wie man eben hier Funktionen mit mehreren Argumenten

hinkriegt. Die meisten Funktionen, für die man sich interessiert haben, ja nun mal mehrere

Argumente, was weiß ich, Addition oder sowas. Wie schonmal angedeutet, funktioniert das im

Allgemeinen über Currying, das heißt dadurch, dass ich eine Funktion mit zum Beispiel zwei

Argumenten ansehen als eine Funktion, die wenn ich sie einmal anwende, noch nicht einen Wert

zurückliefert, sondern eine weitere Funktion, die immer noch ein Argument erwartet, nämlich das

Fehlende. Also, im Allgemeinen schreibe ich das also so, nicht? Wir haben einfach so eine Sequenz von

Pfeilen. Das hier repräsentiert mir letztlich eine Funktion, die N Argumente von Typen alpha 1 bis

alpha n erwartet und einen Wert vom Typ Better ausspuckt. Und das ist einfach nur hier ein in

dieser Grammatik gebildeter Typ, in dem ich Klammern weglasse. Und zwar wird per Default

rechtsrum geklammert. Sodass also in der Tat das hier hinhaut, nicht? Also das ist nicht etwa eine