Церковные списки в Haskell

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 

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

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

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

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

-- 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 (:) [] означает следующее: «если вы видите пустой список возвращает пустой список, и если вы видите пару return 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.)