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

Bevor wir in das Video beginnen, möchte ich etwas hinweisen, das ich am Montag nicht fertig sein konnte.

Das könnte euch mit dem Übungsgerät helfen.

Letztes Mal haben wir mit einem Konduktivtyp gespielt, das auf ein dynamisches Terrain gepräsentiert hat.

In dem wir an jedem Ort aufnehmen konnten, wo wir nach rechts oder links und absteigen konnten.

Das ist sehr einfach. Man kann sich ein anderes Terrain vorstellen, in dem man mehr als zwei Optionen hat.

Man hat 72 Optionen an jedem Schritt. Wir wollen nicht 72 verschiedene Observer haben.

Die Richtung 1, die Richtung 2, die Richtung 3, das wäre ein bisschen dumm.

Was man anstattdessen gerne machen möchte, ist, nur einen Observer zu haben, der eine Funktion ist, die,

was wir nehmen wollen, auf der nächsten Schraube führt.

Wir nehmen jetzt die Möglichkeit, absteigen zu bekommen, da das uns nichts mehr bringen kann.

Man könnte einen Typen definieren, den wir InfTerrain nennen, für Infinite Terrain.

Wir können nicht absteigen, so etwas.

Diesmal mache ich es parametrisch, nicht nur die Art von Objekten, die wir an jedem Schraubendruck finden,

sondern auch die Direktionen, die wir nehmen können.

Dies könnte ein Typen sein, das Vor- und Rück- und links- und rechts- und nord-eester- und nordwest-Vorwärts-Vorwärts-Vorwärts-Vorwärts hat.

Und dann würden die Observer, wie letztes Mal, etwas von einem Terrain geben,

das uns eine Liste von Objekten gibt, die wir auf der aktuellen Schraube sehen.

Dann würden wir nur einen Observer nennen, den wir dann,

wenn wir einen Infinite Terrain geben,

eine Funktion geben, die uns, wenn wir eine Direktion nehmen, auf die nächste Schraube sendet.

Die Paranthesis, die wir an der Konvention benutzen, sind nicht nötig, ich nehme sie nur als Einfluss.

Wir können diese Konduktivtype als eine Koalgebra für einen Funktor T, D-Rov, A,

in diesem Fall, in dieser Art, uns in Liste von A plus,

und nun die Notation, die man typisch für eine Funktion benutzt, ist so,

das sollte so gelöst werden wie, ja, ja, klar, wo sind sie?

Hier schon.

So, das ist ein Times und das ist eine Funktion von Direktionen zu x.

Also, letztes Mal, stattdessen, haben wir es so geschrieben,

was als ein Paar von x sein könnte, aber wir können es auch als eine Funktion von einem Set mit nur zwei Elementen zu x sehen,

was ein isomorphisches Objekt ist, das ist eigentlich das gleiche.

Und wenn wir uns die letzte Koalgebra für diese ansehen, dann ist es ein Baum von infiniter Höhe,

und die Bremsung des Baums ist von der Kardinale von dem, was wir hier auspicken.

Also, wenn wir sieben Direktionen haben, dann haben wir Tres mit sieben Abfällen auf jeder Note.

Und jetzt die Frage, was ist das Bissimulation Notion für diese Art von Dingen?

Es sollte nicht schwer sein, zu sehen.

Wir sagen, dass R ein Info-Terrain ist,

durch Bissimulation.

Also, jetzt haben wir zwei Elemente und wollen sehen, ob wir sie ein Teil erzählen können,

oder ob wir sie in irgendeinem Fall bezeichnen können. Also, welche Tests, was sollten wir machen können?

Wir sollten zuerst die Objekte in der aktuellen Position vergleichen.

Das ist wie die letzte Zeit.

Die erste Beziehung, die wir letzte Zeit verwendet haben, war, dass wir die Elemente nicht bezeichnen konnten,

indem wir links und rechts auf beiden Sachen gehen.

Aber jetzt ist die gleiche Beziehung, dass wir die Elemente nicht bezeichnen können,

indem sie in der gleichen Richtung auf beiden Abfällen gehen.

Die zweite Beziehung ist, dass für alle Direktion D,

wenn wir an x auf Direktion D gehen,

wir nicht bezeichnen können, was wir da bekommen, was wir sehen, wenn wir in der gleichen Richtung auf y gehen.

Und wieder zeigt man, dass, wenn zwei Dinge, wenn es eine Bissimulation zwischen zwei

und einem infinite Terrain gibt, dann sind sie die gleichen. Ist das mehr oder weniger klar?

Okay, dann gehen wir zum Thema der heutigen Sitzung.

Ich möchte jetzt die Lichter aufstecken.

Wir werden darüber reden, wie wir Polymorphism verwendet haben.

Wir werden die Zeiten, in denen wir verwendet haben, explizit machen und versuchen, es ein bisschen besser zu verstehen.

Also, zuerst, was ist Polymorphism? Ich dachte, es war ein Kind von Supermöglichkeit, das es nicht ist.

Das Problem mit Polymorphism ist, dass es in der Computer-Scienzen verwendet wird,

mit verschiedenen Bedingungen, was die Parallel-Languagen verwendet haben.

Also, es ist besser, die Terminologie zu beenden.

