我希望能够在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
要在我的列表中使用它,我需要:
- 使用
type family instance Base (ListC a) = ListF a
声明列表的基本函数类型。 - 实现
instance Recursive (List a) where project = ...
。
我在这两个步骤上都失败了。
newtype
以便使用),它工作得很好。 - MigMitnewtype
证明是必不可少的,而不仅仅是方便。现在代码可以正常工作了。 - nponeccop