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

Ja, herzlich willkommen.

Wie letztes Mal angekündigt,

fangen wir jetzt an, die Theorie der Datentypen zu dualisieren und stattdessen eine Theorie der Codatentypen uns anzusehen.

Ja, und dazu erinnern wir uns nochmal kurz an das Grundprinzip der Datentypen, wie wir sie eingeführt haben.

Das Grundprinzip an Daten ist, wir können sie konstruieren.

Das heißt, wir haben sowas wie einen Konstruktor nil, der uns also aus dem Nichts eine Liste konstruiert, oder einen Konstruktor cons,

der ein Element nimmt und eine vorher konstruierte Liste und uns eine neue Liste konstruiert.

Ja, wenn wir uns jetzt mal so ein bisschen von diesem wohlfundierten Bereich wegbewegen, und ja, wohlfundiert heißt, wir können also so ein Datenelement aus gewissermaßen ersten Prinzipien,

also entweder nichts oder irgendwelchen vorhandenen Datenelementen in endlicher Form aufbauen.

Es gibt ja durchaus Objekte von Interesse, die nicht so entstehen.

Das sind nun nicht Dinge, die wir im Computer selber aufbauen, das sind eher Dinge, die wir im Betrieb eines Programms, oder denen wir im Betrieb eines Programms begegnen.

Typisches Beispiel Streams. Ja, also so ein Stream, den ich konstruiere natürlich nicht im Computer, einen Stream. Wie soll ich das machen?

Ja, so ein Stream ist eine unendliche Abfolge von Datenelementen, die ich also in meinen Speicher nie rein bekomme.

Trotzdem wird man nicht leuchten können, dass es Streams wohl gibt.

Wenn ich irgendwo meinen Rechner nehme und ihn an den nächsten Wettersensor anschließe, dann habe ich einen Stream, der da reinkommt.

Gut, dass er tatsächlich unendlich ist, dann das werde ich irgendwie auf Dauer nicht nachprüfen können, und irgendwann wird das Wetter aufhören und der Wettersensor wird aufhören zu senden.

Aber die sinnvolle Annahme zur Behandlung dieses Stückes Daten ist eben, dass das ein nicht abbrechender Strom von Daten ist.

Ja, gut, gehen wir also hin und sagen, okay, das mit dem CONS, das funktioniert ja ganz wunderbar auch mit den Strömen.

Also, ich nehme mir ein Datenelement und ich nehme mir einen Strom und baue mir daraus einen Strom.

Das, was ich mir da vorne ranhänge, also dieses Datenelement, das A, das wird dann irgendwann das erste Element meines Stroms.

Und hier habe ich halt den Rest meines Stroms, also die Operation, die macht durchaus auch auf Datenströmen Sinn.

Nur findet man keinen vernünftigen Sinn, indem Datenströme durch dieses CONS konstruiert sind.

Woraus denn? Abgesehen davon, dass ich also nicht einen unendlichen Strom konstruieren kann, indem ich also einen leeren Strom nehme und dann immer weiter Datenelemente vorne ranhänge, das wird natürlich nichts.

Ganz abgesehen davon gibt es ja idealerweise auch gar keinen leeren Strom, denn ein Strom ist nun mal was mit unendlich vielen Daten, insbesondere nicht keinen Daten.

Das heißt also, diese ganze Idee des Konstruierens, die fällt schlicht für solche unendlichen Datentypen typischerweise fehl.

Sehen wir uns mal was anderes an, was so analog zu Listen ist. Und zwar kann ich ja nicht nur konstruieren, ich kann auch destruieren.

Naja, ich habe zum Beispiel eine Head-Operation, ich habe jetzt, ich schreibe das, ich tue mal so, als wäre das eine Operation von List A nach A.

Gut, ich muss mir überlegen, was ich mache, wenn die Liste leer ist und deswegen keinen Kopf hat, dann muss ich irgendwie einen Fehlwert zurückheben oder irgend sowas.

Und ich habe eine Tail-Operation von List A nach List A, wiederum muss ich mir überlegen, was der Tail der leeren Liste ist, zum Beispiel die leere Liste.

So, das sind die bekannten Destruktoren für Listen. Gut, und die habe ich natürlich genauso, genauso auch für Streams.

Wenn mir jemand einen Stream gibt, dann kann ich sagen, gut, nehme ich mal den Head, das liefert mir eben ein Datenelement, das aktuelle gewissermaßen.

Und dann habe ich Tail, das liefert mir, gegeben, meinen aktuellen Datenstrom halt, naja, den Rest des Datenstroms und anerbauten, das schaltet einfach das Lesen ein Element weiter.

Also, was ich lese, irgendwelchen Inputs sage, Dankeschön, Nächster.

Und man sieht auch, dass das im Grunde das ist, was ich mit so einem Stream machen will, was mich daran interessiert.

Ich sehe ja einen Stream in erster Linie als was, was auf mich zugerollt kommt, eine Kette von Datenwerten, von Benutzereingaben, wenn ich ein Geldautomat bin, dann irgendwelche Tastendrücke, die am Gerät passieren.

Das heißt also, die Idee überhaupt einen Stream zu konstruieren ist eh so ein bisschen abwegig, was ich eher will, ist auf einen Stream zugreifen über solche Destruktoren.

Ja, und ich kann hinschreiben, einmal der Deutlichkeit halber, ich habe jetzt mal die Dinger über ihren Namen verwendet, nehmen wir mal kurz S gleich.

Naja, formulieren wir das mal einmal jetzt wirklich handfest aus, was sind denn eigentlich Ströme, Ströme sind zum Beispiel,

wenn ich jetzt als Interpretation für meinen Typ Klein a irgendeine Menge Groß a ansetze, dann soll Stream a letztlich sein,

dann die Menge aller Abbildungen von den natürlichen Zahlen nach a spricht, die Menge aller unendlichen Sequenzen von Elementen von a,

und dieses Ding, das schreibe ich dann kurz S und so eine Sequenz, so eine a, das schreibe ich gerne dann auch als so eine nicht abbrechende Folge hier.

Und dann habe ich hier einfache Definition meiner Head-and-Tail-Funktion, die natürlich jeder auch sofort raten kann.

Wenn ich mir so einen Stream nehme und davon den Head nehme, dann ist der Head einfach a0, jetzt kann er lesen, a0,

und der Tail von so einem Stream a0, a1, a2 und so weiter ist halt der Tail-Stream, der hier bei a1 anfängt, sprich das ist a1, a2 und so weiter.

Das sind natürliche Operationen auf diesen Streams.

So, und wenn ich mich jetzt mal entschlossen habe, dass die Destruktoren das sind, was mich an so einem Codatentyp interessiert,

dann werde ich das wohl also in meine Datentyp oder Codatentyp-Deklaration primär reinschreiben.

Das heißt, hier haben wir unsere erste exemplarische Codatentyp-Deklaration.

Ich mache das also genauso jetzt syntaktisch wie für Datentypen, außer dass ich eben hier statt Data-Codata schreibe.