Wenn wir auf ein Buch, auf ein Textbuch, auf Typesystems schauen,

dann ist die Definition von Polymorphism ein bisschen vig.

Zum Beispiel, ein Polymorphisches System ist ein Typesystem,

in dem ein einziges Stück Kode mit mehreren Typen verwendet werden kann.

Das ist eine vige Definition.

Aber wir können es benutzen.

Also, wir sehen ein paar Beispiele, in denen wir diese Situation sehen.

Wenn Sie nicht mit der Sprache dieser Beispiele aussehen, ist das nicht sehr wichtig.

Ich glaube, dass Sie vielleicht etwas in C++ gesehen haben.

Dort gibt es das, was wir als Operator-Overloading nennen.

Wir können es dort machen, um z.B. zu definieren, was der Operator Plus bedeutet,

wenn Sie zwei Integer zu ihm geben.

Und Sie können definieren, was der Operator Plus bedeutet,

wenn Sie zwei Stränge zu ihm geben oder zwei Referenzen zu konstanten Strängen oder so weiter.

Und dann können Sie Plus in dem gleichen Programmtext benutzen, mit unterschiedlichen Bedingungen.

Das wäre ein Beispiel des Polymorphismus.

Ein ähnliches, wieder in C++, ist, wenn Sie Meteroverwaltung haben.

Wir haben zwei Klassen, C und D.

D ist eine Subklasse von C.

Und wir definieren ein Method, das bereits in C definiert wurde.

Und wenn wir dann ein Stück Text haben, das C bildet und etwas macht,

und ein anderes, das D bildet und etwas nennt,

dann ist das das gleiche Symbol, das mit unterschiedlichen Typen benutzt wird.

Das beinhaltet das eine in C und das andere in D.

Ein anderes, ähnliches, nicht genau das gleiche Beispiel, würde die Dynamik-Dispatch korrespondieren.

Wir könnten das in C++ mit Virtual Methoden machen.

Das ist auch das gleiche mit Java.

Also sagen wir, wir haben eine Interface mit nur einem Method, Draw.

Und wir haben zwei Klassen oder mehr Klassen, die diese Interface implementieren.

Das bedeutet, dass beide Klassen, C und D, diese Methode implementieren müssen.

Und dann haben wir ein Method, das eine Array von Figuren nimmt.

Also jeder Element in dieser Array kann ein C, ein D, ein Square sein oder so.

Und für jede dieser Elemente nennt es das Draw-Method.

Und wiederum benutzen wir dieses Method, Draw.

Wir bezeichnen den Draw eines der Klassen, die diese Interface implementieren, jedes Mal.

Also wiederum haben wir ein Symbol, das mit unterschiedlichen Typen benutzt wird.

Zwei weitere Beispiele und wir sind fertig.

Genetics in Java.

Also an einigen Stellen wurde Java mit Genetics ausgestattet.

Das bedeutet, dass man zum Beispiel eine Klasse Stacks definieren kann und sie parametriert auf dem Stacks Content machen kann.

Also wir können zum Beispiel Stacks von Integern, Stacks von Strängen definieren.

Und hier können wir ein Method push definieren, das einen Element der Parameter-Type nimmt.

Also hier haben wir push-Called mit 42 und push-Called mit Hello.

Es ist das gleiche Symbol, das mit verschiedenen Typen benutzt wird.

Hier mit Integern, hier mit Strängen.

Dies ist ähnlich zu Polymorphischen Datatypen wie in Haskell.

Dies ist ähnlich zu den Noten, die wir in den Übungen benutzen.

Dies kann als Wert von Type List A gesehen werden.

Und dies ist ein Konstruktor, das von List A und von List A aus geht.

Und wiederum können wir eine Funktion append definieren, die zwei Liste von Strängen, Integern und so weiter nimmt und sie konkateniert.

Warum all diese Beispiele?

Es gibt eine sehr alte Klassifikation, die von 1967 kommt.

Sie sagt, dass wir mindestens zwei Formen Polymorphismus bezeichnen können.

Einer ist Parametrie Polymorphismus.

In Parametrie Polymorphismus haben wir, sagen wir mal, eine Klasse von Koden, eine Funktion,

zu der wir einen genetischen Typen geben.

Wir müssen ihn kompilen oder nur einmal verzeihen.

Und er wird in einem unibaren Weg verhandeln.

Ich denke, dies wird klarer sein, wenn wir die vorherigen Beispiele verabschieden.

Und an der anderen Seite, was Ad-hoc-Polymorphismus nennt,

Ad-hoc ist nicht derogativ, sondern schriftlich,

haben wir viele Symbolen, die die gleichen mit unterschiedlichen Behörden definieren.

Also, wir verabschieden die Beispiele.

Hier haben wir zum Beispiel dieses Symbol plus.

Aber wenn es an Koden und Strängen verwendet wird,

wird es vielleicht komplett anders.

Das ist der Fall, wie wir das definieren.

Es kann nichts mit der Zusammensetzung zu tun haben.

Dies ist ein klarsamer Beispiel von Ad-hoc-Polymorphismus.

Hier ist es die gleiche Situation.

Dieses Method Draw wird wieder auf jeder Klasse, die die Interface verwendet,

