Списки церквей в Хаскеле

Question

Мне пришлось реализовать функцию карты haskell для работы со списками церквей, которые определены следующим образом:

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

Я понятия не имею, как работает это решение, и я не знаю, как создать такую ​​функцию. Я уже имел опыт работы с лямбда-исчислением и церковными цифрами, но это упражнение стало для меня большой головной болью, и я должен быть в состоянии понять и решить такие проблемы для моего экзамена на следующей неделе. Может кто-нибудь дать мне хороший источник, где я мог бы научиться решать такие проблемы, или дать небольшое руководство о том, как это работает?

Answer 1

Все структуры данных лямбда-исчисления - это, в общем-то, функции, потому что это все, что есть в лямбда-исчислении.Это означает, что представление для логического значения, кортежа, списка, числа или чего-либо должно быть некоторой функцией, которая представляет активное поведение этой вещи.

Для списков это «сворачивание».Неизменяемые односвязные списки обычно определяются 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 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)) =

Теперь рассмотрим назначение функции карты - это применить данную функцию к каждому элементу списка. Итак, давайте посмотрим, как это работает для каждого из конструкторов.

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 должен работать должным образом во всех списках.

Answer 3

Ну, мы можем прокомментировать тип церковного списка таким образом, чтобы уточнить это:

-- 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

Если вам хочется заняться чем-то сложнее, попробуйте написать tail для Churchlist. (Начните с записи tail для [a], используя foldr.)