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

Ja, wir hatten noch aus dem Exkurs zum Thema System F, den Herr Gurin letzte Woche angefangen hatte.

Ah ja, da hätte ich doch noch eine Frage. Sind Sie klargekommen mit Herrn Gurin?

Alles in Ordnung, sind noch Rückfragen?

Herr Gurin hat im Gegensatz zu mir das mit Folien gemacht, die müsste, meine ich, online gestellt haben.

Sind noch Fragen, sind alle geflüchtet?

Ja, also die Typinferenz in System F ist, ja, ja, das ist schon richtig, der Rest kommt jetzt, das ist das, was ich meinte, mit übrig geblieben.

Also wir werden nicht beweisen, dass Typinferenz in System F unentscheidbar ist, wir werden stattdessen jetzt uns von unten her im positiven Sinne ranrobben, dass wir also mal angucken, was denn stattdessen entscheidbar ist.

Gut, und das kommt genau jetzt.

So, also wie gesagt, Typinferenz in vollen System F ist unentscheidbar.

Wir gucken uns jetzt noch zwei Wege an, wie man dem ausweicht.

Das eine ist, man schränkt halt die Sprache ein auf ein Fragment, auf dem wir dann entscheidbare Typinferenz bekommen.

Und die andere Idee ist die, naja, dann ändern wir halt das Problem, nicht unbedingt die Sprache, aber das Problem.

Und verlegen uns von Typinferenz auf Typchecking und ändern dabei auch noch leicht die Sprache.

Das werden wir dann in Detail noch sehen.

Jetzt also zunächst mal der erste Ansatz, wir schränken die Sprache ein auf etwas, das nennt sich ML-Polymorphin.

So, und das nennt sich nicht umsonst ML-Polymorphin, das ist eben tatsächlich eine Form von Polymorphin,

die in vielen funktionalen Programmiersprachen, darunter eben daher der Name ML, aber auch in Haskell ohne Glasgow Extensions zum Beispiel,

die unterliegende Form von Polymorphin ist.

So, da fehlen wir wieder auf keine passende deutsche Entsprechung ein.

Die grundsätzliche Einschränkung ist die, dass der Al-Quantor, also die Quantifizierung von Typen über Typparameter,

dass die nur top level stattfinden darf.

Das schließt also bestimmte Dinge aus.

Also folgender Typ ist also dann damit verboten.

Wir erinnern uns an diesen Typ hier, ne, aber doch richtig.

Mensch, jetzt muss ich mich hier wieder ins Boxhorn jagen.

So, dieser Typ hier, der also Polymorph über eine Variable a, die Funktionen enthält, die eine Endofunktion auf a nehmen

und ein Element von a und dann wieder ein Element von a ausspucken.

Ja, und dafür alle nur top level, da verstehe ich, dass die Al-Quanturen nur ganz oben im Term auftauchen dürfen.

Das Beispiel ist dazu gedacht, das zu illustrieren, also ich wollte es jetzt gleich am Beispiel erklären, was da verboten ist.

Also, ich nehme mir das hier, das sind die natürlichen Zahlen.

Und bilde von da ab wieder in die natürlichen Zahlen.

So, und das da wäre der Typ der Successor-Funktion.

Gut, und der wäre danach verboten. Warum?

Weil, naja gut, weil hier streng genommen zwei Quanturen auftauchen, die nicht top level sind.

Sie sind nicht top level, weil sie unter einen Funktionsraumkonstruktor hier kommen.

Also top level heißt, wenn ich den Syntaxbaum des Typs absteige, ganz oben liegend.

Und das hier ist nicht ganz oben liegend, ganz oben liegt eben hier der Funktionsraumkonstruktor und darunter kommen diese beiden Quanturen hier.

Das wäre also verboten. Das ist bei dem hier im Grunde kein Problem, den könnte ich auch nach vorne ziehen.

Müsste ihn dann natürlich, nö, müsste ich gar nicht.

Also, ich könnte ihn einfach nach vorne ziehen, dann wäre er top level, das wäre dann dasselbe.

Aber dieser hier, der in einer negativen Position sitzt, also links von einem Funktionraumkonstruktor, den kriege ich nicht nach oben geschoben.

Man kann das im Grunde machen wie bei aussagenlogischen Formeln und wer darüber ein bisschen nachdenkt, wird feststellen, wenn ich das Ding hier nach oben schiebe, wird es ein Existenzquantor und den haben wir nicht.

Also, die ernsthafte Einschränkung ist, ich darf links vom Funktionenfall keine Alquanturen verwenden.

Links meinen natürlich also in der topologischen Struktur des Baums, nicht in der tatsächlich lexikalischen Struktur der Formel.

Also, kurz gesagt, das linke Argument des Funktionenfalls, das darf keine Alquanturen enthalten.

Also, schreiben wir mal.

Also, weniger missverständlich vielleicht diese Formulierung.

Also, im linken Argument vom Funktionenfall darf ich keine Alquanturen verwenden.

Ja.