Where do I get my non-regular types?

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 FunLists, 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 a1 <*> impure a2 <*> ...

for some b and a1, a2, etc. In other words, impure and Applicative are all that you need. The following function converts a FunList to the above form, where impure and the Applicative instance are left as parameters:

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 a1
\imp -> pure b <*> imp a1 <*> imp a2
-- 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

(optional)
(optional, will not be revealed)
8 + 12 =
Use > code for code blocks, @code@ for inline code. Some html is also allowed.