just Scott encoding, Scott-Mogensen refers to a meta encoding of LC in LC. Scott's encoding is fine but requires fixpoint recursion for many operations as you said.
Interestingly though, Mogensen's ternary encoding [1] does not require fixpoint recursion and is the most efficient (wrt being compact) encoding in LC known right now.
> Just use [..], seriously
do you have any further arguments for Scott's encoding? There are many number encodings with constant time predecessor, and with any number requiring O(n) space and `add` being this complex, it becomes quite hard to like
First, if we're talking about practicality, and not just theoretical considerations, then the numbers should not be stored as Peano integers a.k.a. base 1 in the first place. Use lists of 8-tuples of bools or native machine integers or whatever, otherwise, you will suffer from O(n) complexities somewhere in your arithmetic, that's just how base 1 works. Fretting over which particular basic operation has to house this linear-over-logarithmic overhead is IMO unproductive: use better data structures instead of counting sticks.
Second, if we're talking about other data structures, especially recursive ones, e.g. lists, then having easily available (and performant) structural recursion is just more useful than having right folds out of the box: those can be recreated easily, but going in the other direction is much more convoluted.
> then the numbers should not be stored as Peano integers a.k.a. base 1 in the first place
That's my point though. The linked n-ary encoding by Mogensen, for example, does not suffer from such complexities. Depending on the reducer's implementation, (supported) operations on my presented de Bruijn numerals are also sublinear. I doubt 8-tuples of Church booleans would be efficient though - except when letting machine instructions leak into LC.
Though I agree that the focus of functional data structures should lie on embedded folds. Compared to nested Church pairs, folded Church tuples (\cons nil.cons a (cons b nil)) or Church n-tuples (\s.s a b c) should be preferred in many cases.
just Scott encoding, Scott-Mogensen refers to a meta encoding of LC in LC. Scott's encoding is fine but requires fixpoint recursion for many operations as you said.
Interestingly though, Mogensen's ternary encoding [1] does not require fixpoint recursion and is the most efficient (wrt being compact) encoding in LC known right now.
> Just use [..], seriously
do you have any further arguments for Scott's encoding? There are many number encodings with constant time predecessor, and with any number requiring O(n) space and `add` being this complex, it becomes quite hard to like
[1]: https://dl.acm.org/doi/10.5555/646802.705958