Списки церквей в Haskell

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

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

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

26
задан Bill the Lizard 16 September 2012 в 22:29
поделиться