Katamorphismen und F-Algebren

So höre ich oft die Worte “Katamorphismus” und “Rekursionsschemata”. Worum geht es?

Katamorphismen (oder Cata) sind Verallgemeinerungen des Konzepts einer Falte in der funktionalen Programmierung. Bei einer F-Algebra und einer rekursiven Datenstruktur erzeugt ein Katamorphismus einen Wert, indem er Ihre Datenstruktur rekursiv auswertet.

Was ist eine F-Algebra? Vielleicht können Sie zuerst einige Codebeispiele zeigen?

Das Setup ist nicht so einfach, also fangen wir einfach an. Angenommen, Sie haben die folgende Datenstruktur, um einen Ausdruck darzustellen:

Und ein einfacher Ausdruck kann so aussehen:

Natürlich benötigen Sie eine Funktion, um das Ergebnis auszuwerten und zu erhalten:

Dies ist, wo Katamorphismus Verallgemeinerung kommt in:

🤨, aber was ist der Sinn? Sie wenden nur ein Argument auf eine Funktion an?

Das liegt daran, dass es notReallyCata ist. Die real cata -Funktion ist generisch und hängt nicht von einer bestimmten Datenstruktur oder Evaluatorfunktion ab. Das Erstellen einer rekursiven Datenstruktur und das anschließende Umklappen ist ein häufiges Muster, das cata zu verallgemeinern versucht.

Ok, wie sieht dann die echte Cata aus?

🤯

Deshalb haben wir mit notReallyCata angefangen. Wir werden die Implementierung später aufschlüsseln, bis sie klickt. Aber jetzt fahren wir mit unserem Expression Beispiel fort. Zuerst müssen wir die Rekursion durch Einführung eines Typparameters beseitigen:

Alle Verweise auf Expression werden durch den Typparameter a ersetzt, sodass die Datenstruktur nicht mehr rekursiv ist.

Warum gibt es am Ende von Typkonstruktoren ein F ?

Schön, dass du gefragt hast — das ist ein Hinweis, dass ExpressionF ein Functor:

Nichts Besonderes, nur eine Funktion auf die umschlossene werterhaltende Struktur anwenden.

Nicht sicher, warum wir das brauchen 🤔

Es macht jetzt keinen Sinn, aber es wird ein bisschen später. Die Art und Weise, wie wir unseren Ausdruck erstellen, hat sich nicht geändert (mit Ausnahme der Konstruktornamen):

Aber der resultierende Typ ist anders:

expr reduziert alles in einem einzigen Expression, während exprF Informationen über die Verschachtelungsebene unseres Ausdrucksbaums codiert. Apropos Evaluierung: So können wir eval implementieren für ExpressionF:

Der Hauptunterschied zum Original evalExpr besteht darin, dass wir keinen rekursiven Aufruf von evalExprF (ExpressionF ist nicht rekursiv, erinnern Sie sich?). Dies bedeutet auch, dass unser Evaluator nur mit einem einstufigen Ausdruck arbeiten kann:

Und wird nicht kompilieren:

Einfach weil exprF ExpressionF Int erwartet und wir ExpressionF (ExpressionF Int) schieben.

Damit es funktioniert, könnten wir einen anderen Evaluator definieren:

Sieht irgendwie ad hoc aus, was ist, wenn Sie tief verschachtelte Ausdrücke haben?

Ja, für beliebige verschachtelte Ausdrücke ist dieser Ansatz nicht skalierbar.

Es gibt eine Möglichkeit, diese Verschachtelung mit einem neuen Typ zu verallgemeinern:

Reparieren? Sieht aus wie eine rekursive Datenstruktur, die nicht viel bewirkt. Wie ist es nützlich?

Schauen wir uns zuerst den Ausdruck vor dem Gleichheitszeichen an: Tatsächlich ist Fix eine rekursive Datenstruktur mit einem Typparameter f . Dieser Parameter hat kind * -> * zB nimmt er auch einen Typparameter. Zum Beispiel können Sie Fix , Int oder Bool nicht konstruieren, es muss so etwas wie Maybe , List oder… ExpressionF sein. Aus diesem Grund haben wir den Typparameter für ExpressionF eingeführt. Als nächstes haben wir nach dem Gleichheitszeichen einen einzelnen Typkonstruktor Fx, der ein einzelnes Argument vom Typ f (Fix f) , das im Grunde ein Ausdruck ist, der den Wert von f konstruiert. Im Falle von Maybe wäre es Maybe (Fix Maybe) und dann wird das Ganze mit Fx in den Typ Fix Maybe .

