Операции над церковными списками в Хаскеле

Question

Я имею в виду этот вопрос

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

В лямбда-исчислении списки кодируются следующим образом:

[] := λ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

Я думаю о том, какие другие функции списка я мог бы реализовать в церковных списках и успешно написал функцию conc2, которая объединяет 2 церковных списка

conc2Church l1 l2 c n = l1 c (l2 c n)

Я также попробовал zipWithChurch, который работает как zipWith в обычных списках. Но я не могу найти решение. Может кто-нибудь мне помочь?

Answer 1

Вы хотите использовать настоящие кортежи или церковные кортежи? Я возьму первое.

Итак, начнем с нужной подписи типа. Вы хотите взять в 2 разных Churchlist и производят Churchlist кортежей.

churchZip :: Churchlist a u -> Churchlist b u -> Churchlist (a,b) u

Как бы вы это реализовали? Напомним, что Churchlist s представлены функцией, которая складывается над ними. Так что, если наш результат Churchlist (a,b) u мы хотим, чтобы он имел вид функции типа ((a,b) -> u -> u) -> u -> u (в конце концов, это эквивалент синонима типа Churchlist (a,b) u).

churchZip l1 l2 c n = ???

Каким будет следующий шаг? Ну, это зависит. Является l1 пусто? Как насчет l2? Если любой из них, то вы хотите, чтобы результат был пустым списком. В противном случае вы хотите создать пару первых элементов из каждого списка, а затем churchZip остальные.

churchZip l1 l2 c n
  | isEmpty l1 || isEmpty l2 = n
  | otherwise                = c (churchHead l1, churchHead l2)
                                 (churchZip (churchTail l1) (churchTail l2) c n

Это поднимает некоторые вопросы.

• Вам разрешено писать эту функцию рекурсивно? В чистом лямбда-исчислении вы должны написать рекурсивные функции с оператором точки фиксирования (он же комбинатор у).
• У тебя есть churchHead, churchTail, а также isEmpty имеется в наличии? Вы готовы их написать? Вы можете написать их?
• Есть ли лучший способ структурировать эту функцию? Все можно сделать со сгибом (помните, l1 а также l2 на самом деле это функция складывания над собой), но является ли это чистым решением этой проблемы?

Достижение этой точки является чисто механическим, если мы хорошо понимаем церковное кодирование списков. Я оставлю вам глубокие размышления, так как это домашняя работа.