Recursive definitions are a lot of fun. The typical example of a recursive definition is the natural numbers:
A natural number is either 0 or the successor of a natural number.
Expressed in Haskell, this is:
data Nat = Zero | Succ Nat
Zero is Zero, as you’d expect. One is Succ Zero, two is Succ (Succ Zero), etc.
The natural numbers can be recursively defined like this.
Lists are extremely similar to the natural numbers – we just attach something to each Succ, and now we’ve got a linked list of things.
data List a = Nil | Cons a (List a)
And, interestingly enough, you can encode the natural numbers as lists. We can replace the a with the unit type () and the list is equivalent to the natural number representing it’s length:
Cons () (Cons () (Cons () Nil ))
Succ (Succ (Succ Zero))
Cool! But now that I’ve seen one example of this sort of progression, I want to see what else can happen.
For lists, we added a type variable a to the definition of the natural numbers.
Let’s try adding another type variable:
data TwoList a b = Z | S a b (TwoList a b)
But this is boring. It’s basically the exact same thing as List (a, b).
And it’s easy to see that adding more of these variables is the same as adding elements to the tuple, so a FiveList a b c d e is really just a List (a, b, c, d, e).
So, we don’t want our new type variable to be trivially expressible by a regular list.
What’s next?
We could add the type variable to the Nil constructor, but that’s also pretty uninteresting.
List' b a = Nil' b | Cons' a (List' b a) doesn’t buy any real expressive power.
Well, let’s differentiate that new type variable b in some way. Since it’s a type variable, we can really only talk about the kind that it has. b :: * didn’t work, so let’s try b :: * -> *.
data ListB a b = NilB | ConsB (b a) (ListB a b)
Ah, but this is also trivial!
A ListB Int Maybe is the same as a List (Maybe Int).
We have bought nothing with this arrangement.
Well, we can’t just apply a to b, we have to try something else.
The remaining list is the only thing left, so let’s try that.
data ListF a b = NilF | ConsF b (a (ListF a b))
There we go.
This is not trivially expressible as a List!
And I really felt weird writing ListF Int Maybe so I swapped the type variables: b is now the value, and a is the new thing we’re playing with.
But… What does it look like? Let’s try a ListF Maybe Int:
-- specialized type: List = Nil | Cons Int (Maybe List)
nil = NilF
one = ConsF 1 Nothing
one' = ConsF 1 (Just NilF)
two = ConsF 1 (Just (ConsF 2 Nothing))
Interesting! We have two termination cases here.
The ordinary NilF that we get from the list definition, and Nothing we get from using Maybe as the f.
What about Either?
Let’s see what ListF (Either String) Int looks like:
-- specialized: List = Nil | Cons Int (Either String List)
oneR = ConsF 1 (Right NilF)
oneL = ConsF 1 (Left "asdf")
twoR = ConsF 1 (Right (ConsF 2 (Right NilF)))
twoL = ConsF 1 (Right (ConsF 2 (Left "nope")))
We’ve got two ways to terminate again.
The first is the NilF constructor.
The second is the string in the Either definition.
Is there an interesting thing of kind * -> * can we try this with?
We’ve tried Maybe and Either, which were both basically the same thing.
We can figure out why by inspecting their definitions:
data Maybe a = Nothing | Just a
data Either b a = Left b | Right a
They’re both sum types.
When we have Maybe (), we have two values: Nothing and Just ().
We’ve only added 1 to the number of values in the type variable.
Maybe Bool has Nothing, Just True, and Just False.
Again, just one more value than Bool itself.
When we use these in our augmented list, the a variable is fixed to ListF f a.
So anything that doesn’t carry the last type variable is just going to terminate the list.
Either can therefore terminate the list with a different type, but this isn’t fundamentally very interesting.
Since simple sum types don’t seem to be terribly interesting, let’s try a product type!
type With a = (,) a
is a convenient synonym we’ll use.
To keep things simple, we’ll stick with Bool for now.
oneL :: ListF (With Bool) Int
oneL = ConsF 1 (True, NilF)
twoL :: ListF (With Bool) Int
twoL = ConsF 1 (False, ConsF 2 (True, NilF))
Well, this feels just like a List (a, b), but laid out differently.
So far, product and sums haven’t really bought us anything.
Fortunately, there are exponential types, or functions as they’re more commonly known.
Reader is defined as type Reader r = (->) r.
It’s a functor, like Maybe and Either, and it has the right kind when we supply the type to be read.
Let’s… give that a shot?
We’ll specialize the Reader to Bool because there’s only two possible values of type Bool. This makes it a bit easier to deal with.
-- specialized: List = Nil | Cons Int (Reader Bool List)
Ok, wait, what does this mean again?
A ListF (Reader Bool) Int means that the next item in the list is a function that takes a Boolean value and returns a List.
Ok. Let’s do this.
one = ConsF 1 (\c -> NilF)
two = ConsF 1 (\c -> if c then NilF else ConsF 2 (const NilF))
Wait, what? We’re expressing control flow and branching! Oh, this is just too cool. How do we evaluate that? We’ll pass a single in the thing and see what it does, and collect the results into a regular list.
single :: Bool -> ListF (Reader Bool) Int -> [Int]
single _ NilF = []
single c (ConsF n f) = n : single c (f c)
single False two == [1, 2]
single True two == [1]
Cool! By using the Reader functor we’ve turned the List into a binary tree. Observe:
binTree =
ConsF 1 $ \a ->
if a then branchOne
else branchTwo
branchOne =
ConsF 10 $ \a ->
if a then binTree
else branchTwo
branchTwo =
ConsF 2 $ \a ->
if a then NilF
else branchTwo
Check this craziness out. What even is it? It’s some kind of graph/maze thing. Let’s write a function to traverse this business:
traverseBool :: [Bool] -> ListF (Reader Bool) Int -> [Int]
traverseBool _ NilF = []
traverseBool [] (Cons n _) = [n]
traverseBool (b:bs) (Cons n f) = n : traverseBool bs (f b)
Alright, so given [True, True, False, True, True, False], we’ll generate [1, 10, 1, 2]. Given a different list of Bools, it’d traverse differently.
Very interesting!
We can represent binary trees using Reader Bool.
Bool has two possible values, and we’ve got trees with two branches.
It seems that the number of branches we’ll get is dependent on how many inhabitants there are in the type.
If that’s the case, then Reader () will simply be a linked list.
fancyList :: ListF (Reader ()) Int
fancyList = ConsF 1 (\() -> ConsF 2 (\() -> NilF))
So List a can be expressed as ListF (Reader ()) a, and the natural numbers are then ListF (Reader ()) ().
This is the first really interesting functor we’ve used here. Either and Maybe simply provided extra termination options. Tupling just added a bit of extra information at each cell. Reader gives us branching.
Finally, let’s try another more interesting functor: State!
newtype State s a
= State
{ runState :: s -> (a, s) }
-- specialized type: ListF (State Bool) Int
one = ConsF 1 (State (\s -> (NilF, s)))
two =
ConsF 1 (State (\s -> (ConsF 2 (State (\s' -> (NilF, not s') )), s)))
Well, this is kind of weird. Let’s traverse it and see what happens.
traverseState :: [Bool] -> ListF (State Bool) Int -> [Int]
traverseState _ NilF = []
traverseState [] (ConsF n _) = [n]
traverseState (b:bs) (ConsF n s) =
n : traverseState bs (fst (runState s b))
So, this will go down the list, applying the Bool values to the states in turn, extracting the Ints, and discarding the result states. This isn’t any different from Reader yet. It seems like we should be able to kick off the computation with a single Bool and let it carry on down. Let’s try passing the state down.
-- specializing the type:
-- traverseState' :: Bool -> ListF (State Bool) Int -> [Int]
traverseState' :: s -> ListF (State s) a -> [a]
traverseState' _ NilF = []
traverseState' b (ConsF n s) =
let (list, state) = runState s b
in n : traverseState' state list
And if we want to remember the state history,
-- specialized:
-- traverseState'' :: Bool -> ListF (State Bool) Int -> [(Int, Bool)]
traverseState'' :: s -> ListF (State s) a -> [(a, s)]
traverseState'' _ NilF = []
traverseState'' b (ConsF n s) =
let (list, state) = runState s b
in (n, b) : traverseState' state list
Cool!
So now we can drop a seed value into a chain of stateful computations and the result will be a list of the return values of each computation.
Those type signatures are actually a bit more specific than they need to be: we can replace the signature with traverseState' :: a -> ListF (State a) b -> [b]
Let’s do something a tiny bit more interesting with it:
collatz :: Int -> [Int]
collatz x = traverseState' x (chain x)
where
chain n = ConsF n (State go)
go y =
if y == 1
then (NilF, y)
else let val = if even y
then y `div` 2
else 3 * y + 1
in (chain val, val)
This will evaluate the Collatz Conjecture for a given number.
Now, what is ListF?
It’s kind of similar to the Free monad, but there’s an important distinction:
data Free f a = Pure a | Free (f (Free f a))
data ListF f a = Nil | ConsF a (f (ListF f a))
Free only carries values at the leaves or end of the chain. ListF carries values at each step. The common structure seems like it could be extracted out like so:
data DualFree f b a = DPure a | DFree b (f (DualFree f b a))
Using the above definition of DualFree, the free monad can be thought of as a list of computations in the f functor with some return value b where a is ().
ListF on the other hand is a list of values a along with a list of computations in the f functor.
ListF over Reader r gives us trees of values.
ListF over State s gives us unfolding structures.
In fact… This is (almost!) the list monad transformer “done right!” The canonical implementation is:
newtype ListT m a =
ListT { unListT :: m (Maybe (a, ListT m a)) }
This uses the Maybe to avoid having the Nil data constructor, which allows it to use the newtype declaration.
This also ensures that even the first element in the list is wrapped in the monad.
The ListF version I wrote associates the monadic actions with the links between values, and this version associates the monadic action with the values themselves.
It’s also pretty similar to the cofree comonad:
newtype Cofree h a =
Cofree { unCofree :: (a, h (Cofree h a)) }
If you took out the NilF constructor, anyway.
Thanks to Gary Fixler for notifying me that the type signature in
traverseStatewas wrong!