我希望能够cata
从recursion-schemes
包中使用 Church 编码中的列表。
type ListC a = forall b. (a -> b -> b) -> b -> b
为方便起见,我使用了第二等级类型,但我不在乎。如果您认为有必要,请随意添加newtype
、使用 GADT 等。
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 = ...
我在两个步骤中都失败了。