Oleg,<div><br></div><div>Let me try to understand what you're saying here:</div><div><br></div><div>(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.</div>
<div><br></div><div>(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.</div>
<div><br></div><div>So it looks like you're trying to set the record straight on who actually did what.</div><div><br></div><div><br></div><div>-- Kim-Ee<br><br><br><div class="gmail_quote">On Tue, Sep 18, 2012 at 3:27 PM, <span dir="ltr"><<a href="mailto:oleg@okmij.org" target="_blank">oleg@okmij.org</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><br>There has been a recent discussion of ``Church encoding'' of lists and<br>
the comparison with Scott encoding.<br><br>I'd like to point out that what is often called Church encoding is<br>actually Boehm-Berarducci encoding. That is, often seen<br><br>> newtype ChurchList a =<br>> CL { cataCL :: forall r. (a -> r -> r) -> r -> r }<br>
<br>(in <a href="http://community.haskell.org/~wren/list-extras/Data/List/Church.hs" target="_blank">http://community.haskell.org/%7Ewren/list-extras/Data/List/Church.hs</a> )<br><br>is _not_ Church encoding. First of all, Church encoding is not typed<br>
and it is not tight. The following article explains the other<br>difference between the encodings<br><br> <a href="http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html" target="_blank">http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html</a><br>
<br>Boehm-Berarducci encoding is very insightful and influential. The<br>authors truly deserve credit.<br><br>P.S. It is actually possible to write zip function using Boehm-Berarducci<br>encoding:<br> <a href="http://okmij.org/ftp/ftp/Algorithms.html#zip-folds" target="_blank">http://okmij.org/ftp/ftp/Algorithms.html#zip-folds</a><br>
</blockquote></div></div>