Frage über (ko-)induktive Datentypen

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Frage über (ko-)induktive Datentypen
In dem Skript zur Vorlesung wurde in Bezug auf induktive und koinduktive Datentypen der Begriff eines Mengenkonstruktors und einer Algebra eingeführt.

Was hat es denn hiermit genau auf sich? Insbesondere würde mich interessieren welche Rolle der Mengenkonstruktor in Bezug auf die Algebra spielt und wie man diesen für einen gegebenen koinduktiven Datentypen findet.

Vielen Dank im Vorraus für Antworten. : )


Grundsätzlich sind die beiden Konzepte dual. Ein induktiver Datentyp ist die initiale F-Algebra FX → X für eine Mengenkonstruktion F und ein koinduktiver Datentyp ist die terminale G-Koalgebra X → GX für eine Mengenkonstruktion G.

Beispielsweise hat man beim induktiven Typ der Listen über einem Parametertyp A die Konstruktion FX = 1 + AX. Die initiale F-Algebra ist dann List(A) mit der Abbildung 1 + AList(A) → List(A), und die Summanden in F entsprechen den Konstruktoren nil: 1 → List(A) und cons: A*List(A) → List(A).

Beim koinduktiven Typ der Streams über A ist die Konstruktion GX = AX und Stream(A) ist die terminale G-Koalgebra mit der Abbildung Stream(A) → AStream(A). Die Observer von Stream(A) entsprechen in diesem Fall den Faktoren in G, also hat man hd: Stream(A) → A und tl: Stream(A) → Stream(A).

Wenn man jetzt von den Konstruktoren eines gegebenen induktiven Typs oder den Observern eines gegebenen koinduktiven Typs auf die Mengenkonstruktion zurückschließen will, muss man die entsprechende Konstruktion umkehren, also bei einem induktiven Typ die Summe der linken Seiten oder bei einem koinduktiven Typ das Produkt der rechten Seiten bilden.