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

Ja, heute beginnt der spannende Teil des Abschnitts über Induktion und Kohinduktion.

Also jetzt mal so ganz ehrlich, wie aufregend fanden Sie das mit den initialen Algebren?

Ich meine jetzt nicht schwierig, sondern wie anregend fanden Sie das?

Die meisten waren ja nicht... was?

Die meisten waren...

Ja, ja.

Gut, das ist eine ungewohnte Sichtweise gewesen.

Im Prinzip geht es nur um die ganz normalen Datentypen, wie man sie, wenn man sie funktional programmieren kann, kennt.

Wenn nicht, kennt man sie natürlich nicht, dann ist es schwieriger.

Die dann eben zusammenfallen mit einfach den Thermenmengen, wie wir sie aus GLOLOB kennen.

Also Thermen, die man aus den Konstruktoren bilden kann.

Und der abstrakte Teil daran ist dann eben eine Charakterisierung dieses Datentyps,

gleich dieser Thermenmenge, als eine initiale Algebra für eine gegebene Signatur.

Wobei initial heißt, in jede andere Algebra bekomme ich einen Homomorphismus.

Gut, das ist jetzt ein Konzept außer Algebra und da muss man sich reinfuchsen.

Das sind alle anderen so auf ähnlichen Level damit.

Also schwierig, schwer von der Motivation her zu verstehen, aber letztlich verdaut sind dazu noch Rückfragen,

dass einigermaßen drin sein muss für das, was ich heute mache.

Erläuterungsbedarf.

Also ich habe gleich sowieso noch einen kurzen Recap dafür, weil ich dann nämlich anfange, Pfeile umzudrehen.

So, also machen wir einfach mal.

So, ab jetzt geht es also nicht mehr um Datentypen, sondern um Codatentypen.

Und dazu erinnern wir nochmal an die Datentypen.

Was ist das Entscheidende an Daten, was wir kennengelernt haben?

Daten werden konstruiert, deswegen hat ein Datentyp Konstruktoren, zum Beispiel nimmt sich da etwas ein Element x

und eine Liste l und macht daraus konst xl.

Also Daten baue ich auf.

So, dual dazu werden Codaten destruiert, die baue ich ab.

Und das mache ich nicht, weil ich Freude am Kaputtmachen habe, sondern das Ziel dabei ist, die Codaten zu beobachten.

Das ist das Entscheidende an Codaten. Also Daten baue ich auf, Codaten beobachte ich.

Und das Beispiel, das wir jetzt zumindest in dieser Sitzung erstmal als unser wesentlichen einziges Beispiel machen werden, wir sehen dann später noch mehr, sind Streams.

Also Streams ist ein typisches Beispiel für Codaten, so einen Stream, den konstruiere ich nicht im Rechner, sondern so ein Stream, da kommt auf mich zugerollt über eine Internetverbindung oder ein Sensor oder irgendwas.

So, die Menge der Streams bezeichnen wir mit S. Und formal ist die Menge S der Streams gegeben irgendeinem Basisalphabet A, ist das die Menge A hoch Omega.

Ich schreibe noch hin, was das ist, aber wenn jemand sich ein bisschen auskennt mit regulären Sprachen oder sowas, dann weiß er, was das ist. Nämlich das hier.

Das ist die Menge aller Sequenzen A0, A1 und so weiter.

Der Klarheit-Halber schreibe ich noch mal drunter, also es soll sich hier handeln um eine unendliche Sequenz, wobei diese Ai alle aus A stammen.

Für i größer gleich Null.

Ein Stream über A ist eine unendliche Sequenz von Elementen von A. Also genau das, was ich eben angedeutet habe, wenn ich Fernsehe, dann ist der Stream eine unendliche Sequenz von Bildern, die ich verarbeiten muss, wenn ich irgendwo an einem Socket lausche, dann ist so ein Stream eine unendliche Sequenz von Worten oder was auch immer.

Wie gesagt, einen Stream zu konstruieren macht nicht so richtig viel Sinn. Natürlich kann ich mir vorstellen, dass ich einen Stream nehme und noch ein Element vorne dran hänge, aber ich stelle mir nicht vor, dass der Stream auf diese Art konstruiert ist.

Wo sollte ich denn da anfangen? Die Vorstellung ist eher, der Stream ist einfach da und ich nehme ihn auseinander. So, wie mache ich das?

Ich habe eine Kopffunktion, mit der lese ich das aktuelle Element des Streams.

Anständig umbrechen. Das heißt, so eine unendliche Sequenz a0, a1 und so weiter, die bilde ich ab auf das erste Element a0.

Das reicht mir natürlich nicht, denn damit kann ich ja eben nur den Anfang des Streams beobachten. Was ich dann noch brauche, ist eine Funktion, dann einfach den Stream weiter zu schalten.

Ich habe das erste Element jetzt gelesen. Okay, weiter geht's. Das ist diese Funktion tail. Und die bildet einen Stream a0, a1 und so weiter ab auf den Teil des Streams, der hier bei a1 anfängt.

Also schneidet a0 vorne ab und das ist dann also der Stream a1, a2, a3 und so weiter.

Ja, und das ist auch schon alles, was diesen Codatentyp eben ausmacht. Informell, warum macht es den Codatentyp aus?

Nun, weil es mir erlaubt, den Stream vollständig zu beobachten. Wenn ich diese Funktion head und tail anwenden kann, dann kann ich mir den gesamten Stream angucken.

Nacheinander. Ich sehe mir den head an, dann sage ich einmal tail, dann sehe ich mir eins an und so weiter und so weiter.

Das heißt, wir sehen diese beiden Funktionen jetzt als die Deklaration des Codatentyps an und haben dafür auch Notationen, die jetzt so nicht mehr in Haskell zur Verfügung steht.