Ich versuche, meinen Kopf um F-Algebren zu bekommen, und dieser Artikel macht einen hübschen Eindruck Gut gemacht. Ich verstehe die Vorstellung einer dualen Kategorientheorie, aber es fällt mir schwer zu verstehen, wie F-Coalgebras (das Duale von F-Algebren) mit faulen Datenstrukturen in Haskell zusammenhängen.
F-Algebren werden mit einem endofunctor mit der Funktion beschrieben: F a - & gt; a, was Sinn macht, wenn Sie an F a als Ausdruck denken, und als Ergebnis der Bewertung dieses Ausdrucks, wie der verlinkte Artikel es erklärt.
Als das Duale von F-Algebren wäre die entsprechende Funktion für ein F-Coalgebra ein - & gt; F a. Wikipedia sagt, dass F-Coalgebras verwendet werden können, um unendliche, faule Datenstrukturen zu erstellen. Wie funktioniert das a - & gt; Können Sie mit einer Funktion unendliche, faule Datenstrukturen erstellen? In diesem Sinne, da Haskell im Kern faul ist, sind die meisten Datentypen in Haskell F-Coalgebras statt F-Algebren? Werden F-Algebren nicht faul ausgewertet?
Wenn Datentypen (oder zumindest diejenigen, die sind, die zu unendlichen Daten fähig sind) auf F-Coalgebras in Haskell basieren, was ist das a - & gt; ZB eine Funktion für Listen? Was ist das Terminal F-Coalgebra für Listen?
Eine unendliche Liste [1,2,3,4 ...] könnte in Haskell so aussehen:
%Vor%Verwendet das irgendwie F-Coalgebras? Benötigen unendliche Datenstrukturen neben der Verwendung von F-Coalgebras auch eine faulige Bewertung und Rekursion? Fehle ich hier etwas?
Ein Coalgebra A -> F A
kann verwendet werden, um die äußere Schicht einer (möglicherweise unendlichen) Datenstruktur abzuschälen. Für Listen von X
ist der Funktor F a = Maybe (X, a)
, derselbe wie in der algebraischen Ansicht. In Haskell ist die Funktion für die Kohlebra
unfoldr
ist die Entfaltung, die dieser Kohlebra entspricht, genau wie foldr
die dieser Algebra entsprechende Faltung ist.
Wenn Sie [a]
nicht als Typ von Listen betrachten, sondern als Art von Beschreibungen von Listen oder Programmen, dann können Sie (scheinbar) unendliche Werte nur mit einer notwendigerweise endlichen Beschreibung konstruieren.
Wie man sieht, sieht eine Haskell-Liste sowohl wie eine F-Algebra als auch eine F-Coalgebra aus. Dies ist möglich, weil Haskell nicht konsistent ist. Sie können eine Entfaltung falten und eine Endlosschleife erhalten. Sprachen wie coq und agda unterscheiden zwischen Datentypen (F-Algebren) und Codatentypen (F-Coalgebren) explizit. In diesen Sprachen gibt es zwei Listentypen, eine algebraische List
und eine coalgebraische Colist
.
Tags und Links haskell category-theory