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