猫摄像机用于教堂编码列表

Question

我希望能够在Church编码的列表中使用recursion-schemes包中的cata。

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

我将用第二级类型来方便翻译，但这对我并不重要。如果您认为有必要，可以自由添加 newtype 、使用GADTs等。

Church编码的思想被广泛地理解和简单易懂：

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

然而，我未能将其适用于 Church 编码的列表：

-- 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 = ...。

我在这两个步骤上都失败了。

- nponeccop

---

你失败了吗？我已经尝试过这个方法（添加newtype以便使用），它工作得很好。 - MigMit

我更新了我的问题。 - nponeccop

newtype证明是必不可少的，而不仅仅是方便。现在代码可以正常工作了。 - nponeccop

事实上，任何代数数据类型都具有教堂编码。 - PyRulez

是的。我甚至尝试过对基本函子进行 Church 编码：http://nponeccop.livejournal.com/454146.html - nponeccop

Answer 1

我错过的关键步骤是使用 newtype 包装器。以下是代码示例，包括来自 recursion-schemes 的样本 catamorphism。

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

- nponeccop