verabschiedet.

Die Verabschiedung wird vielleicht komplett anders.

Und das ist der Fall.

Das ist der Fall.

Das ist der Fall.

Das ist der Fall.

Das ist der Fall.

Das ist der Fall.

Wenn wir hier eine Definition für Funktion append machen,

wird diese Definition ein genäherter Typ gegeben.

Es nimmt eine Liste von Interfaces,

die sich an eine andere Klasse verwendet.

Das ist der Fall.

Das ist der Fall.

Das ist der Fall.

Diese Definition wird ein genäherter Typ gegeben.

Es nimmt eine Liste von was auch immer und

verwendet eine Liste von dem selben Ding.

Es gibt nur eine Definition.

Es ist egal, was A ist, ob es ein Interfaces, ein String, ein Kreis oder was auch immer ist.

Die Konkatenation wird in der gleichen Weise verhalten.

Das wäre ein Beispiel des parametrischen Polymorphismus.

Nur eine Definition, uniformes Behabe.

Und Generics in Java,

in diesem Beispiel ist einer

versuch, zu sagen, dass es auch ein Instanz des

parametrischen Polymorphismus ist.

Also eine Definition des Behabe für einen Push in nur einem Platz.

Es ist geplant, eine Extension von Java mit parametrischem Polymorphismus zu sein.

Das Ding ist, dass das zu Java als Art Nachdenk wurde.

Es hat nicht wirklich gut mit einigen Features zu tun.

Man könnte z.B. die Methode Push in dieser Weise vornehmen.

Du gibst mir eine E und jetzt mache ich eine Type-Case.

Ich sage, ist das ein String oder ist es etwas anderes?

Wenn es etwas anderes ist, dann mache ich einfach einen normalen Push auf den Stack.

Aber wenn es ein String ist, dann mache ich etwas seltsames.

Ich weiß nicht, ich kann etwas von der Web downloaden oder so.

Was das bedeutet, ist, dass das Behabe von Push,

an dieser Implementation, es ist nicht uniform, auf allen Typen.

Es kann also verschiedene Dinge auf unterschiedliche Typen machen.

Uniformität fehlt, ich weiß nicht, wie man das parametrisches Polymorphismus nennen sollte.

Aber es sollte eine Idee geben, was das umgeht.

Das war's für heute.

Das ist natürlich das Subjekt.

Kann Conta in etwas Ästhetisches machen?

Wie in diesem Beispiel?

Kann Conta die Uniformität in der 2. Jahr?

Es ist etwas, das wir später erwähnen werden.

In diesem Beispiel kann man nichts mit dem Wert A machen.

Man weiß nichts von A.

Es gibt keine Operation, die man mit A machen kann,

als nur diese Werten von hier herzukopieren.

Das ist das Hauptpunkt.

In der Java-Ausgabe, obwohl man nichts von T kennt,

kann man immer noch testen, ob es ein Instanz von einem anderen Typen ist,

und dann ein Casten machen, was hier passiert ist.

Aber ist das nicht so, weil man die Reflektion-Kapazitäten hat?

Es gibt Reflektion-Kapazitäten, aber sie werden auf den Typen der Funktionen impactiert.

Wenn man Reflektion benutzen will, muss man es explizit sagen.

Dann wird es gefiltert.

Reflektion wird durch Typen-Klassen ergeben,

die eine Form von ad-hoc-Polymorphismus sind.

Aber es wird auf den Typen reflektiert.

Was ich versuchen werde, ist, dass

parametrisches Polymorphismus mehr wichtig ist, wenn man will,

als ad-hoc-Polymorphismus.

In vielen Szenen ist ad-hoc-Polymorphismus

nur eine Syntaktik-Sugar-Methode.

Es ist meistens nur ein Mechanismus,

um die Neuheit, einen anderen Namen zu geben,

zu äußern.

Man kann ad-hoc-Polymorphismus simulieren, wenn man ein System mit parametrischem Polymorphismus hat,

das ist expressiv genug.

Parametrisches Polymorphismus, wie wir versuchen werden,

gibt uns Sicherheitsbedingungen,

die wir mit ad-hoc-Polymorphismus nicht haben können.

Mal sehen, ob das funktioniert.

Was wir tun werden, ist, ein System zu schauen,

um in der Lamda-Kalculus Parametrisches Polymorphismus zu haben.

Man könnte fragen, warum wir das definieren,

warum wir nicht einfach die Lamda-Kalculus-Simpli-Type benutzen,

die wir ein paar Monate vorbeikamen.

Wenn man sich das anstellt, sieht man,

dass diese Notion von Prinzipieltypen, also von jedem Lamda-Term,

der generellste Typen der Terme ist,

und dann kann man es mit jedem Typen instanzieren.

Das Problem mit diesem System ist,

dass es für eine Polymorphismus-Type oder für einen Termen-Typen funktioniert,

aber nicht für die Nutzung.

Mal sehen, wie wir das mit einem Beispiel machen.

Wenn Sie sich das anstellen,

waren das drei Typen-Ruhr für die Lamda-Kalculus-Simpli-Type.

Eine Arroh-Introduktion und eine Arroh-Elimination plus die Axiom-Ruhr.

