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.λ

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.