Chcę móc używać cata
z pakietu dla list w kodowaniu Kościoła.Katamorfizmy dla list zakodowanych w kościele
type ListC a = forall b. (a -> b -> b) -> b -> b
Dla wygody stosowałem typ drugiego rzędu, ale mnie to nie obchodzi. Jeśli uważasz, że jest to konieczne, dodaj numer newtype
, użyj GADT itp.
Pomysł kodowania Kościele jest powszechnie znany i prosty:
three :: a -> a -> a -> List1 a
three a b c = \cons nil -> cons a $ cons b $ cons c nil
zasadzie „streszczenie nieokreślone” cons
i nil
są używane zamiast „normalnych” konstruktorów. Wierzę, że wszystko może być zakodowane w ten sposób (Maybe
, drzewa itp.).
Łatwo pokazać, że List1
rzeczywiście jest izomorficzna normalnych list:
toList :: List1 a -> [a]
toList f = f (:) []
fromList :: [a] -> List1 a
fromList l = \cons nil -> foldr cons nil l
Więc jego podstawa funktor jest taka sama jak list, i powinno być możliwe do wdrożenia project
dla niego i używać maszyn z recursion-schemes
.
Ale nie mogłem, więc moje pytanie brzmi "jak to zrobić?". Dla normalnych list, mogę tylko wzór mecz:
decons :: [a] -> ListF a [a]
decons [] = Nil
decons (x:xs) = Cons x xs
Ponieważ nie wzór meczu na funkcji może muszę użyć krotnie dekonstrukcji listę. Mógłbym napisać krotny oparte project
dla normalnych list:
decons2 :: [a] -> ListF a [a]
decons2 = foldr f Nil
where f h Nil = Cons h []
f h (Cons hh t) = Cons h $ hh : t
Jednak nie udało mi się dostosować go do listy kościelnych zakodowane:
-- 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
ma następujący podpis:
cata :: Recursive t => (Base t a -> a) -> t -> a
Aby używać go z moimi listami, potrzebuję:
- Aby zadeklarować typ bazowy funktora na liście przy użyciu
type family instance Base (ListC a) = ListF a
- celu realizacji
instance Recursive (List a) where project = ...
zawiodę w obu etapach.
Jaka jest Twoja wina? Próbowałem tego (dodając "newtype" dla wygody) i działa dobrze. – MigMit
Zaktualizowałem moje pytanie: – nponeccop
"Nowy typ" okazał się niezbędny, a nie tylko udogodnieniem. Kod działa teraz. – nponeccop