[Gajurgensen]

Learning about Church and Scott encoding was much more interesting than I thought it would be. I was expecting it to be tedious and banal, but I came out of it feeling like I had some sort of revelation. Imagining naturals, lists, trees, etc. as function application was mind-bending at first, but it eventually clicks into place. Lambda calculus is so incredible in its combination of simple semantics, expressiveness, and abstraction/compositionality.

To go a step further, think about how you would implement a predecessor function on the Church encoding of the naturals. It is much more complicated than one might expect, and perfectly motivates the introduction of Scott encodings and the fixed-point function.

[chewxy]

Scott encoding even has a weirder implications (if you're not used to it) if you think about it

    0 ≡ λf.λx.x
    1 ≡ λf.λx.x (λf.λx.x)
    2 ≡ λf.λx.x (λf.λx.x (λf.λx.x))

Or if you allow meta variables in your expression:

    0 ≡ λf.λx.x
    1 ≡ λf.λx.x 0
    2 ≡ λf.λx.x 1

This implies 2 contains 1, 1 contains 0. Bam. Scott encoding also encodes some parts of set theory.

Following from this, of course, all ADTs can be encoded following the Scott encoding scheme.