Friday I wrote about the type

data FunList a b = Done b | More a (FunList a (a -> b))

Where did this type come from? What can you use it for?

The story starts with another way of constructing `FunList`s, besides `pure`.
For contrast I will call it 'impure'.

impure :: a -> FunList a a impure a = More a (Done id)

I claim that *any* FunList can be written in the form

pure b <*> impure a_{1}<*> impure a_{2}<*> ...

for some `b` and `a _{1}`,

withImpure :: Applicative f => (a -> f a) -> FunList a b -> f b withImpure imp (Done b) = pure b withImpure imp (More a f) = withImpure imp f <*> imp a

If you use this with the Applicative instance from last time you will find that `getAs . withImpure impure = reverse . getAs`!, I have written a reverse function without realizing it. Since this time we *don't* want to reverse the list, I am going to turn the Applicative instance around for this post:

instance Applicative (FunList a) where pure = Done c <*> Done b = fmap ($b) c c <*> More a z = More a ((.) <$> c <*> z)

To support my claim above I need to prove that `withImpure impure = id`. This is a simple exercise in proof by induction. First of, we have that

withImpure impure (Done b) = pure b = Done b

Now assume that the theorem holds for `z`, i.e. `withImpure impure z = z`. Then

withImpure impure (More a z) = withImpure impure z <*> impure a = z <*> impure a -- by induction hypotheis = z <*> More a (Done id) = More a ((.) <$> z <*> Done id) = More a (fmap ($id) (fmap (.) z)) = More a (fmap (.id) z) = More a z

By induction `withImpure impure z = z` for all `z`.

I actually came upon FunList from the other direction.
I started with the higher order type

type ApplicativeFunList a b = forall f. Applicative f => (a -> f a) -> f b

An ApplicativeFunList is a function of the form `\imp -> applicativeStuff`. Since the applicativeStuff has to work for *any* applicative functor it can only use operations from that class in addition to the `imp` argument. Because of the Applicative laws, things like `anything <*> pure x` are the same as `(x) <> anything`, so the only interesting functions of this form are

\imp -> pure b \imp -> pure b <*> imp a_{1}\imp -> pure b <*> imp a_{1}<*> imp a_{2}-- etc.

Which is precisely what a `FunList` can represent!
Indeed, we can convert any FunList to an ApplicativeFunList, and back again:

toAFL :: FunList a b -> ApplicativeFunList a b toAFL fl imp = withImpure imp fl fromAFL :: ApplicativeFunList a b -> FunList a b fromAFL afl = afl impure

We already know that `fromAFL . toAFL = withImpure impure = id`. The other way around, I claim (but do not prove yet) that `toAFL . fromAFL = id`. Hence, `FunList` and `ApplicativeFunList` are isomorphic!

## Comment