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?
Well, we can comment the Churchlist type this way to clarify it:
Note that this is intimately related to the
foldr
function:foldr
is a very general function that can implement all sorts of other list functions. A trivial example that will help you is implementing a list copy withfoldr
:Using the commented type above,
foldr (:) []
means this: "if you see an empty list return the empty list, and if you see a pair returnhead:tailResult
."Using
Churchlist
, you can easily write the counterpart this way:Now, to implement
map
, you just need to replacecons
with a suitable function, like this:Mapping is like copying a list, except that instead of just copying the elements verbatim you apply
f
to each of them.Study all of this carefully, and you should be able to write
mapChurchlist :: (t -> t') -> Churchlist t u -> Churchlist t' u
on your own.Extra exercise (easy): write these list functions in terms of
foldr
, and write counterparts forChurchlist
:If you're feeling like tackling something harder, try writing
tail
forChurchlist
. (Start by writingtail
for[a]
usingfoldr
.)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 eitherNil
orCons anElement anotherList
. If you write it out in lisp-style, wherec
isCons
andn
isNil
, then the list[1,2,3]
looks like this: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 isfoldr
Look familiar? Take out the
[a]
and you have the exact same type asChurchlist a b
. Like I said, church encoding represents lists as their folding function.So the example defines
map
. Notice howl
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 everyc
withc . f
and everyn
withn
".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)
, and3
to(f 3)
.So let's start by encoding the two list constructors, using your example as reference:
[]
is the end of list constructor, and we can lift that straight from the example.[]
already has meaning in haskell, so let's call oursnil
:The other constructor we need takes an element and an existing list, and creates a new list. Canonically, this is called
cons
, with the definition:We can check that this is consistent with the example above, since
Now, consider the purpose of the map function - it is to apply the given function to each element of the list. So let's see how that works for each of the constructors.
nil
has no elements, somapChurch f nil
should just benil
:cons
has an element and a rest of list, so, in order formapChurch f
to work propery, it must applyf
to the element andmapChurch f
to rest of the list. That is,mapChurch f (cons x xs)
should be the same ascons (f x) (mapChurch f xs)
.So since all lists are made from those two constructors, and
mapChurch
works on both of them as expected,mapChurch
must work as expected on all lists.