[Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
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?
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
> > reference given that Boehm-Berarducci's algorithm is rarely used?
> > When I need to encode pattern matching it's goodbye Church and hello
> > 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...
More information about the Haskell-Cafe