教会在Haskell中列出

Question

我必须实现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演算和教堂数字,但是这个练习对我来说是一个很大的问题,我必须能够在下周的考试中理解并解决这些问题.有人可以给我一个很好的消息来源,我可以学习如何解决这些问题,或者给我一些关于它是如何工作的指导？

Answer 1

所有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),2to (f 2)和3to (f 3).

Answer 2

所以让我们从编写两个列表构造函数开始,使用您的示例作为参考:

[] := ?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起作用,因此必须在所有列表上按预期工作.