listy Kościół w Haskell

Question

miałem do realizacji funkcji Haskell mapa pracować z listami kościelnych, które są zdefiniowane w następujący sposób:

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

W rachunku lambda, listy są kodowane w następujący sposób:

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

Przykładowe rozwiązanie tego ćwiczenia to:

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

Nie mam pojęcia, jak to rozwiązanie działa, a ja nie ". t wiedzieć, jak stworzyć taką funkcję. Mam już doświadczenie z rachunkiem lambda i liczebnikami kościelnymi, ale to ćwiczenie było dla mnie dużym bólem głowy i muszę być w stanie zrozumieć i rozwiązać takie problemy na moim egzaminie w przyszłym tygodniu. Czy ktoś mógłby podać mi dobre źródło, w którym mógłbym nauczyć się rozwiązywać takie problemy lub udzielać mi wskazówek, jak to działa?

Answer 1

Wszystkie struktury danych rachunku lambda to, cóż, funkcje, ponieważ to wszystko jest w rachunku lambda. Oznacza to, że reprezentacja wartości boolowskiej, krotki, listy, liczby lub cokolwiek innego musi być jakąś funkcją reprezentującą aktywne zachowanie tej rzeczy.

W przypadku list jest to "fałd". Listy niezmienne pojedynczo są zwykle zdefiniowane jako List a = Cons a (List a) | Nil, co oznacza, że ​​jedynymi sposobami na skonstruowanie listy są: Nil lub Cons anElement anotherList.Jeśli piszesz go w lisp stylu, gdzie c jest Cons i n jest Nil, lista [1,2,3] wygląda następująco:

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

Podczas wykonywania fałdę na liście, wystarczy podać swój własny "Cons "i" Nil ", aby zastąpić listy. W Haskell, funkcja biblioteki to foldr

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

wygląda znajomo? Wyjmij [a] i masz dokładnie ten sam typ co Churchlist a b. Tak jak powiedziałem, kodowanie kościelne przedstawia listy jako funkcję składania.

---

Przykład ten definiuje map. Zauważ, że funkcja l jest używana jako funkcja: jest funkcją, która przecina pewną listę. \c n -> l (c.f) n mówi "wymień co c z c . f i co n z 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)) 

To powinno być oczywiste, że teraz jest to rzeczywiście funkcja mapowania, ponieważ wygląda jak oryginał, z wyjątkiem 1 przekształcony (f 1), 2 do (f 2) i 3 do .

Answer 2

Więc zacznijmy od kodujące dwie lista konstruktorów, wykorzystując swój przykład jako odniesienie:

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

[] jest koniec listy konstruktora, a my możemy podnieść, że prosto z przykładu. [] już ma sens w Haskell, więc nazwijmy nasz nil:

nil = \c n -> n 

Drugi konstruktor musimy bierze element i istniejącej listy, a tworzy nową listę. Kanonicznie, nazywa się to cons, z definicją:

cons x xs = \c n -> c x (xs c n) 

Możemy sprawdzić, czy jest to zgodne z powyższym przykładzie, ponieważ

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

Teraz rozważyć przeznaczenie funkcji mapy - to zastosować daną funkcję do każdego elementu listy. Zobaczmy więc, jak to działa dla każdego z konstruktorów.

nil ma żadnych elementów, więc mapChurch f nil powinny być tylko nil:

mapChurch f nil 
= \c n -> nil (c.f) n 
= \c n -> (\c' n' -> n') (c.f) n 
= \c n -> n 
= nil 

cons ma element i resztę listy, tak, aby na mapChurch f pracować propery, musi stosować f do elementu i mapChurch f do reszty listy. Oznacza to, że mapChurch f (cons x xs) powinien być taki sam jak 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) 

Więc skoro wszystkie listy są wykonane z tych dwóch konstruktorów i mapChurch prace na obu z nich zgodnie z oczekiwaniami, mapChurch musi działać zgodnie z oczekiwaniami na wszystkich listach.

Answer 3

Cóż, możemy komentować typu Churchlist w ten sposób, aby je wyjaśnić:

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

pamiętać, że jest ściśle związany z foldr funkcję:

foldr :: (t -> u -> u) -> u -> [t] -> u 
foldr k z [] = z 
foldr k z (x:xs) = k x (foldr k z xs) 

foldr jest bardzo ogólna funkcja może implementować wszystkie rodzaje innych funkcji list. Trywialny przykład, który pomoże Ci realizuje liście kopiowania z foldr:

copyList :: [t] -> [t] 
copyList xs = foldr (:) [] xs 

Używanie skomentował typ powyżej, foldr (:) [] oznacza to: „jeśli widzisz pustą listą zwróci pustą listę, a jeśli widzisz parę return head:tailResult. "

Korzystanie Churchlist, można łatwo napisać odpowiednik w ten sposób:

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

Teraz, aby wdrożyć map, wystarczy zastąpić cons z odpowiedniej funkcji, takich jak to:

map :: (a -> b) -> [a] -> [b] 
map f xs = foldr (\x xs' -> f x:xs') [] xs 

Mapowanie jest jak kopiowanie listy, z tą różnicą, że zamiast tylko kopiować elementy w dosłownym brzmieniu, dla każdej z nich stosuje się f.

Przestudiuj dokładnie to i powinieneś być w stanie samodzielnie napisać mapChurchlist :: (t -> t') -> Churchlist t u -> Churchlist t' u.

Dodatkowe ćwiczenia (łatwe): napisz list tych funkcji pod względem foldr i napisać odpowiedniki dla 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 

Jeśli czujesz jak przeciwdziałanie coś mocniej, spróbować napisać tail dla Churchlist. (Start pisząc tail dla [a] użyciu foldr.)