title: Where do I get my non-regular types?
date: 2009-04-25
tags: haskell
sourcelink: This post is literate Haskell, click here to download the source code.
> -- IGNORE
> {-# LANGUAGE Rank2Types #-}
> {-# LANGUAGE ImplicitParams #-}
> import Control.Applicative
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@, @a__2@, 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 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!
> -- HIDDEN
> -- this is stuff from the previous post, see http://twanvl.nl/blog/haskell/non-regular1.lhs
>
> instance Functor (FunList a) where
> fmap f (Done b) = Done (f b)
> fmap f (More a z) = More a (fmap (f .) z)
>
> -- reverse instance is above
> {-
> instance Applicative (FunList a) where
> pure = Done
> c <*> Done b = fmap ($b) c
> c <*> More a z = More a ((.) <$> c <*> z)
> -}
>
> -- for testing purposes
> t1 = More 1 $ More 2 $ More 2 $ More 3 $ Done (,,,)
>
> getB :: FunList a b -> b
> getB (Done b) = b
> getB (More a z) = getB z a
>
> getAs :: FunList a b -> [a]
> getAs (Done _) = []
> getAs (More a z) = a : getAs z