Ich habe dieses Beispiel in Haskell geschrieben.

Hier muss man den Slash hier als Lamda lesen.

Das ist Haskell für Lamda.

Das befindet sich jetzt als Funktion id, als Lamda x, x.

Dann benutzt man das in dieser Funktion,

wenn man Bullen und 42 Typen hat.

Ente, oder so etwas.

Die Frage ist, warum wir das nicht in das Lamda-Kalculus-Simpli-Type typen.

Ich werde es hier auf dem Blackboard schauen.

Wenn wir das Programm einem Kompiler, einem Interpreter oder so geben,

wird es von Definition nach Definition gehen.

Es wird es zuerst typen und dann wird es in der restlichen Definition erhoben.

Ein Kompiler für Haskell würde zuerst Funktion id nehmen und sagen,

was ist der generelle Typ Lamda x, x?

Und wenn man die Variation des Prinzipialtypes-Algorithms kennt,

wird es sagen, dass der Prinzipialtype dieses ist A-A für ein Typ Variable A.

So far so good.

Dann wird es die zweite Definition typen.

Das Wichtigste ist, was die Assumptionen sind,

die der Kompiler in so einem Kontext benutzen wird.

Es wird eine Kontext Gamma mit viel Information haben.

Es wird wissen, dass es eine constant True ist,

dass es von Type Boolean ist und es eine constant False ist,

dass es von Type Boolean ist und es eine constant Zero von Type Int ist

und eine constant One von Type Int ist und eine constant Forty-Zwo von Type Int ist,

und auch wissen, dass es eine Funktion id von Type A-A gibt.

Das ist der Kontext, der benutzt wird.

Der wichtige Punkt hier ist, dass id der Type A-A ist.

Wenn wir dann versuchen, zu sehen, ob wir mit diesem typischen Kontext

zeigen können, dass Lambda x, y, x, id von True, id von False,

hat Type Int, dann sollte es eine Forty-Zwo sein.

Wenn wir versuchen, es zu tun, werde ich es nicht komplett tun,

aber wenn ihr die Übungen gemacht habt, solltet ihr realisieren,

dass ihr an einem Punkt feststellen müsstet, dass Gamma das id von True zeigt,

dass es von Type Boolean ist.

Die Übungen bleiben und hier sollte man prüfen, dass id von Type...

Sorry, das sollte Type Boolean sein.

Id von True sollte Type Boolean sein,

wenn es den polymorphischen Typen der id gibt, aber dafür muss man prüfen,

dass in der Gamma-Kontexte id von Type Boolean ist.

Aber das einzige, was wir dafür nutzen können, ist die Axiom-Ruhe.

Die Axiom-Ruhe braucht, dass wir in der Gamma-Kontexte

id von True, in der Gamma-Kontexte,

in der Gamma-Kontexte id von Type Boolean haben.

Das ist nicht ganz so.

Und wenn wir vorher mal denken könnten, dass Gamma anstatt Type...

Ich denke, dass Gamma anstatt Type id von Boolean sein sollte,

um diese Sache zu funktionieren.

Dann, wenn wir in der anderen Branche zeigen müssen, dass Gamma...

Gamma zeigt, dass id von Type...

Das andere Teil würde fehlen.

Wir können einfach Type-Lemme-Langstuhl nutzen, um generelle Typen zu verhindern,

aber das ist nicht genug, um es zu nutzen.

Wir brauchen ein mehr wunderschönes System.

Und...

Also, was wir hier zeigen werden, ist System F.

Es ist ein anderes Typen-System.

Es ist mit dem einfachen Typen Lambda-Calculus, wie wir sehen,

als interessanter historischer Fakt.

Es wurde mehr oder weniger gleichzeitig entdeckt

von zwei berühmten Jungs, Gérard und Reynolds.

Und sie waren auf komplett andere Dinge gearbeitet.

Gérard war auf Proof-Theorie gearbeitet, war interessiert in Proofs

für intuitionistische Logik mit Quantifizieren.

Und Reynolds war interessiert auf Polymorphismus, parametrisches Polymorphismus.

Und sie haben das selbe entdeckt,

was, naja, es ist nur ein anderer Beispiel des sogenannten Curry-Howard-Isomorphismus.

Proofs und Programme sind zwei berühmte Objekte.

Jetzt gibt es zwei Versionen System F.

Einer ist normalerweise an Alla Curry und der andere an Alla Church.

Wir werden beide sehen.

Ich werde jetzt versuchen, die Unterschiede zu erklären.

Das ist wieder eine kleine Definition des Typen Lambda-Calculus.

Das einzige, was missen ist die bessere Reduktion-Ruhe.

Wie bekommen wir, wie bekommen wir das Polymorphismus-Type-System aus dem System?

Wir müssen ein paar Dinge tun.

Zuerst müssen wir unsere Notion von Typen verändern oder aussteigen.

Nicht nur werden wir Typen, Variablen und Funktionen haben,

sondern auch diese für alle A-Alpha.

Die Intuition für das ist, dass wenn wir eine Typen-Variabel wollen,

die Polymorphik ist, wenn wir sie verändern wollen,

müssen wir sie explizit quantifizieren.

