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

Ja, herzlich Willkommen.

Ja, heutiges Thema Codaten mit Alternativen soll heißen Codatentypen, in denen sich verschiedene Zustände auch mal grundsätzlich unterschiedlich verhalten können, in dem Sinne, dass verschiedene Beobachtungen auf ihnen möglich sein können.

Also nicht nur verschiedene Beobachtungen, das haben wir immer, sondern dass also verschiedene Beobachtungsoperationen auf ihnen möglich sind.

Hauptunterscheidungsbeispiel wären einerseits unsere bekannten Streams.

In unseren Streams, da verhält sich also praktisch jeder Zustand in so einer Co-Algebra vom Grundsatz her gleich, in dem Sinne, er gibt halt irgendein Datenelement aus und schaltet dann zu einem nächsten Zustand weiter.

Und was wir gleich einführen wollen, ist ein Codatentyp E-List für finite or infinite list.

Das Feinheit kommt irgendwie in der Abkürzung nicht vor. Das sollen also Streams sein, die gewissermaßen auch mal abbrechen können. Das soll ein Codatentyp sein, der aber den bekannten Datentyp der endlichen Listen erweitert um unendliche Listen.

Wir können uns erstmal überlegen, was das für den Datentyp als Co-Algebra bedeutet.

Wir wollen jetzt praktisch hier rechts hinschreiben, irgendeine Mengenkonstruktion, die uns also die möglichen Beobachtungen auf so einem Zustand in einem System beschreibt, wo also ein Zustand entweder schon das Ende der Fahnenstange sein kann oder sich noch weiterentwickelt.

Dieses entweder oder äußert sich in einer disjunkten Vereinigung, sprich in einer Mengensumme, die diesen beiden Fällen entspricht.

Das heißt, entweder es geht normal weiter, wie bei den Streams auch, dann haben wir also hier rechts a Kreuz n, wie bisher auch.

Also es wird ein Datenelement aus a ausgegeben und es wird dann zu einem Nachfolgezustand in n weitergeschaltet. Oder es ist halt Schluss.

In dem Falle wird überhaupt nichts ausgegeben. Also wenn unser Element jetzt das letzte Element oder unser Zustand praktisch für das Ende einer hier endenden endlichen Liste steht, dann gibt es weder ein Datenelement noch gibt es in sinnvoller Weise einen Nachfolgezustand.

Das heißt, hier muss irgendwas hin, was keine Information repräsentiert und keine Information ist einfach eins.

Das ist ein Datentyp, wo alles gleich ist, wo also überhaupt keine Information besteht, wenn ich von dem Typ was ausgebe.

So, die Frage ist jetzt, wie wir das in unsere Syntax rein kriegen und eigentlich nur darum geht es heute, dass wir nochmal unsere Syntax erweitern, um Datentypen dieser Form deklarieren zu können.

Die Beobachtung ist die, wenn ich das Ding jetzt mal alpha nennen, dann induziert die disjunkte Zerlegung, die ich hier habe, eine disjunkte Zerlegung von dem n.

Nämlich, wenn ich mir hier den linken Anteilbild nehme und davon das Urbild nehme, alpha hoch minus eins von, ja ich nenne die Teilmenge jetzt mal auch weiterhin eins.

Und dann außerdem das Urbild der rechten Seite, dann sehen wir, dass das auf jeden Fall, dass die Vereinigung von diesen beiden Urbildern ganz n ist,

denn jedes Element von n muss ja unter alpha in einer dieser beiden Hälften abgebildet werden und es wird auch jedes Element von n nur in genau einer dieser beiden Hälften abgebildet, weil das ja eine disjunkte Vereinigung hier ist.

So, mit anderen Worten, das ist jetzt nur noch bis auf Biektion, ich habe auch eine disjunkte Zerlegung von dem n, einmal in die Zustände, die so enden und die Zustände, die noch weitergehen.

Gut, es ist ja auch nicht weiter überraschend, dass das eine disjunkte Zerlegung ist.

So, und jetzt müssen wir einfach nur sehen, dass wir das jetzt noch in der Syntax einfangen und das tun wir, indem wir diesen beiden Seiten Namen geben.

Diese hier bekommen also sympathische Namen, diese hier heißt dead und diese heißt alive.

So, ja, also dead sind die Zustände, wo nichts mehr kommt und alive sind die, wo es noch weitergeht.

Ja, und dann können wir uns ja natürlich ein bisschen Freestyle jetzt unsere Syntax dafür ausdenken und das, was wir schreiben, ist dieses.

Wir beginnen wieder eine Q-Datentyp-Deklaration, Codata, I-List, A-Ware.

Ja, und jetzt kommen wieder Deklarationen von Beobachtern, nur sind diese Beobachter, also Beobachter gleich Destruktoren,

nun sind diese Destruktoren nicht mehr auf dem gesamten Codatentyp deklariert.

Zum Beispiel hier würde ich wieder sowas wie head and tail haben wollen, aber head and tail sind eben nur dann definiert, wenn ich hier in dieser rechten Hälfte bin.

Deswegen deklariere ich das.

Head geht also im Prinzip von I-List A nach A, aber eben nicht vom ganzen Codatentyp, sondern nur von der rechten Alternative und das drücke ich aus durch so ein Add.

Head geht also von I-List A Add Alive, also von den lebendigen Bewohnern von I-List A nach A, genauso ist also tail auch nur auf I-List A Add Alive definiert und geht nach

I-List A.

Ja, und dann brauchen wir noch einen weiteren Konstruktor, um die andere Alternative zumindest mal erwähnen zu können, um sagen zu können, wie die heißt.

Da soll also was gehen von I-List A Add Dead nach 1.

Das ist als Information natürlich völlig bedeutungslos, es gibt nur genau eine Abbildung, die eben nach 1 reingeht.

Aber wie gesagt, es erlaubt uns eben hier nochmal diesen Namen der zweiten Alternative zu deklarieren und gut, wir nennen das zum Beispiel End, also aufhören.

Also insbesondere können wir das wieder in so Gruppen zusammenfassen, um zu sehen, wie das also hier rechts drin landet.

Wenn ich die Domänen jetzt mal nur auf die Alternative abkürze, geht End von Dead nach 1 und das Par, Head, Tail, das geht von Alive nach

A Kreuz I-List A.

So, wir wollen uns also jetzt unseren Co-Algebra Format oder unseren Format für Mengenoperationen, die uns wiederum Co-Algebra definieren, in voller Allgemeinheit zu Gemüte führen.

Wir haben ja gesagt, so eine Mengenoperation, die darf ich bauen aus konstanten Mengen, der Argumentmenge x, kathesischen Produkt und bis jungen Summen.

So, und das gibt im Prinzip dann beliebig komplizierte Ausdrücke in dieser Syntax.

Nun haben wir schon mal angedeutet, es gilt als allgemeines Rechengesetz für diese Mengenoperationen, das Distributivgesetz.

Und zwar finde ich eine Abbildung von x plus y Kreuz z nach x Kreuz z plus y Kreuz z, nämlich, das muss ich hier machen, hier habe ich so ein W verpaart mit einem z.

Das W stammt entweder aus x oder aus y.

So, und naja, jetzt mache ich das mal als Case-Ausdruck hier, wie man das in Haskell machen würde.

In Haskell würde jetzt also hier gepatternmatched werden auf die Injektionen in diesem Summendatentyp hier, die hießen in left und in right, oder in 1 und in 2.