Typed Transitions, Finite State Machines and Free Categories

In this post we will explore finite state machines with typed transitions represented as finite directed graphs via free categories. You will also see how usefull is the Kleisli category.

Free Category Construction

A free category generated by a (directed) graph is formed by adding identity edges to each vertex and then taking the graph of all possible paths, i.e every path in this graph, becomes arrow in the generated category. The final step is to impose category theory laws: so that the added identity arrows satisfy the unit law. Path composition is always associative, so at least this we get for free. Composition of arrows is just composition of paths. Note that this construction correponds exactly to the construction of the free monoid: if you take a graph with a single vertex * and a bunch of edges from * to * then the free monoid generated by this set of edges is the same as the free category (every monoid can be seen as a category with a single object).

Let us check that the category theory laws holds. First let us observe that by recursive definition of Cat, every element has a form: (f1 :.: (f2 :.: ( ... :.: Id))).

normal form of a morphism in Cat f
normal form of a morphism in Cat f

The smallest n such that a morphism has this form we call the length of a morphism.

First unit law: Id . x = x holds by definition; to show x . Id = x, it’s enough to consider the case when x has length greater than 1:

(x :.: xs) . Id
   == x :.: (xs . Id)
   -- by induction on the length of xs
   == x :.: xs

Now let us prove associativity. The proof is also by induction on the length of the first element:

((x :.: Id) . y) . z
  == (x :.: y) . z
  == (x :.: (y . z))
  == (x :.: (Id . (y . z))
  == (x :.: Id) . (y . z)

And the induction step:

((x :.: xs) . y) . z
  == (x :.: (xs . y)) . z
  ==  x :.: ((xs . y) . z)
  -- by induction on the length of xs
  ==  x :.: (xs . (y . z))
  ==  (x :.: xs) . (y . z)

As expected we have a lawful category Cat f.

For each a we have an embedding:

As all the free constructions, also free category has the lift operation which let you embed the generating graph into the free category generated by it. It is a generalisation of the singleton list

(: []) :: a -> [a]

and at the same time lift for monad transformers.

Being a free category means that whenever you have a binatural transformation from f :: * -> * -> * to a category Category g => g :: * -> * -> * you can construct (in a unique way) a functor from Cat f to g. This is the spirit of free algebras. And indeed we can get a foldMap like map:

This is a free constructions in the sense I’ve been advocating for some time in a series of blog posts: from free algebras to free monads, monadicity, based on free-algebras package (published on hackage).

The Kleisli Category

in Control.Arrow there is the following construction, which is attributed to a Swiss category theorist Heinrich Kleisli. It turns out that with any moand m one can associate a category where arrows are a -> m b instead of a -> b. Let us investigate this in detail, as this allows for many interesting interpretations.

The arrow

(>=>) :: (a -> m b) -> (b -> m c) -> a -> m c
(f >=> g) a = f a >>= g

is called Kleisli composition (or if you prefer using join: \f g a -> join $ fmap g (f a)). Monadic operations return and >>= carry the unitality laws:

return >>= f == f
m >>= return == m

They become even simpler when we re-write them using >=>:

return >=> f == f
f >=> return == f

This means that Kleisli return is indeed the identity arrow in Kleisli m category. It remain to show that the composition is associative, and this, as you can expect, can be derived from the monad associativity law:

m >>= (\x -> k x >>= h)
  == (m >>= k) >>= k)

which using Kleisli composition, takes much simpler form (which conveys the reason for the name of this axiom):

f >=> (g >=> h) == (f >=> g) >=> h

Let us prove this:

(f >=> (g >=> h)) a 
  == f a >>= (g >=> h)
  == f a >>= \b -> g b >>= h)
  -- by monadic associativity law
  == (f a >>= g) >>= h
  == ((f >=> g) a) >>= h
  == ((f >=> g) >=> h) a

The associativity of Kleisli composition >=> is exactly what we need to prove associativity of Kleisli m category, so we’re done! This is the one of rare cases when using point free style makes the presentation look much easier to read ;).

Also note that there is a functor from (->) category to Kleisli m given by

It is a part of the Monad m => Arrow (Kleisli m) instance in Control.Arrow module of the base package.

There is a worth noting sepcialization of foldFunCat to Kleisli category:

if you expand Kleisli newtype wrapper we will get

A final observation, is that in any category the type cat c => c v v is a monoid with identity id and multiplication (.). In (->) we have Data.Monoid.Endo newtype wrapper for that purpose, and it could be generalised:

This includes Endo (Kleisli m) a ≅ a -> m a as an example (for a monad m). If you try to prove the associativity and unit laws for this monoid, you’ll discover that what you need is associativity and unit laws for monad.

Example: bifunctor with a single object

As an example let us consder a bifunctor with a single object:

