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

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?

• "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. Nov 30 '19 at 22:13