Zum Beispiel, der Typ der Funktion id wie vorher, sollte für alle A, A-A sein.

Das bedeutet, dass id eine polymorphische Funktion sein soll.

Variablen, die nicht von einem Quantifier verbunden sind, sind Typen-Konstanzen.

Wie Bool, Int oder so weiter.

Die nächste Sache, die wir tun müssen, ist, eine Regel zu geben,

die Universal-Quantifikation in Typen vorstellt.

Das ist die Vor-All-Introduktion.

Wenn wir zeigen können, dass S Type Alpha hat,

und A nicht ein Typ in der Kontexte genannt,

also A nicht ein Typ wie Int oder Bool oder so weiter,

dann können wir damit beenden, dass wir Type Alpha für alle A-Variablen geben.

Das ist vielmehr einfach.

Es gibt auch die entsprechende Elimination-Ruhe,

die wieder einmal einfach sein sollte.

Wenn man bereits zeigt, dass die Terme S Type für alle A-Alpha hat,

dann ist es okay, dass S Type Alpha hat,

aber A von jeder Type Beta verwechselt.

Wenn wir zeigen können, dass S Type so ist,

dann können wir damit beenden, dass S Type,

ich weiß nicht, von Int zu Int zu Int zu Int,

nur um ein Beispiel zu geben. Was habe ich getan?

Ich habe A verwechselt von Int zu Int.

Und wir können das für alle Typen tun.

Also, wenn wir das tun, können wir das hier fixieren.

Also, jetzt haben wir die Type, die wir für alle A-Variablen beenden,

das ist das, was wir im Kontext einstellen.

Und dann kann diese Part von der Elimination verwendet werden.

Wir verwechseln A von Bool in diesem Fall und A von Int in diesem Fall.

Also, für alle Elimination, bekommen wir es.

Wir haben gerade eine Type-Konstruktion und zwei Regeln beigetragen.

Es gibt einige schöne Fähigkeiten, die man über System F beweisen kann.

Es gibt viele Fähigkeiten des SimpliType-Landakalkulus.

Zum Beispiel, eine Versorgung.

Das bedeutet, wenn man eine Betareduktion macht,

dann wird der Termin, den man reduziert, das gleiche Type wie vorher,

oder kann die gleiche Type als vorher gegeben werden.

Und mehr interessant ist die Normalisierung.

Was man in System F type, wird in einer normalen Form reduziert.

Das ist, wie es immer ist, wenn wir nur eine Betareduktion haben,

wir haben keine exklusiv beigetragenen,

also magische Fischpunktkombination oder eine Beweglichung in der Sprache.

Das sind Lambda-Termen und Typen.

Und wieder eine Konsequenz dieses Theorien, wenn man will, ist,

dass der Y-Kombinator, der Fischpunktkombinator,

der in der puren Landakalkulus definiert werden kann,

nicht in System F type werden kann,

das würde diese Theorie verbreiten.

Ich will die Beweise geben, das ist eher involviert,

aber es ist auf die gleichen Ideen gebeten,

die hinter der Beweise der Normalisierung der simple Type Lambda-Kalkulus waren,

die Sie in der vorherigen Sitzung gesehen haben.

Das ist ein interessantes Faktor, es ist nicht nur, dass typische Terme enden,

sondern es kann auch gezeigt werden, dass man in diesem System viel machen kann.

Man kann alle primitiven, bewegten Funktionen schreiben.

Ihr habt gesehen, was primitiv-recussion in BFS ist,

aber falls Sie es nicht erinnern, oder das sagt Ihnen nicht sehr viel,

primitiv-recussion sagt, dass wenn es eine Funktion gibt,

die man in Java oder in so etwas schreiben kann,

und man zeigt, dass die Funktion in polynomialer Zeit läuft,

dann ist es auch primitiv-recussion.

Wenn es in exponentialer Zeit läuft,

wenn man die komplexe Analyse macht, und sagt,

in der schlimmsten Falle exponential, ist es auch primitiv-recussion.

Wenn man die Analyse macht und sagt,

dass die runnende Zeit in der schlimmsten Falle 2 zu 2 zu N ist,

dann ist es eine sehr schwierige Funktion,

aber das ist auch primitiv-recussion.

Das hat alle terminierten Funktionen,

die man in der Praxis schreiben will.

Ich wüsste, dass man eine Funktion mit dieser Komplexität

noch nie mehr programmen will.

In der Tat, Sie können sich erinnern,

dass es die bekannte Ackermann Funktion war,

die das erste Beispiel einer komputierten Funktion war,

die total war, aber nicht primitiv-recussion.

Diese kann auch in System F definiert werden.

Eine gute Intuition für die expressive Kraft dieses Systems ist,

dass es so schwierig ist, als ein Kompiler,

wo man alle typischen Funktionen machen muss,

Grafik-Algorithmen,

die als Lambda-Term in System F verwendet werden.

Aber wenn Sie einen Interpreter machen wollen,

was Sie nicht erwarten können,

was die Komplexität sein wird,

was die Programme betrifft,

dann werden Sie die meisten Zeit nicht mehr bezeichnet.

In der Technik kann man alle primitiven-recussionen Funktionen schreiben.

