Was ist der Typ einer Katamorphose (Faltung) für nicht-reguläre rekursive Typen?

Question

Viele Katamorphismen scheinen einfach genug zu sein, wobei meistens jeder Datenkonstruktor durch eine benutzerdefinierte Funktion ersetzt wird, z.

data Bool = False | True 
foldBool :: r    -- False constructor 
     -> r    -- True constructor 
     -> Bool -> r 

data Maybe a = Nothing | Just a 
foldMaybe :: b    -- Nothing constructor 
      -> (a -> b)  -- Just constructor 
      -> Maybe a -> b 

data List a = Empty | Cons a (List a) 
foldList :: b    -- Empty constructor 
     -> (a -> b -> b) -- Cons constructor 
     -> List a -> b 

Doch was ist mir nicht klar ist, was passiert, wenn der gleiche Typ-Konstruktor verwendet wird, aber mit einem anderen Typ Argumente. Z.B. anstelle eines List a-Cons vorbei, was

data List a = Empty | Cons a (List (a,a)) 

Oder vielleicht ein verrückter Fall:

data List a = Empty | Cons a (List (List a)) 
foldList :: b    -- Empty constructor 
     -> ???   -- Cons constructor 
     -> List a -> b 

Die beiden plausible Ideen, die ich für den ??? Teil haben, sind

• (a -> b -> b) , dh ersetze alle Anwendungen des List Konstruktors rekursiv)
• (a -> List b -> b), d.h. lediglich alle List a Anwendungen ersetzend.

Welche der beiden wäre richtig - und warum? Oder wäre es etwas ganz anderes?

Answer 1

Dies ist nur eine Teilantwort.

Das Problem, das das OP aufwirft, ist: Wie definiert man fold/cata im Fall von nicht-regulären rekursiven Typen?

Da ich mir nicht traue, das richtig zu machen, werde ich mich stattdessen an Coq wenden. Beginnen wir mit einem einfachen, rekursiven Listentyp.

Inductive List (A : Type) : Type := 
    | Empty: List A 
    | Cons : A -> List A -> List A 
. 

Nichts Besonderes, hier wird List A in Bezug auf List A definiert. (Denken Sie daran - wir kommen wieder darauf zurück.)

Was ist mit der cata? Lassen Sie uns das Induktionsverfahren abfragen.

> Check List_rect. 
forall (A : Type) (P : List A -> Type), 
    P (Empty A) -> 
    (forall (a : A) (l : List A), P l -> P (Cons A a l)) -> 
    forall l : List A, P l 

Mal sehen. Das obige nutzt abhängige Typen aus: P hängt vom tatsächlichen Wert der Liste ab. Lassen Sie es einfach manuell in dem Fall P list ist ein konstanter Typ B. Wir erhalten:

forall (A : Type) (B : Type), 
    B -> 
    (forall (a : A) (l : List A), B -> B) -> 
    forall l : List A, B 

, die äquivalent als

geschrieben werden kann

forall (A : Type) (B : Type), 
    B -> 
    (A -> List A -> B -> B) -> 
    List A -> B 

Welche foldr außer, dass die „aktuelle Liste“ wird auch auf die binäre Funktion Argument übergeben - kein großer Unterschied.

, jetzt in Coq können wir eine Liste in einem anderen auf subtile Weise anders definieren:

Inductive List2 : Type -> Type := 
    | Empty2: forall A, List2 A 
    | Cons2 : forall A, A -> List2 A -> List2 A 
. 

Es denselben Typ aussieht, aber es gibt einen großen Unterschied. Hier definieren wir nicht den Typ List A in Bezug auf List A.Stattdessen definieren wir eine Typ-Funktion List2 : Type -> Type in Bezug auf List2. Der Hauptpunkt dabei ist, dass die rekursiven Verweise auf List2 nicht auf A angewendet werden müssen - die Tatsache, dass wir oben nur einen Vorfall haben.

Wie auch immer, lassen Sie uns den Typ für das Induktionsprinzip siehe:

> Check List2_rect. 
forall P : forall T : Type, List2 T -> Type, 
    (forall A : Type, P A (Empty2 A)) -> 
    (forall (A : Type) (a : A) (l : List2 A), P A l -> P A (Cons2 A a l)) -> 
    forall (T : Type) (l : List2 T), P T l 

Lassen Sie uns das List2 T Argument von P entfernen, wie wir vorher, im Grunde davon aus P auf sie konstant ist.

forall P : forall T : Type, Type, 
    (forall A : Type, P A) -> 
    (forall (A : Type) (a : A) (l : List2 A), P A -> P A) -> 
    forall (T : Type) (l : List2 T), P T 

Gleichwertig neu geschrieben:

forall P : (Type -> Type), 
    (forall A : Type, P A) -> 
    (forall (A : Type), A -> List2 A -> P A -> P A) -> 
    forall (T : Type), List2 T -> P T 

was in etwa entspricht, in Haskell Notation

(forall a, p a) ->       -- Empty 
(forall a, a -> List2 a -> p a -> p a) -> -- Cons 
List2 t -> p t 

Gar nicht so schlecht - das Basismodell hat jetzt eine polymorphe Funktion sein, so sehr Empty in Haskell ist. Es macht Sinn. Ähnlich muss der induktive Fall eine polymorphe Funktion sein, so wie es Cons ist. Es gibt ein extra List2 a Argument, aber wir können das ignorieren, wenn wir wollen.

Jetzt ist das oben genannte immer noch eine Art falten/cata auf einem regulären Typ. Was ist mit nicht regulären? Ich werde

data List a = Empty | Cons a (List (a,a)) 

Studie, die in Coq wird:

Inductive List3 : Type -> Type := 
    | Empty3: forall A, List3 A 
    | Cons3 : forall A, A -> List3 (A * A) -> List3 A 
. 

mit Induktionsprinzip:

> Check List3_rect. 
forall P : forall T : Type, List3 T -> Type, 
    (forall A : Type, P A (Empty3 A)) -> 
    (forall (A : Type) (a : A) (l : List3 (A * A)), P (A * A) l -> P A (Cons3 A a l)) -> 
    forall (T : Type) (l : List3 T), P T l 

den "abhängig" Teil ausbauen:

forall P : (Type -> Type), 
    (forall A : Type, P A) -> 
    (forall (A : Type), A -> List3 (A * A) -> P (A * A) -> P A) -> 
    forall (T : Type), List3 T -> P T 

In Haskell Notation :

(forall a. p a) ->          -- empty 
    (forall a, a -> List3 (a, a) -> p (a, a) -> p a) -> -- cons 
    List3 t -> p t 

Abgesehen von der zusätzlichen List3 (a, a) Argument ist dies eine Art von Falte.

Schließlich, was ist mit dem OP-Typ?

data List a = Empty | Cons a (List (List a)) 

Ach, Coq nicht akzeptieren, die Art

Inductive List4 : Type -> Type := 
    | Empty4: forall A, List4 A 
    | Cons4 : forall A, A -> List4 (List4 A) -> List4 A 
. 

da die inneren List4 Auftreten nicht in einer streng positiven Position ist. Das ist wahrscheinlich ein Hinweis darauf, dass ich aufhören sollte, faul zu sein und Coq zu benutzen, um die Arbeit zu machen und über die beteiligten F-Algebren alleine nachzudenken ... ;-)