I had to implement the haskell map function to work with church lists which are defined as following:
type Churchlist t u = (t->u->u)->u->u
In lambda calculus, lists are encoded as following:
[] := λc. λn. n
[1,2,3] := λc. λn. c 1 (c 2 (c 3 n))
The sample solution of this exercise is:
mapChurch :: (t->s) -> (Churchlist t u) -> (Churchlist s u)
mapChurch f l = \c n -> l (c.f) n
I have NO idea how this solution works and I don't know how to create such a function. I have already experience with lambda calculus and church numerals, but this exercise has been a big headache for me and I have to be able to understand and solve such problems for my exam next week. Could someone please give me a good source where I could learn to solve such problems or give me a little guidance on how it works?
All lambda calculus data structures are, well, functions, because that's all there is in the lambda calculus. That means that the representation for a boolean, tuple, list, number, or anything, has to be some function that represents the active behavior of that thing.
For lists, it is a "fold". Immutable singly-linked lists are usually defined List a = Cons a (List a) | Nil
, meaning the only ways you can construct a list is either Nil
or Cons anElement anotherList
. If you write it out in lisp-style, where c
is Cons
and n
is Nil
, then the list [1,2,3]
looks like this:
(c 1 (c 2 (c 3 n)))
When you perform a fold over a list, you simply provide your own "Cons
" and "Nil
" to replace the list ones. In Haskell, the library function for this is foldr
foldr :: (a -> b -> b) -> b -> [a] -> b
Look familiar? Take out the [a]
and you have the exact same type as Churchlist a b
. Like I said, church encoding represents lists as their folding function.
So the example defines map
. Notice how l
is used as a function: it is the function that folds over some list, after all. \c n -> l (c.f) n
basically says "replace every c
with c . f
and every n
with 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))
It should be apparent now that this is indeed a mapping function, because it looks just like the original, except 1
turned into (f 1)
, 2
to (f 2)
, and 3
to (f 3)
.