Das ist die Definition von Funktionen,

die von natürlichen Nummern zu natürlichen Nummern ausgehen.

Das ist ohne Verlust der Generalität.

Eine Frage, die sich anbietet, ist, wie man natürliche Nummern

oder mehr komplexe Sachen in System F entdeckt.

Wenn Sie sich erinnern,

dass wir das in der untypen Lambda-Calculus gesehen haben,

aber nicht in der einfachen Lambda-Calculus.

Die Idee ist, dass die Entdeckung von natürlichen Nummern

die gleichen Terme wie in der untypen Lambda-Calculus sind.

Das heißt, dass der Nummer 5

der Terme Lambda f a und dann f f f f f f a,

wo es fünf f's sein sollten.

Das ist die generelle Idee.

Wir können das eigentlich schreiben.

Der Typ, den wir für natürliche Nummern benutzen, ist dieser.

Für alle a, a zu a, a zu a.

Das ist der Typ der Funktion f.

Das ist der Typ der Argument a.

Das ist der Endresult.

Es sollte klar sein, dass 0 als dieser Terme wie vorher werden.

Und man sollte einfach glauben, dass er nicht der Typ ist.

Denn wir haben in der einfachen Lambda-Calculus gezeigt,

dass dieser Terme hier der Typ a zu a, a zu a,

und dann f for all als Vorbild.

Wir sehen ein ganzes Beispiel in einer Minute.

Und dann für Successor können wir zeigen,

dass es die gleiche Definition ist als bei Successor,

die wir vorher gesehen haben.

Da ist wirklich nichts Neues da.

Zu zuschreiben ist ein schönes Beispiel.

Die Idee ist, dass ein natürliches Nummer

eine Endzeit-Applikation der Funktion,

die als erste Argument gegeben wird.

Wenn wir n zu m hinweisen wollen,

können wir einfach die Successor-Funktion

n Mal anzulassen, von m aus.

Das sollte n mal plus 1 anzulassen, ja.

Ich habe mich nur gefragt, warum wir es nur anzulassen müssen.

Warum können wir es einfach alleine lassen und es vorher verbreiten?

Wir hatten das Encoding für natürliche Nummern in der Endzeit-Applikation.

Warum hat das System das verändert?

Wir benutzen die gleiche Encoding.

Okay.

Die Unterschiede... also das ist die gleiche Encoding in diesem Sinne.

Die einzige Unterschiede ist, dass wir definieren,

was der Typ der natürlichen Nummern ist.

Und wir müssen nur verifizieren, dass all diese Terme

in System F nicht der typische Nummer sind.

Dieser Typ sagt, dass wenn man einen nummerlosen,

einen natürlichen Nummer n hat,

kann man ihm eine Funktion von a nach a geben und man wählt, was a ist.

Also zum Beispiel in diesem Fall können wir a nach b wählen,

dann natürliche Nummern wieder, ja, natürliche Nummern wieder.

Das ist der typische Successor.

Und die Multiplikation, wieder, ist n x a nach b.

Es ist die gleiche Encoding wie vorher.

Das einzige, was wir verifizieren, ist, dass wir diese Dinge im System F typisch verifizieren können.

Das wird ein Übungswerk für euch in den Übungsschritten.

Also gehen wir nicht in all diese Beispiele.

Vielleicht machen wir einen.

Also, wir versuchen, dass der Successor diese Type hat, N x N.

Das ist das, was wir zeigen wollen.

Die erste Sache, die wir machen, ist, N x N in den Kontext zu geben,

mit dem Angriff von Arrow.

Und dann, wenn ihr erinnert, ist N hier von Type for all a x a, a x a.

Und was wir tun müssen, oder was wir tun können, ist, das for all zu entfernen,

mit dieser Regel.

Also, wir kopieren die selben Termine von hier her,

nur, dass das for all ausgerichtet wurde.

Jetzt haben wir eine feste a, die natürlich nicht hier passiert ist,

sonst könnten wir die Regel nicht nutzen.

Und von hier her beginnen wir, wie immer, wie ihr schon viele Mal gemacht habt,

wir legen F und x in den Kontext und wir wissen, dass F Type a a und x Type a sein sollte.

Wir bekommen es von diesem.

Und jetzt müssen wir zeigen, dass das gut typisch ist.

Und das case für F, wir wissen, dass es nur Type a to a haben kann.

Und jetzt müssen wir diesen Teil typisch checken.

Und, also, ich kopiere diesen Teil hier.

Und, das ist eine App, also, wir können mehr oder weniger feststellen,

dass dies Type a to a sein sollte und dies Type a, die von dem Kontext folgt.

Und nun wird das wichtige Teil hier sein.

Wir wissen, dass F Type a to a hat.

Was wir zeigen müssen, ist, dass N Type a to a zu a zu a hat.

Und hier a ist fest.

Und in dem Kontext hat N Type diese hier, für alle a a to a a to a.

Aber wir können es für alle Eliminationen nutzen, um diesen Type zu bekommen.

Wie? Wir machen einfach die Variante a zu Variante a.

Das ist perfekt wert.

Und was wir in der Prozess tun, ist, den universalen Quantifier zu erlösen,

der auf dem Typ aufgewachsen ist.

