Differences between Church and Scott encoding
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 -&gt; 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).