Free monads allow derivation of many common data structures, including lists. What arises when we index them?

I’d like to augment the current discussion on free monads with some thoughts about indexed free monads, and what we can get from them. (Incidentally, if you haven’t read it yet, please check out Conor McBride’s Kleisli arrows of outrageous fortune for an in-depth discussion of indexed types.)

The basics of free monads

First, a quick and dirty explanation of free monads; essentially, they are a way of rolling up an arbitrarily high tower of functors:

> {-# LANGUAGE TypeOperators, RankNTypes #-}
> {-# LANGUAGE PolyKinds, DataKinds, KindSignatures #-}
> {-# LANGUAGE GADTs #-}

> module IFree where

> data Free f e = Roll (f (Free f e))
>               | Pure e

This is just induction: Pure is the base case, and Roll is the inductive step. The thing that may initially be confusing is getting an intuition for what f is supposed to be: think of it as single layer of data with a (fully polymorphic) facility to bind to further data; so, what Free does is saturate the functor’s data slot recursively until you get to the base-case.

A particularly enlightening instantiation of Free is that of the partially-applied product functor and the Unit type:

$\begin{align} \def\F{\alpha\times} \textbf{Free} &= \Lambda f. \Lambda e.\ f\; (\textbf{Free}\; f\; e) + e\\ \textbf{Foo} &= \Lambda \alpha.\ \textbf{Free}\; (\Lambda\beta.\ \F\beta)\ 1\\ &\equiv \Lambda \alpha.\ \F \textbf{Foo} + 1\\ &\equiv \Lambda \alpha.\ \F (\F \textbf{Foo} + 1) + 1\\ &\equiv \Lambda \alpha.\ \F (\F (\F \textbf{Foo} + 1) + 1) + 1 \end{align}$

Remind you of something? From this expansion, we can see plainly that Foo is just a linked list!

So, in fact, we can derive a type that’s isomorphic to Haskell’s lists using Free:

> newtype FreeList a = FL { unFL :: Free ((,) a) () }

> nil :: FreeList a
> nil = FL $ Pure ()

> cons :: a -> FreeList a -> FreeList a
> x `cons` xs = FL $ Roll (x, unFL xs)

And of course, we can prove that FreeList is isomorphic to [] by providing a natural isomorphism (FreeList :<~>: []):¹

> data Bijection (~>) a b = Bi { biTo :: a ~> b, biFrom :: b ~> a }
> newtype f :~>: g = NT (forall a. f a -> g a)
> type f :<~>: g = Bijection (:~>:) f g

> listIsomorphism :: FreeList :<~>: []
> listIsomorphism = Bi (NT to) (NT fro)
>   where to (FL (Pure _))      = []
>         to (FL (Roll (x,xs))) = x : to (FL xs)
>         fro []     = nil
>         fro (x:xs) = x `cons` fro xs

Incidentally, the reason that FreeList can’t just be a type synonym rather than a newtype (and thus save us a bunch of explicit wrapping and unwrapping) is that Haskell won’t allow type synonyms to be partially applied, whereas type constructors can be. This is obviously necessary for producing a natural isomorphism.²

Please remember: if you find it useful to view free monads as a sort of generalized list, remember that the actual element type of that list is wrapped up in the functor f; that is, there is some bifunctor b for which f = b a, where a is your element type.

Indexing Free Monads: Vectors for Free

This is where it starts to get interesting. How could we go about encoding the depth of the functor roll in the type system? First, let’s start with the natural numbers (using GHC 7.4’s -XDataKinds extension, the following declaration creates a kind Nat with two constructors at the type level):

> data Nat = S Nat | Z

Our goal now is some data type IFree which behaves just like Free, but is depth-indexed by Nat. First, let’s start with a length-indexed vector and work our way up from there:

> data Vector (n :: Nat) (a :: *) where
>   VNil  :: Vector Z a
>   VCons :: a -> Vector n a -> Vector (S n) a

What is happening here is that the base case is indexed by zero, and VCons returns a vector of an index one higher than that of its input. Let’s see if we can generalize this to IFree:

> data IFree (n :: Nat) (f :: * -> *) (e :: *) where
>   IPure :: e -> IFree Z f e
>   IRoll :: f (IFree n f e) -> IFree (S n) f e

And so it should be trivial to derive a datatype isomorphic to Vector using IFree:

> newtype FreeVector n a = FV { unFV :: IFree n ((,) a) () }

> vnil :: FreeVector Z a
> vnil = FV $ IPure ()

> vcons :: a -> FreeVector n a -> FreeVector (S n) a
> x `vcons` xs = FV $ IRoll (x, unFV xs)

And, as we should hope, FreeVector n is isomorphic to Vector n:

> vectorIsomorphism :: FreeVector n :<~>: Vector n
> vectorIsomorphism = Bi (NT to) (NT fro)
>   where to :: FreeVector n a -> Vector n a
>         to (FV (IPure _))      = VNil
>         to (FV (IRoll (x,xs))) = x `VCons` to (FV xs)
>         fro :: Vector n a -> FreeVector n a
>         fro VNil           = vnil
>         fro (x `VCons` xs) = x `vcons` fro xs

Incidentally, the type-checker can’t properly infer the types of natural transformations to and fro.

Generalizations & Conclusions

So, free monads are a general way to derive many recursive data structures, which differ only in the way that data are linked together. Another interesting instantiation of the free monad would be the one that arises from the ((->) a) functor, which captures the idea of a function whose number of arguments may vary at runtime: as I will show in a later article, such a technique can be used for stream processing.

Indexed free monads, then, allow us to derive only such recursive data structures for which evaluation can reasonably be expected to terminate (I do not say guaranteed, since nothing is guaranteed in a non-total language like Haskell).