With Single you can only construct terms of type Single e v v v, any other term diverge. We need VoidSingle constructor to provide a Category type class instance.

In this case endo is an isomorphism with inverse (modulo Single e v v v ≅ e):

Whenever e is a Monoid, Single e v is a Category:

Furthemore, in this case the free category corresponds to free monoid; Cat (Single e v) is a single object category with

Cat (Single e v) v v ≅ [e]

the free monoid generated on type Single e v v v ≅ e.

category (Cat (Single e v)) with one object v
category (Cat (Single e v)) with one object v

We will show now that foldFunCat in this case is nothing than a foldMap:

First let us see how foldFuncCat specializes:

now note that the only natural transformation f x y -> Single e v x y that we can have are one that comes from a map g :: f v v -> Single e v v v. Hence foldFunCat reduces further to to

Assuming that endo :: f v v -> Cat f v v is an isomorphism (which it is for a large class of bifunctors, e.g. Single e v) we have: Cat f v v ≅ [v]; so we end up with a map Monoid m => (a -> m) -> [a] -> m which is the claimed foldMap. Finally, both foldMap and foldFunCat are defined using the same recursion pattern, hence they must be equal.

To recap what we have just show: foldFunCat for f = Single e v and g = Monoid m => Single e v is just foldMap. In this case we can view foldFunCat as a generalisation foldMap. There is also another way of coming to this conclusin via free objects (check out free-algebras package.

Example Finite State Machine

For this post I picked the example of a state machine explored by Oscar Wickström in his short series about state machines: part 1 and part 2. It is a simple state transition for an online shop. I slightly simplified it, by making the assumption that one can cancel at any stage (just for presentation purposes).

States (vertices of the FSM):

The shop only sells unit objects (better than seling Void terms ;) )

Accepted credit cards:

The FTM’s directed graph can be described by a type of kind * -> * -> *, where first type is the source of an arrow, the second type is its target. Directed graph lack composition, and we will fix this. In this example we take (after Oscar Wickström, though here Cancel can abort at any stage rather than just during confirmation, just for simplicity):

Category generated by the Tr graph.

Tr graph
Tr graph

As a graph ShoppingCat has the same vertices as Tr, but has more edges. Any path that you can follow in the Tr graph becomes a new edge in ShoppingCat, e.g. SelectFirst followed by Select is a new edge from NoItems to HasItems. Note that at this point we don’t have any interpretation of the arrows, we only modeled the shape of the category we want to have. This gives us freedom how to interpret this category in other categories using functors (not to confuse with Functor instances: these are endofunctors of (->)).

Interpretation of the Tr graph in the (->) category:

Interpretation of ShoppingCat in (->) (a functor between two categories):

But we can easily interpret in ShoppingCat in any Kleisli category, especially in Klesli IO. Here we lift just the pure interpretation, but equaly well you could do some IO here.

Unpacking the Kleisli category gives us:

The freedom of the choice of monad in the Kleisli category can give you various ways of dealing with exceptional conditions (e.g. not valid card) and error handling (IOExceptions …). Also having various interpretation can be very good for testing, e.g. having a reference implementation might be a very good idea to increase assurance of the software you are developing. Check out Duncan Coutts’ lecture on this technique.

Finally tagless description

We can give a finally tagless description of the shopping category. For that we first define the class of categories in which one can do all the Tr operations:

There is a unique functor embed :: ShopingCatT c => ShoppingCat a b -> c a b which with preserves all the operations, e.g.

embed (SelectFirst i) = selectFirst i 
embed (Select i)      = select i
embed (SelectCard v)  = selectCard v
embed Confirm         = confirm
embed PlaceOrder      = placeOrder
embed Cancel          = cancel

This property does not leave any space how this functor has to be implemented, that’s why ShoppingCat is the initial ShoppingCatT category.

Complete graph with a single vertex

Let us go back to the Single e v graph.

A graph is complete if every two vertices are connected by a unique edge. It may also happen that all the vertices can be represented by a single type a. Then the whole theory collapses to a category with a single object, i.e. a monoid (as we discovered earlier for the Single e v graph). In this case the generating graph can also be reduced to just a single type (usually a sum of all possible events). In this case one can describe the state machine simply by a free monoid [e] where e represents the type of events and use the following version of foldMapKleisli (foldFunCat) to give interpretations:

The first argument of foldMapKleisli maps events to (monadic) state transformations. You can model pure transformations with Kleisli Identity (Kleisli Identity a v ≅ v -> v), or you might want to use IO with Kleisli IO (Kleisli IO v v ≅ v -> IO v).

And again, what you are seeing here is foldMap, this is simply because Kleisli m v v is a monoid (as every type Category c => cat a a is). The composition is given by <<< and mempty is the identity arrow id, so the above formula corresponds to foldMap. This is the very special case if your state machine can be represented as a single object category, i.e. a monoid.