<div>Both are excellent points, thank you.</div><div><br></div><div>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."</div>
<div><br></div><div>L&S does not cite B&B. Could they be the same algorithm?</div><div><br></div><br clear="all">-- Kim-Ee<br>
<br><br><div class="gmail_quote">On Wed, Sep 26, 2012 at 11:41 AM, <span dir="ltr"><<a href="mailto:oleg@okmij.org" target="_blank">oleg@okmij.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im"><br>
> Wouldn't you say then that "Church encoding" is still the more appropriate<br>
> reference given that Boehm-Berarducci's algorithm is rarely used?<br>
><br>
</div><div class="im">> When I need to encode pattern matching it's goodbye Church and hello Scott.<br>
> Aside from your projects, where else is the B-B procedure used?<br>
<br>
</div>First of all, the Boehm-Berarducci encoding is inefficient only when<br>
doing an operation that is not easily representable as a fold. Quite<br>
many problems can be efficiently tackled by a fold.<br>
<br>
Second, I must stress the foundational advantage of the<br>
Boehm-Berarducci encoding: plain System F. Boehm-Berarducci encoding<br>
uses _no_ recursion: not at the term level, not at the type level. In<br>
contrast, the efficient for pattern-match encodings need general<br>
recursive types. With such types, a fix-point combinator becomes<br>
expressible, and the system, as a logic, becomes inconsistent.<br>
<br>
</blockquote></div><br>