Re: Am I missing something about unfoldr?

15 Aug 2014


      I think that "for lists" version is pretty much what I ended up with (I
haven't worked through what all the others might be about yet). I don't
understand the "fight" you refer to, unless you actually mean trying to
implement both foldr/build and destroy/unfoldr at the same time. If you
write hyloList in a more inliner-friendly fashion:

hyloList fnil fcons g = go
  where
     go a = case g a of
        Nothing -> fnil
        Just (x,a') -> fcons x (go a')

and then write

unfoldr g a = build $ \c n -> hyloList n c g a

Then foldr/build gets you

foldr c n (unfoldr g a) = hyloList n c g a

And then if g is statically known and sufficiently simple, the Maybes go
away.
On Aug 14, 2014 10:23 PM, "wren romano"  wrote:
...
On Sat, Jul 26, 2014 at 5:10 PM, David Feuer 
wrote:
...
I think this is probably what Hinze et al, "Theory and Practice of
Fusion"
describes as the fold/unfold law, "a fold after an unfold is a hylo" but
I
don't know enough to read that paper.
The two main styles of fusion are build/foldr and unfoldr/destroy. The
difference is in which side of the slash has the recursion. GHC's
choice to use build/foldr is because that worked more nicely with
various other facets of the language; this is discussed in some of the
early papers about list fusion in GHC.
The issue we run into is that you can't really have unfoldr/foldr
fusion because having recursion on both sides means they fight with
each other. But! we can fuse the operations together into a single
operation, and that single operation should behave nicely with both
build/foldr and unfoldr/destroy styles of fusion.
A catamorphism is the class of recursion schemes you get by
generalizing over the list data type in foldr (hence foldr is the list
instance of cata). Dually, an anamorphism is the class of corecursion
schemes you get by generalizing over the list data type in unfoldr
(hence unfoldr is the list instance of ana). If we use an anamorphism
to expand some "seed" value into a structure (e.g., a list), but then
we immediately use a catamorphism to destroy that structure to produce
a "summary" value, then we can eliminate the intermediate structure
and just go from seed to summary directly. That's what hylomorphisms
do. So we have:
roll :: F (fix F) -> fix F
    unroll :: fix F -> F (fix F)
cata :: (F b -> b) -> fix F -> b
    cata f = f . fmap (cata f) . unroll
ana :: (a -> F a) -> a -> fix F
    ana g = roll . fmap (ana g) . g
hylo :: (F b -> b) -> (a -> F a) -> a -> b
    hylo f g = f . fmap (hylo f g) . g
where
cata f . ana g
    == {definition}
    f . fmap (cata f) . unroll . roll . fmap (ana g) . g
    == {unroll/roll fusion}
    f . fmap (cata f) . fmap (ana g) . g
    == {functor law}
    f . fmap (cata f . ana g) . g
    == {inductive hypothesis}
    f . fmap (hylo f g) . g
    == {definition}
    hylo f g
More specifically for lists:
hyloList :: b -> (x -> b -> b) -> (a -> Maybe (x,a)) -> a -> b
    hyloList fnil fcons g a =
        case g a of
        Nothing -> fnil
        Just (x,a') -> fcons x (hyloList fnil fcons g a')
If we inline hyloList whenever g is known concretely, then the
intermediate Maybe(_,_) structure will be fused away by the
case-of-constructor transform.
Hopefully that should be enough to get you started?
--
Live well,
~wren