Qual è il tipo di un catamorfismo (piega) per tipi ricorsivi non regolari?

Question

Molti catamorfismi sembrano essere abbastanza semplici, sostituendo per lo più ogni costruttore di dati con una funzione personalizzata, ad es.

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 

Tuttavia, ciò che non è chiaro per me è quello che succede se si utilizza lo stesso tipo di costruzione, ma con un argomento di tipo diverso. Per esempio. invece di passare un List a-Cons, che dire

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

O, forse un caso più folle:

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

Le due idee plausibili che ho per la parte ??? sono

• (a -> b -> b) , ovvero sostituire tutte le applicazioni del costruttore List in modo ricorsivo)
• (a -> List b -> b), cioè semplicemente la sostituzione di tutte le applicazioni List a.

Quale dei due sarebbe corretto - e perché? O sarebbe qualcosa di completamente diverso?

Answer 1

Questa è una risposta parziale, solo.

Il problema che l'OP solleva è: come definire fold/cata nel caso di tipi ricorsivi non regolari?

Dal momento che non mi fido a farlo correttamente, ricorro a chiedere invece a Coq. Iniziamo da un tipo di lista ricorsiva semplice e regolare.

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

Niente di speciale qui, List A è definito in termini di List A. (Ricordati di questo - ci torneremo sopra.)

E lo cata? Esaminiamo il principio dell'induzione.

> 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 

Vediamo. I tipi dipendenti di exploit di cui sopra: P dipendono dal valore effettivo dell'elenco. Semplifichiamolo manualmente nel caso P list è un tipo costante B. Otteniamo:

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

che può essere scritta come equivalentemente

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

Quale è foldr tranne che la "lista corrente" è anche passato alla argomento della funzione binaria - non una grande differenza.

Ora, in Coq possiamo definire un elenco in un altro modo sottilmente diverso:

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

sembra lo stesso tipo, ma c'è una differenza profonda. Qui non stiamo definendo il tipo List A in termini di List A.Piuttosto, stiamo definendo una funzione di tipo List2 : Type -> Type in termini di List2. Il punto principale di questo è che i riferimenti ricorsivi a List2 non devono essere applicati a A - il fatto che sopra lo facciamo è solo un incidente.

In ogni caso, vediamo il tipo per il principio di induzione:

> 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 

Rimuoviamo l'argomento List2 T da P come abbiamo fatto prima, in pratica assumendo P è costante su di esso.

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 

Equivalentemente riscritta:

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 

che corrisponde approssimativamente, in Haskell notazione

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

Non così male - lo scenario di base deve ora essere una funzione polimorfa, tanto quanto Empty in Haskell è. Ha un senso. Allo stesso modo, il caso induttivo deve essere una funzione polimorfica, come lo è lo Cons. C'è un argomento extra List2 a, ma possiamo ignorarlo, se vogliamo.

Ora, quanto sopra è ancora una sorta di piegatura/cata su un regolare tipo. Che dire di quelli non regolari? Studierò

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

che a Coq diventa:

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

con principio di induzione:

> 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 

Rimozione della parte "dipendente":

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 notazione :

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

A parte l'argomento aggiuntivo List3 (a, a), questo è un tipo di piegatura.

Infine, che dire del tipo di OP?

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

Purtroppo, Coq non accetta il tipo

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

poiché l'interno List4 evento non è in una posizione strettamente positiva. Questo è probabilmente un suggerimento che dovrei smettere di essere pigro e usare Coq per fare il lavoro, e iniziare a pensare alle F-algebre coinvolte da solo ... ;-)