Summary: At the bottom of the message, I give the little fix for the
bug in our ICFP paper. This makes the paper completely
correct... until the next bug is found. :-)
But first, some discussion is in order.
My week was quite full last week, so I'm only now getting around to
reponding to Oleg's post:
> At ICFP'98, Jonathan Sobel, on behalf of himself and Daniel
> P. Friedman uttered a battle cry "Use ANA!". It was at the end of his
> talk "Recycling continuations". This talk had proved that anamorphisms
> can be very efficiently compiled and executed without leaving no or
> little garbage.
> [...]
> This article is to show that 'map' and 'unfold' are not powerful
> enough to express DB:for-each; DB:for-each is an anamorphism and
> thus _requires_ a more capable list generator.
Echoing Jeremy Gibbons, I generally think of "unfold" and "ana" as
synonyms, although "unfold" is usually defined as a 3-argument
function, whereas "ana" is usually defined as a 1-argument function.
So "ana" is more general, but it doesn't really make sense to claim
that the fact that some function is an anamorphism implies that
3-arg "unfold" is too weak to express it.
Anyway, on to Oleg's notes about our ICFP paper:
> But first, about Sobel's paper. Unfortunately, his definition of
> list-anamorophism needs extension. He defined a function (remove x L)
> that removes all instances of x from a list L as an anamorphism:
I'll omit the definitions of the List functor and ana here, and just
include "remove." In the current notation of our datatype system for
Scheme (which looks like it's about to change one more time!), the
"remove" we defined in the paper looked like this:
(define remove
(lambda (x l)
(let ((psi (lambda (l)
(type-case List l
((empty-list) l)
((pair h t) (if (equal? x h) t l))))))
((List-ana psi) l))))
Oleg pointed out that:
> Unfortunately, this 'remove' doesn't quite cut it: consider applying
> it to a list '(3 3). It would return '(3) while the expected result
> is '()
Yep, it's true. Whenever the beast above finds something that needs
to be removed, it leaves it out and *skips* the next item in the list
without checking it! Sorry about that. As you've probably noticed,
the paper was done in Noweb, so we were able to run all the code easily
to check it. It seems there should have been a little more
checking. :-) (or maybe a proof...) Thanks, Oleg, for finding the
bug. Long live the open-source system of research!
But when Oleg "modified Sobel's anamorphism," as he put it, he created
a strange thing that produces the correct answer but no longer has the
mathmatical properties of anamorphisms. An anamorphism is intimately
connected to the type-constructing functor whose fixpoint is the
recursive type you want to produce. The object part of the functor
maps types to types; the arrow part maps arrows to arrows. And the
whole thing is supposed to be a functor in the categorical sense.
The arrow part of Oleg's List functor, which he calls "maybe-map-cdr,"
causes it not to be a functor. For example, it fails the simple
constraint that F(id_t) = id_{F(t)}.
If we wanted to follow through with Oleg's idea of having "remove"
substitute bottoms for the removed elements, we would define "remove"
as a *hylomorphism*, i.e., an anamorphism followed by a catamorphism.
(Or, we could just define "remove" as a catamorphism and be done with
it!)
BUT there is a much simpler solution. You really can define "remove"
as an anamorphism, with no special extensions needed to the List type
(object part of the functor), the List mapper (arrow part of the
functor), or the "ana" operator:
(define remove
(lambda (x l)
(letrec ((psi (lambda (l)
(type-case List l
((empty-list) l)
((pair h t) (if (equal? x h) (psi t) l))))))
((List-ana psi) l))))
In case the changes were too small for anyone to notice, the "let"
became a "letrec" and the "t" became "(psi t)." Although this change
introduces a recursion, it is totally harmless: just a little tail
call (i.e., loop). The loop never involves any allocation, so the
results of our paper still hold: if "List-ana" is the recycling
version, then "remove" operates with no space overhead for the
recursion.
I'll post a corrected version of the paper to my web page:
http://www.cs.indiana.edu/~jsobel/
Thanks for the careful readings!
--
Jonathan