Catamorfismi per elenchi codificati dalla Chiesa

Question

Desidero poter usare il pacchetto cata dal recursion-schemes per gli elenchi nella codifica della Chiesa.

type ListC a = forall b. (a -> b -> b) -> b -> b 

Ho usato un secondo tipo per comodità, ma non mi interessa. Sentiti libero di aggiungere uno newtype, utilizzare GADT, ecc. Se ritieni che sia necessario.

L'idea di codifica Chiesa è ampiamente noto e semplice:

three :: a -> a -> a -> List1 a 
three a b c = \cons nil -> cons a $ cons b $ cons c nil 

Fondamentalmente "astratto specificato" cons e nil sono usati al posto dei costruttori "normali". Credo che tutto possa essere codificato in questo modo (Maybe, alberi, ecc.).

E 'facile dimostrare che List1 è davvero isomorfo a liste normali:

toList :: List1 a -> [a] 
toList f = f (:) [] 

fromList :: [a] -> List1 a 
fromList l = \cons nil -> foldr cons nil l 

Così la sua functor di base è la stessa delle liste, e dovrebbe essere possibile implementare project per esso e utilizzare i macchinari da recursion-schemes.

Ma non potevo, quindi la mia domanda è "come faccio?". Per gli elenchi normali, posso solo pattern match:

decons :: [a] -> ListF a [a] 
decons [] = Nil 
decons (x:xs) = Cons x xs 

Dal momento che non pattern-match di funzioni, devo usare una piega di decostruire la lista. Potrei scrivere un fold-based project per le liste normali:

decons2 :: [a] -> ListF a [a] 
decons2 = foldr f Nil 
    where f h Nil = Cons h [] 
     f h (Cons hh t) = Cons h $ hh : t 

Tuttavia non sono riuscito ad adattarlo per gli elenchi Chiesa-encoded:

-- decons3 :: ListC a -> ListF a (ListC a) 
decons3 ff = ff f Nil 
    where f h Nil = Cons h $ \cons nil -> nil 
     f h (Cons hh t) = Cons h $ \cons nil -> cons hh (t cons nil) 

cata ha la seguente firma:

cata :: Recursive t => (Base t a -> a) -> t -> a 

Per utilizzarlo con i miei elenchi, ho bisogno di:

1. per dichiarare il tipo di base funtore per l'elenco utilizzando type family instance Base (ListC a) = ListF a
2. Per implementare instance Recursive (List a) where project = ...

non riesco ad entrambe le fasi.

Answer 1

L'involucro newtype si è rivelato essere il passaggio cruciale che ho perso. Ecco il codice insieme a un esempio di catamorfismo da recursion-schemes.

{-# LANGUAGE LambdaCase, Rank2Types, TypeFamilies #-} 

import Data.Functor.Foldable 

newtype ListC a = ListC { foldListC :: forall b. (a -> b -> b) -> b -> b } 

type instance Base (ListC a) = ListF a 

cons :: a -> ListC a -> ListC a 
cons x (ListC xs) = ListC $ \cons' nil' -> x `cons'` xs cons' nil' 
nil :: ListC a 
nil = ListC $ \cons' nil' -> nil' 

toList :: ListC a -> [a] 
toList f = foldListC f (:) [] 
fromList :: [a] -> ListC a 
fromList l = foldr cons nil l 

instance Recursive (ListC a) where 
    project xs = foldListC xs f Nil 
    where f x Nil = Cons x nil 
      f x (Cons tx xs) = Cons x $ tx `cons` xs 

len = cata $ \case Nil -> 0 
        Cons _ l -> l + 1