What is the difference between the Mogensen-Scott and the Boehm-Berarducci encoding for ADTs on the Lambda Calculus?

Question

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?

Answer 1

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.