我必须实现 haskell map 函数来处理教堂列表，这些列表定义如下：
type Churchlist t u = (t->u->u)->u->u
在 lambda 演算中，列表编码如下：
[] := λc. λn. n
[1,2,3] := λc. λn. c 1 (c 2 (c 3 n))
本练习的示例解决方案是：
mapChurch :: (t->s) -> (Churchlist t u) -> (Churchlist s u)
mapChurch f l = \c n -> l (c.f) n
我不知道这个解决方案是如何工作的，也不知道如何创建这样的功能。我已经有 lambda 演算和教堂数字的经验，但是这个练习让我很头疼，我必须能够理解和解决这些问题，以便下周的考试。有人可以给我一个很好的资源，让我可以学习解决这些问题，或者给我一些关于它如何工作的指导吗？
所有 lambda 演算数据结构都是函数，因为这就是 lambda 演算中的全部内容。这意味着布尔、元组、列表、数字或任何东西的表示必须是表示该事物的活动行为的某个函数。
对于列表，它是一个“折叠”。不可变单链表通常定义List a = Cons a (List a) | Nil为 ，这意味着您可以构造列表的唯一方法是Nilor Cons anElement anotherList。如果你用 lisp 风格写出来， where cisCons和nis Nil，那么列表[1,2,3]如下所示：
(c 1 (c 2 (c 3 n)))
当您在列表上执行折叠时，您只需提供自己的“ Cons”和“ Nil”来替换列表中的那些。在 Haskell 中，为此的库函数是foldr
foldr :: (a -> b -> b) -> b -> [a] -> b
看起来熟悉？取出[a]，您将拥有与 完全相同的类型Churchlist a b。就像我说的，教堂编码将列表表示为它们的折叠功能。
所以这个例子定义了map. 注意它是如何l用作函数的：毕竟，它是折叠某个列表的函数。\c n -> l (c.f) n基本上说“将每个替换c为” 。c . fnn
(c 1 (c 2 (c 3 n)))
-- replace `c` with `(c . f)`, and `n` with `n`
((c . f) 1 ((c . f) 2) ((c . f) 3 n)))
-- simplify `(foo . bar) baz` to `foo (bar baz)`
(c (f 1) (c (f 2) (c (f 3) n))
现在应该很明显，这确实是一个映射函数，因为它看起来就像原来的一样，除了1变成(f 1)、2to(f 2)和3to (f 3)。
因此，让我们从编码两个列表构造函数开始，使用您的示例作为参考：
[] := λc. λn. n
[1,2,3] := λc. λn. c 1 (c 2 (c 3 n))
[]是列表构造函数的结尾，我们可以直接从示例中提升它。 []在 haskell 中已经有意义，所以让我们调用我们的nil：
nil = \c n -> n
我们需要的另一个构造函数接受一个元素和一个现有列表，并创建一个新列表。典型地，这被称为cons，其定义为：
cons x xs = \c n -> c x (xs c n)
我们可以检查这是否与上面的示例一致，因为
cons 1 (cons 2 (cons 3 nil))) =
cons 1 (cons 2 (cons 3 (\c n -> n)) =
cons 1 (cons 2 (\c n -> c 3 ((\c' n' -> n') c n))) =
cons 1 (cons 2 (\c n -> c 3 n)) =
cons 1 (\c n -> c 2 ((\c' n' -> c' 3 n') c n) ) =
cons 1 (\c n -> c 2 (c 3 n)) =
\c n -> c 1 ((\c' n' -> c' 2 (c' 3 n')) c n) =
\c n -> c 1 (c 2 (c 3 n)) =
现在，考虑 map 函数的目的——它将给定的函数应用于列表的每个元素。那么让我们看看每个构造函数是如何工作的。
nil没有元素，所以mapChurch f nil应该是nil：
mapChurch f nil
= \c n -> nil (c.f) n
= \c n -> (\c' n' -> n') (c.f) n
= \c n -> n
= nil
cons有一个元素和列表的其余部分，因此，为了mapChurch f正常工作，它必须应用于f元素和mapChurch f列表的其余部分。也就是说，mapChurch f (cons x xs)应该与 相同cons (f x) (mapChurch f xs)。
mapChurch f (cons x xs)
= \c n -> (cons x xs) (c.f) n
= \c n -> (\c' n' -> c' x (xs c' n')) (c.f) n
= \c n -> (c.f) x (xs (c.f) n)
-- (c.f) x = c (f x) by definition of (.)
= \c n -> c (f x) (xs (c.f) n)
= \c n -> c (f x) ((\c' n' -> xs (c'.f) n') c n)
= \c n -> c (f x) ((mapChurch f xs) c n)
= cons (f x) (mapChurch f xs)
因此，由于所有列表都是由这两个构造函数组成的，并且mapChurch按预期在它们上mapChurch工作，因此必须在所有列表上按预期工作。
好吧，我们可以这样评论 Churchlist 类型来澄清它：
-- Tell me...
type Churchlist t u = (t -> u -> u) -- ...how to handle a pair
-> u -- ...and how to handle an empty list
-> u -- ...and then I'll transform a list into
-- the type you want
请注意，这与foldr函数密切相关：
foldr :: (t -> u -> u) -> u -> [t] -> u
foldr k z [] = z
foldr k z (x:xs) = k x (foldr k z xs)
foldr是一个非常通用的函数，可以实现各种其他列表函数。一个可以帮助您实现列表副本的简单示例foldr：
copyList :: [t] -> [t]
copyList xs = foldr (:) [] xs
使用上面的注释类型foldr (:) []意味着：“如果你看到一个空列表返回空列表，如果你看到一对返回head:tailResult。”
使用Churchlist，您可以通过这种方式轻松编写对应项：
-- Note that the definitions of nil and cons mirror the two foldr equations!
nil :: Churchlist t u
nil = \k z -> z
cons :: t -> Churchlist t u -> Churchlist t u
cons x xs = \k z -> k x (xs k z)
copyChurchlist :: ChurchList t u -> Churchlist t u
copyChurchlist xs = xs cons nil
现在，要实现map，您只需要替换cons为合适的函数，如下所示：
map :: (a -> b) -> [a] -> [b]
map f xs = foldr (\x xs' -> f x:xs') [] xs
映射就像复制一个列表，只不过不是逐字复制你应用f到每个元素上的元素。
仔细研究所有这些，你应该能够自己写mapChurchlist :: (t -> t') -> Churchlist t u -> Churchlist t' u。
额外练习（简单）：根据 编写这些列表函数foldr，并为 编写对应项Churchlist：
filter :: (a -> Bool) -> [a] -> [a]
append :: [a] -> [a] -> [a]
-- Return first element of list that satisfies predicate, or Nothing
find :: (a -> Bool) -> [a] -> Maybe a
如果您想解决更难的事情，请尝试tail为Churchlist. （从写使用tail开始。）[a]foldr