[Haskell-cafe] Unfold fusion

[Dan Doel]

On Wednesday 06 May 2009 11:27:08 am Adrian Neumann wrote:
> Hello,
>
> I'm trying to prove the unfold fusion law, as given in the chapter
> "Origami Programming" in "The Fun of Programming". unfold is defined
> like this:
>
> unfold p f g b = if p b then [] else (f b):unfold p f g (g b)
>
> And the law states:
>
> unfold p f g . h = unfold p' f' g'
> with
> 	p' = p.h
> 	f' = f.h
> 	h.g' = g.h

If you don't mind a more category theoretic tack, we can argue something like 
this:

Lists of A are the terminal coalgebra for the functor L X = 1 + A*X. Defining 
them this way means that we get the unique existence of the above unfold 
function. Roughly, for any:

    ob : X -> L X

there exists a unique:

    unfold ob : X -> [A]

Such that:

    out . unfold ob = map (unfold ob) . ob

where out : [A] -> 1 + A*[A] is the coalgebra action of the list (observing 
either that it's null, or what the head and tail are), and map corresponds to 
the functor L (so we're mapping on the X part, not the A part).

Coalgebra actions ob have type:

    ob : X -> 1 + A*X

and you can finesse that into three functions in something like Haskell:

    p : X -> 2, f : X -> A, g : X -> X

which is what your unfold at the start does.

Now, we have:

  p' = p . h
  f' = f . h
  h . g' = g . h

Suppose we combine things back into the single coalgebra actions. Then we 
have:

    ob  : X -> 1 + A*X
    ob' : X' -> 1 + A*X'

where ob corresponds to (p,f,g) and ob' corresponds to (p',f',g'). Now, the 
equations above tell us that with regard to these observation functions:

    ob' agrees with ob . h as far as left or right goes
    ob' agrees with ob . h as far as As go, when applicable
    map h . ob' agrees with ob . h as far as Xs go.

All together this means:

    map h . ob' = ob . h

Which means it's an L-coalgebra homomorphism. Such homomorphisms are arrows in 
the category of L-coalgebras, for which [A] is a terminal object (giving us 
the unique existence property of arrows to it from any other object).

So, h : X' -> X is an arrow in the L-coalgebra category. And, so are:

    unfold ob  : X  -> [A]
    unfold ob' : X' -> [A]

Since this is a category:

    unfold ob . h : X' -> [A]

must also be an arrow. *However*, [A] being a terminal object means that for 
every object, there is a unique arrow from it to [A]. We appear to have two 
from X':

    unfold ob'    : X' -> [A]
    unfold ob . h : X' -> [A]

So the uniqueness property tells us that these are the same arrow. Thus,

    unfold ob' = unfold ob . h
    unfold p' f' g' = unfold p f g . h

and we're done. Hopefully that wasn't too verbose. Normally you'd have most of 
that covered by the time you got to proving the unfold fusion, but I wasn't 
sure how much of that part of the theory you'd read before.

Another way you can go is to use coinduction and bisimulation (which can be 
ultimately explained in terms of the above primitives), which talks about 
making individual observations, which would go something like:

  If for all x:
    null (f x) = null (f' x)
   (if not null)
    head (f x) = head (f' x)
    tail (f x) = tail (f' x)

(where equality on the tail is defined as being the same subsequent 
observations) then f and f' are the same function (by coinduction). If we look 
at the equations at the start:

    null . unfold p' f' g' = p'
                           = p . h
                           = null . unfold p f g . h
    head . unfold p' f' g' = f'
                           = f . h
                           = head . unfold p f g . h
    tail . unfold p' f' g' = unfold p' f' g' . g'
                          (coinductive hypothesis?)
                           = unfold p f g . h . g'
                           = unfold p f g . g . h
                           = tail . unfold p f g . h

unfortunately it looks like I'm doing something wrong in that "coinductive 
hypothesis" step, by assuming that unfold p' f' g' = unfold p f g . h. 
However, I'm pretty sure that's how these sorts of coinductive proofs work, 
though I'm not familiar enough with presenting this angle to explain why you 
should allow it. Anyhow, if you believe the above, then we've established that 
all the observations you can make are equal, so our functions must be equal.

Note, that it's somewhat important to have these coalgebraic/coinductive proof 
methods here. Miguel Mitrofanov gave you a proof that:

    take n . unfold p f g . h = take n . unfold p' f' g'

for all n using induction. But, that is not exactly a proof that they are 
equal, but a proof that any finite amount of observation you can make of their 
output will be equal, and unfold can produce infinite objects. That may be 
good enough (for instance, in a total functional programming language extended 
with coinduction, only the inductive/recursive parts and single-step 
observation of coinductive values 'ought' to be subject to evaluation, so you 
can only make finite observations of any corecursively defined value, and the 
above 'take n' proof in a way covers everything you're able to do), but they 
feel different, to me at least.

Anyhow, I'll stop rambling. Hope that helped some.

-- Dan