Катаморфизм для церковных списков

Question

Я хочу, чтобы иметь возможность использовать cata от recursion-schemes пакет для списков в церковном кодировании.

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

Для удобства я использовал тип второго ранга, но мне все равно. Не стесняйтесь добавлять newtype, используйте GADT и т. Д., Если вы считаете, что это необходимо.

Идея кодирования Церкви широко известна и просто:

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

В основном «абстрактный неопределенный» cons и nil используются вместо «обычных» конструкторы. Я считаю, что все можно закодировать таким образом (Maybe, деревья и т. Д.).

Легко показать, что List1 действительно изоморфно нормальных списков:

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

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

Таким образом, ее базовый функтор является такой же, как списки, и это должно быть возможно реализовать project для него и использовать технику из recursion-schemes.

Но я не мог, поэтому мой вопрос: «Как это сделать?». Для обычных списков, я могу просто шаблон матч:

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

Поскольку я не шаблон матч на функции могу, я должен использовать складку деконструкцию списка. Я мог бы написать складку на основе project для обычных списков:

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

Однако мне не удалось адаптировать его для церковных закодированные списков:

-- 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 имеет следующую подпись:

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

Чтобы использовать его в моих списках, мне необходимо:

1. Чтобы объявить базовый тип функтор для списка с помощью type family instance Base (ListC a) = ListF a
2. Для реализации instance Recursive (List a) where project = ...

я не на обоих этапах.

Answer 1

Обертка newtype оказалась решающим шагом, который я пропустил. Вот код вместе с образцом катаморфизма от 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