Soweit ich weiß, entsprechen rekursive Datentypen von Haskell den ursprünglichen Algebren von Endofunctors aus der Kategorie Hask [ 1 , 2 ]. Zum Beispiel:
data Nat = Zero | Succ Nat , entsprechen der ursprünglichen Algebra des endofunctor F(-) = 1 + (-) . data List a = Nil | Cons a (List a) , entsprechen der ursprünglichen Algebra von endofunctor F(A, -) = 1 + A × (-) . Allerdings ist mir nicht klar, was der Rosenknospen-Endofaktor sein sollte:
%Vor%Was mich verwirrt ist, dass es zwei Rekursionen gibt: eine für den Rosenbaum und die andere für die Liste. Nach meinen Berechnungen würde ich den folgenden Funktor bekommen, aber es scheint nicht richtig zu sein:
%Vor%Alternativ können Rosenbäume als gegenseitig rekursive Datentypen definiert werden:
%Vor%Haben gegenseitig rekursive Datentypen eine Interpretation in der Kategorientheorie?
Ich würde davon abraten, von der "Hask-Kategorie" zu sprechen, weil sie dich unbewusst davon abhält, nach einer anderen kategorischen Struktur in der Haskell-Programmierung zu suchen.
Tatsächlich können Rosenbäume als der Fixpunkt eines Endofunktors für Typen und Funktionen angesehen werden, eine Kategorie, die wir besser als Type bezeichnen könnten, jetzt da Type der Typ von Typen ist. Wenn wir uns ein paar der üblichen Funktorkits geben ...
... und Fixpunkte ...
%Vor%... dann können wir
nehmen %Vor% Die Tatsache, dass [] selbst rekursiv ist, verhindert nicht seine Verwendung bei der Bildung von rekursiven Datentypen über Fix . Um die Rekursion explizit zu buchstabieren, haben wir Fixpunkte verschachtelt, hier mit suggestiv ausgewählten gebundenen Variablennamen:
Wenn wir nun im zweiten Fixpunkt angekommen sind, haben wir eine Typformel
%Vor% was sowohl in rose als auch in list funktoriell (in der Tat streng positiv) ist. Man könnte sagen, es ist ein Bifunctor , aber das ist eine unnötige Terminologie: Es ist ein Funktor von (Type, Type) bis Type . Sie können einen Type -> Type -Funktor machen, indem Sie einen Fixpunkt in der zweiten Komponente des Paares nehmen, und genau das ist oben passiert.
Die obige Definition von Rose verliert eine wichtige Eigenschaft. Es stimmt nicht, dass
nur das Rose x :: Type if x :: Type . Insbesondere
ist keine gut typisierte Einschränkung, was schade ist, denn Rosenbäume sollten in den Elementen, die sie speichern, eine Funktion haben.
Sie können das beheben, indem Sie Rose als Fixpunkt für Bifunctor erstellen. Wenn wir also zu Listen kommen, haben wir drei -Typ-Variablen im Bereich, a , rose und list , und wir haben in allen Funktionen eine Funktion. Sie benötigen einen anderen Fixpunkttypkonstruktor und ein anderes -Kit zum Erstellen von Bifunctor -Instanzen: Für Rose wird das Leben leichter, da der Parameter a nicht verwendet wird im inneren Fixpunkt, aber im Allgemeinen, um bifunctors als fixpoints zu definieren erfordert Trifunctors, und los geht's!
Diese Antwort zeigt, wie man die Verbreitung bekämpfen kann, indem man zeigt, wie indexierte -Typen sind closed unter einer Fixpunkt-von-Funktor-Konstruktion. Das heißt, arbeiten Sie nicht in Type , sondern in i -> Type (für die gesamte Vielfalt von Indextypen i ) und Sie sind bereit für gegenseitige Rekursion, GADTs und so weiter.
Beim Herauszoomen werden Rosenbäume durch gegenseitige Fixpunkte angegeben, die eine vollkommen sinnvolle kategorische Beschreibung haben, vorausgesetzt, Sie sehen, welche Kategorien tatsächlich funktionieren.
Dies ist nicht wirklich eine Antwort auf die Frage, die Sie stellen, aber vielleicht trotzdem interessant. Beachten Sie das mit
%Vor% und die Tatsache, dass * über + verteilt, haben Sie
(die Gleichheit bedeutet wirklich Isomorphie). Du hättest also genauso gut definieren können,
%Vor%oder in Haskell,
%Vor%Das heißt, Rosenbäume sind isomorph zu gewöhnlichen (blattmarkierten) Binärbäumen und bilden eindeutig eine normale Anfangsalgebra.
Wie Sie bemerkt haben, ist die Definition des Funktors für Rose a komplizierter, da das rekursive Vorkommen des Typs in List eingefügt wird. Das Problem ist, dass List selbst ein rekursiver Typ ist, der als fester Punkt erhalten wird. List (Rose a) entspricht im Grunde einer "beliebigen Anzahl von Elementen von Rose a ", etwas, das man nicht mit einer Signatur von Produkten und Summen allein ausdrücken kann, daher die Notwendigkeit zusätzlicher Abstraktion über diese multiplen Rekursivpunkte.
Ein Funktor F A - : * -> * wird nicht funktionieren, da wir etwas finden müssen, dass
Eine Möglichkeit besteht darin, List einfach als primitiv zu behandeln. Dann ist Rose a nur der Fixpunkt von
Eine andere, interessantere Möglichkeit besteht darin, dem Vorschlag in der von Ihnen geposteten Referenz zu folgen und zu beachten, dass der Typ von Rose a verallgemeinert werden kann, um über den Funktor zu abstrahieren, in dem das rekursive Vorkommen in
now GRose hat den Typ (* -> *) -> (* -> *) , daher ist es ein Funktor höherer Ordnung, der einen endofunctor in einen anderen ordnet. In unserem Beispiel würde es den Funktor List auf den Typ der Rosenbäume abbilden.
Beachten Sie jedoch, dass GRose immer noch rekursiv ist, so dass das oben Gesagte eher eine Isomorphie als eine Lösung für unser Problem darstellt. Wir können versuchen, dies zu beheben, indem wir zusätzlich über den rekursiven Punkt abstrahieren
%Vor% Beachten Sie, dass HRose nun ein regulärer Funktor höherer Ordnung vom Typ ((* -> *) -> (* -> *)) -> (* -> *) -> (* -> *) ist und daher Funktoren höherer Ordnung in Funktoren höherer Ordnung ordnet. Die Berechnung des kleinsten Fixpunktes von HRose gibt uns
Wenn wir also Rose ≡ μ(HRose) List setzen, erhalten wir
das ist genau die definierende Gleichung für Rosenbäume. Sie finden viele weitere Beispiele für die Theorie und Praxis generischer Programmierung mit Fixpunkten über Funktoren höherer Ordnung. Hier zum Beispiel, Bird und Paterson entwickeln es im Kontext verschachtelter Datentypen ( aber die Definitionen gelten im Allgemeinen eindeutig). Sie zeigen auch die systematische Konstruktion von Falten über so definierte Datentypen sowie verschiedene Gesetze.
Sie scheinen zu verstehen, wie dies modelliert ist
%Vor% indem für jede gegebene A die Anfangsalgebra des endofunctor F(A, -) = 1 + A × (-) genommen wird. Nennen wir diese erste Algebra L(A) .
Wenn wir den Morphismus in L(A) vergessen, können wir sagen, dass L(A) ein Objekt unserer Kategorie ist. Besser, L(-) ist nicht nur eine Zuordnung von Objekten zu Objekten, sondern kann auch als endofunctor betrachtet werden.
Wenn L der Anfangswert von endofunctor ist, wird der rekursive Typ
wird interpretiert, indem für jede A m die Anfangsalgebra des Funktors
Dies ist ein Funktor, der durch Zusammenstellen von L und * (und dem Diagonal-Funktor) erhalten wird.
Daher funktioniert derselbe Ansatz.
Tags und Links haskell category-theory recursion algebraic-data-types algebra