Операции на церковных списков в Haskell

Question

Я имею в виду this 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 s и произвел 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).

Что представляет собой следующий шаг? Ну, это зависит. Is 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 

Это вызывает некоторые вопросы.

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

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