Evening All

I already have a "grasp" of haskell (not terrible, about 6 month experience) and am trying to learn the fundamentals that sit behind it, thus am now turning my attention to trying to learn Lambda Calculus. I thought, perhaps mistakenly, that it might be a good idea to try to work out the λ -terms that corresponds to some functions in Haskell. I am trying the foldr and map functions.

soooo foldr should have the property

              foldr f u [N1, . . . , Nk] →f N1 (f N2 (. . . (f Nk u)))

and map would have (should imagine...)

              map f [N1, . . . , Nk] → [f N1, f N2, . . . , f Nk]

where → represents reduction by any number of β -steps....

But am struggling to flesh this out to be honest. Any help would be greatly appreciated...

Kind Regards.


1 Answer 1


You are looking for Church encodings of datastructures in $\lambda$-calculus, and in particular of lists.

  • $\begingroup$ Thankyou Andrej, indeed there seem to be a good few papers out there on the subject, for example "Programming in the λ-Calculus: From Church to Scott and Back" by Jan Martin Jansen. Do you (or anyone) have any specific recommendations to help me get to the solutions more efficiently, granted, some nice reading to be had out there... $\endgroup$
    – user130129
    Dec 29, 2020 at 7:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.