Catamorphismen für Church-codierte Listen

Question

Ich möchte cata von recursion-schemes Paket für Listen in der Kirche Codierung verwenden können.

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

Ich benutzte einen zweiten Rang-Typ für die Bequemlichkeit, aber das ist mir egal. Fühlen Sie sich frei, eine newtype hinzuzufügen, verwenden Sie GADTs usw., wenn Sie das Gefühl haben, dass es notwendig ist.

Die Idee der Kirche Codierung ist weithin bekannt und einfach:

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

Im Grunde genommen „abstrakt nicht spezifiziert“ cons und nil anstelle von „normalen“ Konstrukteuren verwendet. Ich glaube, dass alles auf diese Weise kodiert werden kann (Maybe, Bäume, etc.).

Es ist leicht zu zeigen, dass List1 in den normalen Listen tatsächlich isomorph ist:

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

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

So seine Basis Funktors ist die gleiche wie von Listen, und es sollte möglich sein, es zu implementieren project und verwenden Sie die Maschinen aus recursion-schemes.

Aber ich konnte nicht, also meine Frage ist "wie mache ich das?". Für den normalen Listen, kann ich Muster Spiel gerade:

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

Da ich nicht Muster-Match auf Funktionen können, muss ich eine Falte verwenden, um die Liste zu dekonstruieren. Ich konnte eine Falte basierte project für normale Listen schreiben:

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

jedoch scheiterte ich es für Church-kodierte Listen anpassen:

-- 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 hat die folgende Signatur:

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

Um es mit meinen Listen zu verwenden, brauche ich:

1. Um die Basis Funktors Typ für die Liste deklarieren mit type family instance Base (ListC a) = ListF a
2. Um instance Recursive (List a) where project = ...

ich an beiden Schritte nicht zu implementieren.

Answer 1

Die newtype Wrapper erwies sich als der entscheidende Schritt, den ich verpasste. Hier ist der Code zusammen mit einer Beispielkatamorphose von .

{-# 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