Also, in diesem Beispiel sollte es nicht schwierig sein,

wenn man die Details selbst versuchen möchte,

sollte man nicht so viele Probleme finden.

Aber der wichtige Teil ist, die Vorreiterung zu nutzen,

um ein Vorreiter von deinem Ziel zu erlösen.

Und die Vorreiterung zu nutzen, wenn du das Ziel hast,

und es sonst nicht mehr benutzen kannst.

Was interessant ist, ist, dass wir nicht nur natürliche Nummern und Bulen anbieten können,

sondern auch Systeme F anbieten können.

Alle algebraischen Typen, die wir vorhin in den Fortschritten benutzt haben,

werden in den Fortschritten als organ XV-W Morrison anb

Wenn man einen Paar hat, wie wir so far so genannt haben,

kann man nicht viele Dinge mit dem machen.

Es ist nur eine Operation, die man machen kann, um die Art zu verhandeln.

Lass mich ein Beispiel schreiben.

So far, if you wanted to define pairs of types,

you would do something like this.

You would define, let's say, pair AB as something like this.

Okay, that can be seen as a definition, as algebraic type of a pair.

And if you wanted to use this in your program, what would you do?

If you wanted a function that takes a pair and returns the first element,

what would you do?

Well, you could define first by pattern matching.

So you write first of PAB equals A, whatever.

And you could write another function, a function that takes a pair of integers

and adds them as...

Now, let's look at the right-hand side of these definitions.

This thing can be seen as... this term over here can be seen as a function on X and Y,

that in this case just adds them.

And this thing over here can be seen as a function on A and B.

We are allowed to use A and B here as we want.

In this case we are just returning A and ignoring B.

And every time you write a definition by pattern matching,

the only thing we need to provide is a function that,

given the two arguments of the pair, computes something,

whatever we want to compute.

Well, that idea is precisely what's behind the definition of the type for the encoding of pairs.

So a pair is something that, if you want to compute something of value R,

you give me the right-hand side of your definition by pattern matching

and I compute the value R for you.

That's the intuition of what's behind this.

So can someone think how to define, for instance, the pair function?

Can someone think of a lambda term for it?

Take two minutes, shouldn't be difficult really.

Okay.

Any ideas?

So we want to build the function pair that needs to take an A and a B

and return a pair of As and Bs.

So it needs to return something that, if you give me a function from A to B to R, gives you an R.

So let's try to build this just by looking at the type.

What shall a pair receive?

Well, it needs to receive something of type A, let's call it X,

and it needs to receive something of type Y, let's call it Y.

That's the first two arguments.

And then it needs to return a pair.

But a pair is a function, it's a function that takes a function and returns some value.

So this should also receive a function.

And now, what should it do with that function?

Well, that function says that if you give me A and B, it computes R.

And I need to return an R.

So what should we do?

Well, a good plan is to give an A and a B to the function.

That's a good way to get the R.

Do we have an A and a B?

Well, so again, this is meant to be of type A and this is meant to be of type B.

And this takes an A and a B and returns an R.

And we want to return an R.

So the only sensible thing to do is give an X, give X and give Y to this function.

I've just looked at the type and derived a term from it.

I'm not doing the type derivation, but it will be a relatively simple exercise.

The important thing to remember is this is an A, this is a B, this is an A to B to R.

So this thing here will be an R.

And a good observation is that I built this term in essentially the only possible way it could be defined,

except for some complex detours.

But if we need to return an R and the only way, we know nothing about R,

the only way to obtain it is by using the function f,

but the only way to use it is by passing it the parameters we are given,

because we know nothing about A or B or anything.

And then if we want to define first, well, we defined first before,

it's just a function that takes the first element of the pair.

So this should take first a pair, and now we need to return the first element,

but a pair is something that can receive a function,

that function being the left-hand side of the definition by pattern matching of first.

So first was defined like this in the previous example,

but this is just, if we look at the right-hand side as a function on these two things,

this is essentially, this corresponds to the function x, y, just return x.

So this means you give me a pair, and we apply,

we use this function to return the first component.

So if we apply a function on the two arguments of the pair,

this one will return just the first.

So it's defining the first element of.

And for second, it's just the same, but returning the second element.

And one thing that you should observe is that really in all these cases,

there's really no other way to define these functions.

Since we know nothing about a, b and r,

we are defining them with the only information we have there.

Okay, so another example, how can we define sums?

Okay, plus the case where we had, for instance,

I'm using the notation of the exercises.

So before we could define a type like this one.

This is a data type that corresponds to the sum of a and b.

And we have two constructors, one that says, I give you an a.

So a value of this data type can be either an a or a b.

And we use inject l, well, that's the name I gave to the constructor,

it's not important, to get a value which is an a.

And inject right and b to get a b.

So for instance, before we could define a function that

is a function of a, b, r,

using that data type one can, for instance, define a function like this.

You give me something which is either an integer or a bool.

It's one of the two.

And I want to return an integer.

And I define it by case analysis, by pattern matching.

So if you gave me inject left of n,

I return, I don't know, n.

It's an integer, that's well defined.

And in case you've given me a boolean,

then if it was true, then one else zero.

It's not important.

