[Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists

[Kim-Ee Yeoh]

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 at 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 }
>
> (in http://community.haskell.org/%7Ewren/list-extras/Data/List/Church.hs<http://community.haskell.org/~wren/list-extras/Data/List/Church.hs>
>  )
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120918/aaeb52da/attachment.htm>