In letzter Zeit habe ich endlich das Gefühl, Katamorphismen zu verstehen. Ich habe etwas über sie in eine aktuelle Antwort geschrieben, aber kurz würde ich sagen, dass ein Katamorphismus für einen Typ über den rekursiven Prozess abstrahiert Durchqueren eines Wertes dieses Typs, wobei das Muster für diesen Typ in eine Funktion für jeden Konstruktor übereinstimmt, den der Typ hat. Ich würde zwar gerne Korrekturen zu diesem Punkt oder zu der längeren Version in der oben verlinkten Antwort begrüßen, aber ich denke, ich habe mehr oder weniger Probleme damit, und das ist nicht das Thema dieser Frage, nur ein Hintergrund.
Sobald ich festgestellt habe, dass die Funktionen, die Sie an einen Katamorphismus übergeben, genau den Konstruktoren des Typs entsprechen und die Argumente dieser Funktionen ebenfalls den Typen der Felder dieser Konstruktoren entsprechen, fühlt sich alles plötzlich ziemlich mechanisch an und ich sehe es nicht wo es Spielraum für alternative Implementierungen gibt.
Ich habe zum Beispiel diesen albernen Typ erfunden, ohne wirklich zu wissen, was seine Struktur "bedeutet", und daraus einen Katamorphismus abgeleitet. Ich sehe keine andere Möglichkeit, eine allgemeine Falte über diesen Typ zu definieren:
%Vor%Meine Frage ist, hat jeder Typ eine einzigartige Katamorphose (bis zur Neuordnung von Argumenten)? Oder gibt es Gegenbeispiele: Typen, für die kein Katamorphismus definiert werden kann, oder Typen, für die es zwei verschiedene, aber gleichermaßen sinnvolle Katamorphismen gibt? Wenn es keine Gegenbeispiele gibt (d. H. Der Katamorphismus für einen Typ ist einzigartig und trivial ableitbar), ist es dann möglich, GHC dazu zu bringen, eine Art Klasse für mich abzuleiten, die diese Plackerei automatisch ausführt?
Der einem rekursiven Typ zugeordnete Katamorphismus kann mechanisch abgeleitet werden.
Angenommen, Sie haben einen rekursiv definierten Typ mit mehreren Konstruktoren, jeder mit seiner eigenen Arität. Ich werde das Beispiel von OP ausleihen.
%Vor% Dann können wir den gleichen Typ umschreiben, indem wir jede Arität zwingen, eins zu sein und alles zu entschärfen. Arity zero ( B ) wird eins, wenn wir einen Einheitentyp () hinzufügen.
Dann können wir die Anzahl der Konstruktoren auf eins reduzieren, indem wir Either anstelle von mehreren Konstruktoren ausnutzen. Im Folgenden schreiben wir einfach Infix + anstelle von Either .
Auf der Termebene wissen wir, dass wir jede rekursive Definition umschreiben können
als die Form x = f x where f w = ... , schreibe eine explizite Fixpunktgleichung x = f x . Auf Typ-Ebene können wir dieselbe Methode verwenden
rekursive Typen refinern.
Nun stellen wir fest, dass wir eine Funktorinstanz automatisch ausgeben können.
%Vor% Dies ist möglich, weil im ursprünglichen Typ jede rekursive Referenz nur in der positiven -Position auftrat. Wenn dies nicht gilt, macht F a b f keinen Funktor, dann können wir keine Katamorphose haben.
Schließlich können wir den Typ von cata wie folgt schreiben:
Ist dies der xCata -Typ des OP? Es ist. Wir müssen nur ein paar Typisomorphismen anwenden. Wir verwenden die folgenden algebraischen Gesetze:
Übrigens ist es leicht, sich an diese Isomorphismen zu erinnern, wenn wir (a,b) als ein Produkt a*b , Einheit () als 1 und a->b als eine Macht b^a schreiben. Tatsächlich werden sie 1) c^(a*b) = (c^a)^b , 2) c^(a+b) = c^a*c^b, 3) c^1 = c .
Wie auch immer, fangen wir an, den F a b f w -> w part nur neu zu schreiben
Betrachten wir jetzt den vollständigen Typ:
%Vor% Was ist tatsächlich (umbenennen w=r ) der gewünschte Typ
Die "Standard" -Implementierung von cata ist
Es bedarf einiger Anstrengungen, um aufgrund seiner Allgemeinheit zu verstehen, aber dies ist in der Tat die Absicht.
Über Automatisierung: Ja, das kann zumindest teilweise automatisiert werden.
Da ist das Paket recursion-schemes auf hackage was erlaubt
man schreibt so etwas wie
Beispiel:
%Vor%Tags und Links haskell