danh sách Giáo Hội trong Haskell

Question

tôi phải thực hiện các chức năng bản đồ Haskell để làm việc với danh sách nhà thờ được định nghĩa như sau:

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

Trong phép tính lambda, danh sách được mã hóa như sau:

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

Giải pháp mẫu của bài tập này là:

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

Tôi KHÔNG biết làm thế nào giải pháp này hoạt động và tôi không ' t biết làm thế nào để tạo ra một chức năng như vậy. Tôi đã trải nghiệm với phép tính lambda và chữ số nhà thờ, nhưng bài tập này đã là một nhức đầu lớn đối với tôi và tôi phải có khả năng hiểu và giải quyết những vấn đề như vậy cho kỳ thi của tôi vào tuần tới. Ai đó có thể xin vui lòng cho tôi một nguồn tốt nơi tôi có thể học để giải quyết vấn đề như vậy hoặc cho tôi một chút hướng dẫn về cách nó hoạt động?

Answer 1

Tất cả cấu trúc dữ liệu tính toán lambda là, tốt, chức năng, bởi vì đó là tất cả những gì có trong phép tính lambda. Điều đó có nghĩa là biểu diễn cho một boolean, tuple, list, number, hoặc bất cứ thứ gì, phải là một số hàm đại diện cho hành vi hoạt động của thứ đó.

Đối với danh sách, đó là "gấp". Danh sách được liên kết đơn lẻ không thể thay đổi thường được xác định List a = Cons a (List a) | Nil, có nghĩa là cách duy nhất bạn có thể tạo danh sách là Nil hoặc Cons anElement anotherList.Nếu bạn viết nó ra trong lisp kiểu, nơi c là Cons và n là Nil, sau đó danh sách [1,2,3] trông như thế này:

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

Khi bạn thực hiện một lần trong một danh sách, bạn chỉ cần cung cấp của riêng bạn "Cons "và" Nil "để thay thế danh sách. Trong Haskell, chức năng thư viện cho điều này là foldr

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

Có vẻ quen thuộc? Lấy ra [a] và bạn có cùng loại chính xác như Churchlist a b. Như tôi đã nói, mã hóa nhà thờ đại diện cho các danh sách như chức năng gấp của chúng.

---

Ví dụ: định nghĩa map. Chú ý cách l được sử dụng như một hàm: đó là hàm lặp lại trên một số danh sách. \c n -> l (c.f) n về cơ bản nói "thay thế mọi c bằng c . f và mọi n bằng 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)) 

Nó nên được rõ ràng bây giờ mà đây thực sự là một chức năng lập bản đồ, bởi vì nó trông giống như bản gốc, ngoại trừ 1 biến thành (f 1), 2-(f 2), và 3-.

Answer 2

Vì vậy, chúng ta hãy bắt đầu bằng cách mã hóa hai nhà xây dựng danh sách, sử dụng ví dụ của bạn như tài liệu tham khảo:

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

[] là kết thúc của danh sách constructor, và chúng ta có thể nhấc rằng thẳng từ ví dụ. [] đã có ý nghĩa trong Haskell, vì vậy chúng ta hãy gọi chúng ta nil:

nil = \c n -> n 

Các constructor khác chúng ta cần có một yếu tố và một danh sách hiện có, và tạo ra một danh sách mới. Theo giáo luật, điều này được gọi là cons, với định nghĩa:

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

Chúng tôi có thể kiểm tra điều này là phù hợp với ví dụ trên, kể từ

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

Bây giờ, hãy xem xét mục đích của chức năng bản đồ - đó là để áp dụng hàm đã cho cho mỗi phần tử của danh sách. Vì vậy, hãy xem cách hoạt động cho từng nhà xây dựng.

nil không có các yếu tố, vì vậy mapChurch f nil chỉ nên nil:

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

cons có một yếu tố và một phần còn lại của danh sách, vì vậy, để cho mapChurch f làm việc propery, nó phải áp dụng f đến phần tử và mapChurch f đến phần còn lại của danh sách. Tức là, mapChurch f (cons x xs) phải giống như 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) 

Vì vậy, kể từ khi tất cả danh sách được làm từ hai nhà thầu, và mapChurch công trình trên cả hai như mong đợi, mapChurch phải làm việc như mong đợi trên tất cả các danh sách.

Answer 3

Vâng, chúng tôi có thể bình luận kiểu Churchlist cách này để làm rõ điều này:

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

Lưu ý rằng đây là liên quan mật thiết đến foldr chức năng:

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

foldr là một chức năng rất chung chung rằng có thể thực hiện tất cả các loại chức năng danh sách khác. Một ví dụ nhỏ sẽ giúp bạn đang thực hiện một bản sao danh sách với foldr:

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

Sử dụng kiểu nhận xét trên, foldr (:) [] nghĩa này: "nếu bạn thấy một danh sách trống trả lại danh sách trống, và nếu bạn nhìn thấy một cặp trả lại head:tailResult. "

Sử dụng Churchlist, bạn có thể dễ dàng ghi các đối tác theo cách này:

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

Bây giờ, để thực hiện map, bạn chỉ cần thay thế cons với một chức năng phù hợp, như thế này:

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

Ánh xạ giống như sao chép một danh sách, ngoại trừ việc thay vì chỉ sao chép các phần tử nguyên văn bạn áp dụng f cho mỗi danh sách.

Nghiên cứu kỹ lưỡng điều này và bạn có thể tự viết mapChurchlist :: (t -> t') -> Churchlist t u -> Churchlist t' u.

tập thể dục tắm (dễ): viết các chức năng danh sách về foldr, và viết các đối tác cho 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 

Nếu bạn đang cảm thấy như giải quyết vấn đề khó hơn, hãy thử viết tail cho Churchlist. (Bắt đầu bằng cách viết tail cho [a] sử dụng foldr.)