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

Я хочу иметь возможность использовать 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 = ...

Я терплю неудачу на обоих шагах.


recursion haskell recursion-schemes church-encoding catamorphism
person nponeccop    schedule 16.07.2015    source источник
comment
В чем твоя неудача? Я пробовал это (добавляя newtype для удобства), и он отлично работает.   -  person MigMit    schedule 17.07.2015
comment
я обновил свой вопрос   -  person nponeccop    schedule 17.07.2015
comment
newtype оказалось необходимым, а не просто удобством. Код работает сейчас.   -  person nponeccop    schedule 17.07.2015
comment
На самом деле верно, что любой алгебраический тип данных имеет церковное кодирование.   -  person PyRulez    schedule 29.08.2015
comment
Ага. Я даже пытался закодировать в Черче базовый функтор: nponeccop.livejournal.com/454146.html   -  person nponeccop    schedule 16.09.2015

Ответы (1)


arrow_upward
4
arrow_downward

Обертка 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
person nponeccop    schedule 16.07.2015