Am I missing something about unfoldr?

[wren romano]

On Sat, Jul 26, 2014 at 5:10 PM, David Feuer <david.feuer at gmail.com> 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