哈斯克尔的教堂名单

Question

我必须实现 haskell 地图功能来处理教堂列表，其定义如下：

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 演算和教堂数字的经验，但是这个练习让我很头疼，我必须能够理解和解决这些问题，以便下周的考试。有人可以给我一个很好的资源，让我可以学习解决这些问题，或者给我一些关于它是如何工作的指导吗？

Answer 1

好吧，我们可以这样评论 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

如果您想解决更难的事情，请尝试为Churchlist 写tail。 （首先使用foldr为[a]写tail。）

Answer 2

所有 lambda 演算数据结构都是函数，因为这就是 lambda 演算中的全部内容。这意味着布尔、元组、列表、数字或任何东西的表示必须是表示该事物的活动行为的某个函数。

对于列表，它是一个“折叠”。不可变单链表通常定义为List a = Cons a (List a) | Nil，这意味着构建列表的唯一方法是Nil 或Cons anElement anotherList。如果你用lisp风格写出来，其中c是Cons，n是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 . f 并将每个 n 替换为 n”。

(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)，2变成(f 2)，3变成(f 3) .

Answer 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 必须在所有列表上都按预期工作。