Die Typsignatur ist zunächst verwirrend zu lesen, da der Typkonstruktor denselben Namen wie der Typ selbst plus Selbstreferenzierung haben kann. Es steckt jedoch nicht viel mehr dahinter, als nur einen Typ höherer Ordnung in eine Datenstruktur einzuschließen. Übrigens ist unfix das Gegenteil von Fx und alles, was es tut, ist der Mustervergleich auf Fx und gibt den Wert zurück, keine große Sache.

Jetzt ersetzen wir jedes ExpressionF unseres Ausdrucksbaums durch Fix ExpressionF . Beachten Sie den Unterschied beim Erstellen von Ausdrücken mit und ohne Fx – sie sind im Grunde gleich, außer dass wir voranstellen müssen Fx $:

Der resultierende Typ einer ‘festen’ Version ist Fix ExpressionF Also sind wir zurück zu einer rekursiven Darstellung, aber jetzt müssen wir die Funktion unfix verwenden, um unsere nicht rekursive Datenstruktur zurückzubekommen.

Was sind die Vorteile von Fix? Sieht so aus, als wäre es der gleiche Ansatz wie der ursprüngliche Expression Typ, aber jetzt haben wir diesen seltsamen Fix und unfix Unsinn?

Ja, aber wir versuchen, den Prozess des Faltens zu verallgemeinern, es erfordert die Einführung zusätzlicher Abstraktionen, wie Fix und Algebra dass wir später diskutieren werden. Bear mit mir, es sollte später mehr Sinn machen.

Wir haben also unsere ‘feste’ Datenstruktur, wie würde die Auswertungsfunktion aussehen?

Bei einem Fix ExpressionF können wir nur unfix aufrufen, was Folgendes erzeugt ExpressionF (Fix ExpressionF):

Das zurückgegebene ExpressionF kann eines unserer ValueF , AddF oder MultF mit einem Fix ExpressionF als Typparameter sein. Es ist sinnvoll, einen Mustervergleich durchzuführen und zu entscheiden, was als nächstes zu tun ist:

Ja, es sieht genauso aus wie unser allererster rekursiver Evaluator für Expression mit dem Zusatz, den Ausdruck mit unfix auspacken zu müssen. Warum also überhaupt mit Fix ?

Hier ist der Schlüssel: wir werden unseren ursprünglichen ‘Fix-less’ Evaluator für ExpressionF wiederverwenden und ihn irgendwie über die Fix ExpressionF -Struktur verteilen. Dies sollte also eine Funktion sein, die zwei Argumente verwendet — den Evaluator und die auszuwertende Struktur:

Versuchen wir, die Implementierung herauszufinden — das erste logische, was zu tun ist, ist, unfix zu verwenden, um ExpressionF zu erhalten, und es dann vielleicht an evaluator:

Offensichtlich funktioniert das nicht, evaluator erwartet ExpressionF Int und nicht ExpressionF (Fix ExpressionF) . Denken Sie übrigens daran, dass ExpressionF ein Functor ist? Hier wird es praktisch – wir können fmap , um denselben Prozess auf die innere Ebene unseres Ausdrucksbaums anzuwenden:

Nehmen Sie sich einen Moment Zeit und überlegen Sie, was passiert: Wir übergeben eine rekursive Funktion almostCata evaluator an fmap . Wenn der aktuelle Ausdruck AddF oder MultF ist, wird diese Funktion eine Ebene tiefer übergeben und fmap wird erneut aufgerufen. Dies wird passieren, bis wir ValueF erreichen, fmapping over ValueF gibt den Wert vom Typ ExpressionF Int zurück und genau das akzeptiert unsere evaluator -Funktion.

Wenn wir uns almostCata ansehen, können wir sehen, dass es nicht wirklich etwas Spezifisches für ExpressionF oder Int Typ hat und theoretisch mit einem Typparameter verallgemeinert werden kann f . Die einzige Einschränkung sollte eine Functor Instanz für f , da wir fmap:

Und das ist die endgültige Version von cata . Hier ist die vollständige Implementierung mit einigen Anwendungsbeispielen:

