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

Kim-Ee Yeoh ky3 at atamo.com
Wed Sep 26 15:48:03 CEST 2012


Both are excellent points, thank you.

Your mention of general recursion prompts the following: in 1995, ten years
after publication of Boehm-Berarducci, Launchbury and Sheard investigated
transformation of programs written in general recursive form into
build-foldr form, with an eye towards the normalization laid out in "A Fold
for All Seasons."

L&S does not cite B&B. Could they be the same algorithm?


-- Kim-Ee


On Wed, Sep 26, 2012 at 11:41 AM, <oleg at okmij.org> wrote:

>
> > Wouldn't you say then that "Church encoding" is still the more
> appropriate
> > reference given that Boehm-Berarducci's algorithm is rarely used?
> >
> > When I need to encode pattern matching it's goodbye Church and hello
> Scott.
> > Aside from your projects, where else is the B-B procedure used?
>
> First of all, the Boehm-Berarducci encoding is inefficient only when
> doing an operation that is not easily representable as a fold. Quite
> many problems can be efficiently tackled by a fold.
>
> Second, I must stress the foundational advantage of the
> Boehm-Berarducci encoding: plain System F. Boehm-Berarducci encoding
> uses _no_ recursion: not at the term level, not at the type level.  In
> contrast, the efficient for pattern-match encodings need general
> recursive types. With such types, a fix-point combinator becomes
> expressible, and the system, as a logic, becomes inconsistent.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120926/3018f1fc/attachment.htm>


More information about the Haskell-Cafe mailing list