Alternative List Implementation

[HalosGhost]

It looks like an accepted alternative (to nested church pairs) implementation of lists in the lambda calculus is representing them as a right-fold.

There are a few benefits to this style:

• it mirrors the style of natural numbers and booleans (etc.) in that the type's encoding is the (or, at least, a) valid eliminator
• fold functions become superfluous (rather, you just need to eval the list with the proper arguments)

The obvious negative is that it would require updating the term-printer to support this encoding rather than the current version.

Is this too much work for not enough gain?