Ich denke, das ist cool. Aber warum tho?

Viele Konzepte in der Kategorientheorie und der funktionalen Programmierung sind ziemlich abstrakt und manchmal ist es schwierig, eine unmittelbare praktische Anwendung für bestimmte Ideen zu finden. Die Suche nach Abstraktionen und Verallgemeinerungen ist jedoch nützlich, um Muster und elegante Lösungen für Probleme zu finden, die ansonsten eine Ad-hoc-Implementierung erfordern.

Übrigens haben wir durch die Verallgemeinerung unserer ExpressionF -> Int -Funktion auf Functor f => (f a -> a) ein weiteres wichtiges Konzept namens F-Algebra entdeckt. Grundsätzlich ist die F-Algebra ein Tripel aus Funktor f, einem Typ a und einer Evaluatorfunktion f a -> a. Beachten Sie, dass a hier nicht polymorph ist – es muss ein konkreter Typ sein, wie Int oder Bool und es wird ein Trägertyp genannt. Für jeden Endo-Funktor f können Sie mehrere darauf basierende F-Algebren erstellen. Nehmen Sie unser Ausdrucksbeispiel – endo-functor f is ExpressionF , a is Int und evaluator is evalExprF . Aber wir können den Trägertyp ändern und mehr Algebren erzeugen:

Das sind nur verschiedene Evaluatoren, die an cata übergeben werden können, oder?

Ja, wir wählen verschiedene Carrier-Typen und unsere Implementierung aus. Aber da ist der Trick — es gibt eine Mutter aller Evaluatoren, die wir erstellen können, indem wir unseren Trägertyp als … Fix ExprF auswählen.

Die Auswertung auf Int oder Bool ist völlig sinnvoll, aber was würde diese initialAlgebra auswerten? Wann muss ich Fix von etwas als Ergebnis meines Evaluators haben?

Natürlich werden Sie so etwas nicht selbst schreiben, sondern wollen Ihnen nur die tiefere Bedeutung hinter f-Algebren und cata zeigen. Tatsächlich haben wir bereits eine Implementierung für einen solchen Evaluator und das ist genau Fx .:

Warte, Fx ist ein Evaluator? Das ist verrückt.

Ja, und es macht das Einfachste, was Sie tun können — speichern Sie die Expession in einer Datenstruktur. Während alle anderen Evaluatoren (algebra0, algebra1 ) einen Wert erzeugten, indem sie den Ausdruck reduzierten (z. B. Summe oder Verkettung), umschließt Fx den Ausdruck einfach, ohne Daten zu verlieren.

Aus diesem Grund haben wir zuerst Fix eingeführt — Sie bewerten zuerst Ihre ursprüngliche Datenstruktur mit Fx in die Anfangsalgebra Fix f und dann mit cata Die ‘echte’ Auswertung erfolgt durch fmaping Ihr konkreter Evaluator über die Anfangsalgebra.

Aus kategorietheoretischer Sicht bilden alle Algebren, die auf demselben Endofunktor basieren, eine Kategorie. Diese Kategorie hat ein Anfangsobjekt, das unsere anfängliche Algebra ist, die durch Auswahl des Trägertyps als Fix f erstellt wurde. Es gibt einige großartige Blogbeiträge von Bartosz Milewski, die ich dringend empfehle, wenn Sie ein tiefes kategorisches Verständnis erlangen möchten.

Es ist immer noch ziemlich schwer zu verstehen, ich glaube nicht, dass ich das Konzept vollständig verstehe

Es ist immer besser, es selbst zu tun: Versuchen Sie, Fix und cata selbst neu zu implementieren, denken Sie über mögliche Datenstrukturen und Algebren nach. Beispielsweise kann ein String rekursiv dargestellt werden (als Char Kopf und Schwanz von String), der length einer Zeichenfolge kann mit cata berechnet werden. Hier sind einige großartige Ressourcen zum weiteren Lesen:

• F-Algebren und etwas andere F-Algebren verstehen von Bartosz Milewski
• Katamorphismen in 15 Minuten von Chris Jones
• Reine funktionale Datenbankprogrammierung mit Fixpunkttypen von Rob Norris
• Katamorphismen im Haskell Wiki
• Praktische Rekursionsschemata von Jared Tobin