Oleg, Let me try to understand what you're saying here: (1) Church encoding was discovered and investigated in an untyped setting. I understand your tightness criterion to mean surjectivity, the absence of which means having to deal with junk. (2) Church didn't give an encoding for pattern-matching to match with construction. Boehm and Berarducci did. So properly speaking, tail and pred for Church-encoded lists and nats are trial-and-error affairs. But the point is they need not be if we use B-B encoding, which looks _exactly_ the same, except one gets a citation link to a systematic procedure. So it looks like you're trying to set the record straight on who actually did what. -- Kim-Ee On Tue, Sep 18, 2012 at 3:27 PM, <oleg@okmij.org> wrote:
There has been a recent discussion of ``Church encoding'' of lists and the comparison with Scott encoding.
I'd like to point out that what is often called Church encoding is actually Boehm-Berarducci encoding. That is, often seen
newtype ChurchList a = CL { cataCL :: forall r. (a -> r -> r) -> r -> r }
is _not_ Church encoding. First of all, Church encoding is not typed and it is not tight. The following article explains the other difference between the encodings
http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html
Boehm-Berarducci encoding is very insightful and influential. The authors truly deserve credit.
P.S. It is actually possible to write zip function using Boehm-Berarducci encoding: http://okmij.org/ftp/ftp/Algorithms.html#zip-folds