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@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.