On the Lambda Calculus, there are several different ways to represent a list. For example, one can encode it as its right fold:

list = (λ (cons nil) (cons 1 (cons 2 (cons 3 nil))))

One can, instead, use pair, false, fst and snd as aliases to cons, nil, head and tail. This way, you will have this:

list = (λ (a) (a 1 (λ (b) (b 2 (λ (c) (c 3 0))))))

Another way is to use the Mogensen-Scott encoding, which represents a list as the case statement required to deconstruct it:

list = (λ (c n) (c 1 (λ (c n) (c 2 (λ (c n) (c 3 (λ (c n) n)))))))

But there is also another way, called Boehm-Berarducci encoding, which I didn't understand. Supposedly, it allows the same thing that the Scott allows: systematically representing ADTs with lambda terms. So, what is the difference?

  • $\begingroup$ "Boehm-Berarducci encoding" is another way to tell "right fold". For list it's list = (λ (c n) (c 1 (c 2 (c 3 n)))), i.e. your first example. $\endgroup$ Nov 30 '19 at 22:13

The Boehm–Berarducci encoding is often mistakenly referred to as the "Church" encoding. They both start from the same general idea (encode data types by their iterator/catamorphism), but differ in subtle ways. In particular, the Church encoding only represents data types in the untyped setting, only covers introduction, and is not tight; whereas, the Boehm–Berarducci encoding works in System F, covers both introduction and elimination, and proves that the encoding is tight.

For an extensive discussion of the differences, see this post by Oleg Kiselyov.

  • 5
    $\begingroup$ What is meant by "tight"? $\endgroup$ Jul 6 '16 at 11:05
  • $\begingroup$ By "tight" was probably meant that principal type of an encoded expression is enough, and there is no need to restrict it more. $\endgroup$ Nov 30 '19 at 22:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.