Haskell Church List Operations

Question

I mean this question

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

In lambda calculus, lists are encoded as follows:

 [] := λc. λn. n [1,2,3] := λc. λn. c 1 (c 2 (c 3 n)) mapChurch :: (t->s) -> (Churchlist tu) -> (Churchlist su) mapChurch fl = \cn -> l (cf) n 

I’m thinking about what other list functions I could implement in Churchlists and have successfully written a conc2 function that combines 2 church lists

 conc2Church l1 l2 cn = l1 c (l2 cn) 

I also tried zipWithChurch, which works like zipWith on regular lists. But I can not find a solution. Can anybody help me?

Answer 1

Do you want to use real tuples or church tuples? I'll take the first one.

So, start with the type signature you need. You want him to accept 2 different Churchlist and produce Churchlist tuples.

 churchZip :: Churchlist au -> Churchlist bu -> Churchlist (a,b) u 

Now, how would you implement this? Recall that Churchlist is represented by a function that develops above them. Therefore, if our result is equal to Churchlist (a,b) u , we want it to have the form of a function of the type ((a,b) -> u -> u) -> u -> u (this is, after all, equivalent a synonym of type Churchlist (a,b) u ).

 churchZip l1 l2 cn = ??? 

What is the next step? Well, it depends. Is l1 empty? What about l2 ? If any of them, then you want the result to be an empty list. Otherwise, you want to combine the first elements from each list, and then churchZip the rest.

 churchZip l1 l2 cn | isEmpty l1 || isEmpty l2 = n | otherwise = c (churchHead l1, churchHead l2) (churchZip (churchTail l1) (churchTail l2) cn 

This raises some questions.

• Are you allowed to write this function recursively? In a pure lambda calculus, you have to write recursive functions with the fixpoint operator (aka y combinator).
• Do you have churchHead , churchTail and isEmpty ? Are you ready to write them? Can you write them?
• Is there a better way to structure this feature? Everything can be done with the help of a fold (remember that l1 and l2 are actually a function of bending over themselves), but is this a pure solution to this problem?

Achieving this goal is purely mechanical, taking a solid understanding of church coding lists. I will leave you deep thought, as this is homework.