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

このソリューションがどのように機能するのかわかりませんし、そのような関数を作成する方法もわかりません。私はすでにラムダ計算と教会数の経験がありますが、この演習は私にとって大きな頭痛の種であり、来週の試験のためにそのような問題を理解して解決できなければなりません. そのような問題を解決する方法を学ぶことができる良い情報源を教えてください。または、それがどのように機能するかについて少しガイダンスを教えてください

Answer 1

すべてのラムダ計算のデータ構造は、まあ、関数です。ラムダ計算にはそれしかないからです。つまり、ブール値、タプル、リスト、数値などの表現は、そのもののアクティブな動作を表す関数でなければなりません。

リストの場合、それは「折りたたみ」です。不変の単一リンクリストは通常​​定義されています。List a = Cons a (List a) | Nilつまり、リストを作成できる唯一の方法は または のいずれNilかCons anElement anotherListです。cisConsとnisを Lisp スタイルで書き出すと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ものに置き換える」と言います。cc . fnn

(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

それでは、例を参照として使用して、2 つのリスト コンストラクターをエンコードすることから始めましょう。

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

[]はリストコンストラクターの終わりであり、例から直接持ち上げることができます。 []haskell ではすでに意味があるので、 ours と呼びましょうnil:

nil = \c n -> n

必要なもう 1 つのコンストラクターは、要素と既存のリストを受け取り、新しいリストを作成します。標準的には、これは と呼ばれ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)) =

ここで、map 関数の目的を考えてみましょう。指定された関数をリストの各要素に適用することです。それでは、各コンストラクターでそれがどのように機能するかを見てみましょう。

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適用する必要があります。つまり、 と同じである必要があります。fmapChurch fmapChurch 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)

したがって、すべてのリストはこれら 2 つのコンストラクターから作成され、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 (:) []「空のリストが表示された場合は空のリストが返され、ペアが表示された場合は が返される」という意味になります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