Differences between Church and Scott encoding

I'm kind of new to lambda calculus and I found this Wikipedia article
https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding

The section Comparison to the Church encoding presents a short comparison between Church and Scott encoding

Church

λx1...xAi.λc1...cN.ci (x1c1...cN)...(xAic1...cN)

Scott

λx1...xAi.λc1...cN.ci x1...xAi

Do you agree with the Church generic encoding description? The page specified that citation is needed for that description.

It's correct as long as all the arguments $x_1 ... x_{A_i}$ are recursive occurrences of the same structure. Otherwise there's no way to say what the Church encoding should be without more information.

That is the major difference between the Church and Scott encodings. If we think in terms of types, then for a fixed point type:

$T \cong F T$

the Church encoding of $T$ has a type like:

$(F r \to r) \to r$

while the Scott encoding has a type like:

$(F T \to r) \to r$

So, Scott encodings generally require some other source of recursion/iteration, both at the value level, because it only gives you access to one level of unfolding at a time, and at the type level (if you have one), because the fixed point type $T$ is still present in the type of the Scott encoding.

However, this means that Scott encodings are much better than Church encodings for some things. For instance, it's obvious how to write the (clamped) predecessor for Scott encoded naturals $\mathbb{N} = \forall r. r \to (\mathbb{N} \to r) \to r$:

pred n = n 0 (\pn -> pn)

However, for the Church encoded naturals:

$\mathbb{N} = \forall r. r \to (r \to r) \to r$

writing the predecessor function is a challenging exercise (and the resulting function is expensive).

StackExchange Computer Science Q#97031, answer score: 3