So this function returns this value if you've given me an integer

or one if you've given me true or zero if you've given me false.

It's defined by case analysis.

And now what's, and we can,

and essentially how we are defining this function.

Well, in order to define this function, you need to give me two things.

This here is a function from int to int.

And this here is a function from bool to int,

whereby this here I mean the right-hand side of the definition.

This is a definition that mentions b.

And b is a bool.

So this is essentially, we can look at it as a function from b to int.

And this can only mention n.

But n is an int.

So this can be seen as a function from int to int.

The only way we can define a function by pattern matching

for something of type a there, a and b,

is by providing a function that computes the value for the case a

and a function that computes the value for the case b.

And that is precisely what the type of the sum says.

A sum is defined as something that,

if you want to compute a function from either a or b to some value r,

tell me how to proceed in the case we have an a.

Tell me how to proceed in the case we have a b.

And I will tell you the right result.

So now we need to define, to see how, given an a,

we can construct a sum and given a b,

how we can construct a sum.

And so looking at the type for inject l.

L needs to be able to receive something which is an a.

Let's call it x.

And needs to return something that takes two functions.

One for the case where we have an a

and one for the case where we have a b.

So let's call the functions f and g.

And it needs to return an r.

And the only way we can get an r is either using f or either using g.

f takes an a.

And we have an a.

And g takes a b and we have no b.

So the only possible way is to apply x to f.

The only possible way to get the r.

And similarly for the other case,

we receive let's say a y, which is meant to be a b,

an f and g, and we need to return an r.

This can give us an r if we have an a, but we have no a.

This one can give us an r if we have a b, but we have a b.

So the only way in which we can define such a thing is by applying y to j.

And then we can just define a function in order to do the case analysis,

the definition by pattern matching.

We only need to provide the function for the two cases, f and g,

and provide a sum.

And we want to return an s.

So we just apply f and g to s.

I'm just following the types and building the terms

as if they were a puzzle, trying to assemble these things in the only possible way in this case.

And again, I repeat the observation, in this particular case,

there was only one way in which these terms can be written,

therefore adding superfluous things like applying the identity or things that compute the same function.

A more interesting case, perhaps, is the list.

It can be seen as a sum, but one of the cases is recursive.

So before we would have defined this as nil is a list of a's,

and cons takes an a and a list of a's, and returns a list of a's.

So in a sense, a list is a sum, just like before.

And a definition by case analysis is similar, has two cases,

one for the empty list, one for the non-empty list.

But it's essentially a definition with two cases, and we need to provide a right-hand side for each.

So if we want to define a length function that takes a list of a's and gives us a natural number,

we would have defined it like this, we would have said length of nil is 0,

length of cons x of xs is 1 plus length of xs.

So again, it's a definition by pattern matching with two cases,

and the important thing is that here we have nothing here, this is a constructor with zero arguments.

So in this first case we can only put a constant of the type we want to return.

And in the second case we need to produce something of the type we need to return,

but we can use both xs and x.

Actually we can use x, which I'm ignoring here, and we can use also the result of applying the function recursively on the type we are defining.

So list is a recursive type, we can assume that this function, if it's meant to be defined recursively,

then once we apply the recursion to the recursive argument, we get something of the type we want to return,

and we can just use it here together with the x.

And that's the idea behind the encoding of lists.

The encoding of lists says if you want to compute an R from a list,

you need to give me an R for the base case, and you need to give me a function from the current element,

which takes also the result of computing the function recursively on the tail of the list,

and returns the result you want, and I give you such a result.

It's not hard to see how to define such a thing.

If you want to build an empty list, every time you want to compute something from such a list,

you need to return the argument for the base case.

And if you are given the head of the new list and a list, and you want to compute a function from it,

this is the element, this is the tail, this is the value for the base case,

and the combining function for the result of computing the function you are trying to compute

on the smaller part plus the current element.

And length is defined just like there as base case, I return zero,

and for the... well, this is not okay, this should have been...

So there is a typo there, so length should be defined as...

You give me a list, and I compute the function using zero as the base case,

and now this needs to take an element and the value of the recursive thing,

and return the value, add one to the value of the recursive step.

Yes?

Yes, but the argument it's taking is the argument... so this should return a list.

So if you have arguments, nil should return a list, okay? And a list is a function of two arguments.

What to return when defining something by pattern matching on the empty case and how to compute the recursive case?

Nil is an empty list, so if you want to compute a function and you are defining it by pattern matching,

and you have the value for the empty case, which is U, which is just the first value of the definition of list,

you need to return that case.

So if you want to define a function by pattern matching on a list, you need to provide the value for the base case,

and you need to indicate how to compute the value given the result of the recursion and the head of the list.

So nil, given those two things, returns the value that's expected on the empty list.

So the case for sums was okay. It's essentially the same thing.

For a sum you had to provide a function for the case left and a function for the case right.

And in the case of injection left, you use the first function to compute the result.

My problem is I don't get where f and g are defined, so where do I see what f and g do?

They are not defined. So the thing is, every time, look at this, perhaps this example helps,

while maybe looking at the definition of length.

You see how to define length here by case analysis.

So this is defining the same function in the same way.

And how it does it? Well, here we had a value.