教会在Haskell列出 [英] Church lists in Haskell

问题描述

我必须实现haskell map函数才能使用教会列表，它的定义如下：

  type Churchlist tu = （t-> u-> u） - > u-> u 
  

在lambda微积分，列表编码如下：

  []：=λc。 λN。 n 
 [1,2,3]：=λc。 λN。 c 1（c 2（c 3 n））
  

本练习的示例解决方案是： p>

  mapChurch ::（t-> s） - > （Churchlist t u） - > （Churchlist s u）
 mapChurch f l = \c n  - > l（cf）n 
  

我不知道这个解决方案如何工作，我不知道如何创建这样一个功能。我已经有了lambda微积分和教会数字的经验，但这个练习一直是我头痛的问题，我必须能够在下周的考试中理解和解决这些问题。有人可以给我一个很好的资源，我可以学习解决这些问题，或者给我一些指导它如何工作？ 解决方案

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

对于列表，这是一个折叠。不可变的单链表通常定义为 List a = Cons a（List a）| Nil ，这意味着你可以构造一个列表的唯一方法是 Nil 或 Cons anElement anotherList 。如果你用lisp风格写出来，其中 c 是 Cons 和 n 是 Nil ，那么列表 [1,2,3] 看起来像这样： p>



 （c 1（c 2（c 3 n）））
  

当您对列表执行折叠时，只需提供自己的缺点和 Nil 来替换列表中的内容。在Haskell中，这个库函数是 foldr

  foldr :: （a  - > b  - > b） - > b  - > [a]  - > b 
  

看起来很熟悉吗？取出 [a] ，您的类型与 Churchlist a b 完全相同。就像我说的，教会编码代表列表作为他们的折叠功能。

---

所以这个例子定义了 map 。请注意， l 是如何用作函数的：毕竟，它是折叠在某个列表上的函数。 \c n - > l（cf）n 基本上是说用 c。f 和每一个替换每一个 c n 与 n 。

 （c 1（c 2（c 3 n）））
  - 用`（c。f）`替换`c`，用`n`替换`n` 
 （c。f）1（（c。f）2）（（c。f）3 n）））
  - 简化'（foo.bar）baz`到`foo（bar baz）`
（c（f 1）（c（f 2）（c（f 3）n））
  

<现在应该很明显这确实是一个映射函数，因为它看起来就像原始文件，除了 1 变成了（f 1） ， 2 至（f 2）， 3 至（f 3）。

I had to implement the haskell map function to work with church lists which are defined as following:

type Churchlist t u = (t->u->u)->u->u

In lambda calculus, lists are encoded as following:

[] := λc. λn. n
[1,2,3] := λc. λn. c 1 (c 2 (c 3 n))

The sample solution of this exercise is:

mapChurch :: (t->s) -> (Churchlist t u) -> (Churchlist s u)
mapChurch f l = \c n -> l (c.f) n

I have NO idea how this solution works and I don't know how to create such a function. I have already experience with lambda calculus and church numerals, but this exercise has been a big headache for me and I have to be able to understand and solve such problems for my exam next week. Could someone please give me a good source where I could learn to solve such problems or give me a little guidance on how it works?

解决方案

All lambda calculus data structures are, well, functions, because that's all there is in the lambda calculus. That means that the representation for a boolean, tuple, list, number, or anything, has to be some function that represents the active behavior of that thing.

For lists, it is a "fold". Immutable singly-linked lists are usually defined List a = Cons a (List a) | Nil, meaning the only ways you can construct a list is either Nil or Cons anElement anotherList. If you write it out in lisp-style, where c is Cons and n is Nil, then the list [1,2,3] looks like this:

(c 1 (c 2 (c 3 n)))

When you perform a fold over a list, you simply provide your own "Cons" and "Nil" to replace the list ones. In Haskell, the library function for this is foldr

foldr :: (a -> b -> b) -> b -> [a] -> b

Look familiar? Take out the [a] and you have the exact same type as Churchlist a b. Like I said, church encoding represents lists as their folding function.

---

So the example defines map. Notice how l is used as a function: it is the function that folds over some list, after all. \c n -> l (c.f) n basically says "replace every c with c . f and every n with 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))

It should be apparent now that this is indeed a mapping function, because it looks just like the original, except 1 turned into (f 1), 2 to (f 2), and 3 to (f 3).

这篇关于教会在Haskell列出的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！