Where do I get my non-regular types?

<a href="http://twan.home.fmf.nl/code/blog/haskell/non-regular2.lhs" style="color:grey;font-size:smaller;">[This post is literate Haskell, view the source code here]</a>

> -- IGNORE
> {-# LANGUAGE Rank2Types #-}
> {-# LANGUAGE ImplicitParams #-}
> import Control.Applicative

<a href="http://twan.home.fmf.nl/code/blog/haskell/non-regular1.lhs">Friday I wrote</a> 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@.


<br>
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://twan.home.fmf.nl/code/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