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 :<~>: []):1

> 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.2

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.

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).

1. Just as a natural transformation is just a morphism in a category where the objects are functors, a natural isomorphism is a bijection in that category. In combination with GHC’s -XPolyKinds extension, our Bijection type can be used to represent bijections in any category by taking as its first parameter the hom-set of that category (the type of morphisms between objects). So, Bijection (->) is a pair of functions that convert back and forth between data types, whereas Bijection (:~>:) is a pair of natural transformations that convert back and forth between functors.

2. This is also the reason that (:~>:) must be a type constructor rather than a type synonym, namely that we need to use it in its unapplied state as the hom-set for our bijection.

# Want to comment?

I’m @jonsterling on Twitter and App.net.