Inverting a fold

Question

Suppose for a minute that we think the following is a good idea:

data Fold x y = Fold {start :: y, step :: x -> y -> y}

fold :: Fold x y -> [x] -> y

Under this scheme, functions such as length or sum can be implemented by calling fold with the appropriate Fold object as argument.

Now, suppose you want to do clever optimisation tricks. In particular, suppose you want to write

unFold :: ([x] -> y) -> Fold x y

It should be relatively easy to rule a RULES pragma such that fold . unFold = id. But the interesting question is... can we actually implement unFold?

Obviously you can use RULES to apply arbitrary code transformations, whether or not they preserve the original meaning of the code. But can you really write an unFold implementation which actually does what its type signature suggests?

Answer 1

No, it's not possible. Proof: let

f :: [()] -> Bool
f[] = False
f[()] = False
f _ = True

First we must, for f' = unFold f, have start f' = False, because when folding over the empty list we directly get the start value. Then we must require step f' () False = False to achieve fold f' [()] = False. But when now evaluating fold f' [(),()], we would again only get a call step f' () False, which we had to define as False, leading to fold f' [(),()] ≡ False, whereas f[(),()] ≡ True. So there exists no unFold f that fulfills fold $ unFold f ≡ f.                                                                                                                                              □

Answer 2

You can, but you need to make a slight modification to Fold in order to pull it off.

All functions on lists can be expressed as a fold, but sometimes to accomplish this, extra bookkeeping is needed. Suppose we add an additional type parameter to your Fold type, which passes along this additional contextual information.

data Fold a c r = Fold { _start :: (c, r), _step :: a -> (c,r) -> (c,r) }

Now we can implement fold like so

fold :: Fold a c r -> [a] -> r
fold (Fold step start) = snd . foldr step start

Now what happens when we try to go the other way?

unFold :: ([a] -> r) -> Fold a c r

Where does the c come from? Functions are opaque values, so it's hard to know how to inspect a function and know which contextual information it relies on. So, let's cheat a little. We're going to have the "contextual information" be the entire list, so then when we get to the leftmost element, we can just apply the function to the original list, ignoring the prior cumulative results.

unFold :: ([a] -> r) -> Fold a [a] r
unFold f = Fold { _start = ([], f [])
                , _step = \a (c, _r) -> let c' = a:c in (c', f c') }

---

Now, sadly, this does not necessarily compose with fold, because it requires that c must be [a]. Let's fix that by hiding c with existential quantification.

{-# LANGUAGE ExistentialQuantification #-}
data Fold a r = forall c. Fold
  { _start :: (c,r)
  , _step :: a -> (c,r) -> (c,r) }

fold :: Fold a r -> [a] -> r
fold (Fold start step) = snd . foldr step start

unFold :: ([a] -> r) -> Fold a r
unFold f = Fold start step where
  start = ([], f [])
  step a (c, _r) = let c' = a:c in (c', f c')

Now, it should always be true that fold . unFold = id. And, given a relaxed notion of equality for the Fold data type, you could also say that unFold . fold = id. You can even provide a smart constructor that acts like the old Fold constructor:

makeFold :: r -> (a -> r -> r) -> Fold a r
makeFold start step = Fold start' step' where
  start' = ((), start)
  step' a ((), r) = ((), step a r)