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
* 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))).
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
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
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.
(>=>) :: (a -> m b) -> (b -> m c) -> a -> m c (f >=> g) a = f a >>= g
is called Kleisli composition (or if you prefer using
\f g a -> join $ fmap g (f a)). Monadic operations
>>= 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
(->) we have
Data.Monoid.Endo newtype wrapper for that purpose, and it could be generalised:
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:
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):
e is a
Single e v is a
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.
We will show now that
foldFunCat in this case is nothing than a
First let us see how
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
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
foldFunCat are defined using the same recursion pattern, hence they must be equal.
To recap what we have just show:
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
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
SelectFirst followed by
Select is a new edge from
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
natPure :: Tr a b -> a -> b natPure (SelectFirst i) _ = HasItems (i :| ) natPure (Select i) (HasItems is) = HasItems (i <| is) natPure (SelectCard c) (HasItems is) = CardSelected c is natPure Confirm (CardSelected c is) = CardConfirmed c is natPure PlaceOrder _ = OrderPlaced natPure Cancel _ = NoItems
(->) (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
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
class Category c => ShoppingCatT (c :: * -> * -> *) where selectFirst :: CartItem -> c NoItems HasItems select :: CartItem -> c HasItems HasItems selectCard :: Card -> c HasItems CardSelected confirm :: c CardSelected CardConfirmed placeOrder :: c CardConfirmed OrderPlaced cancel :: c s NoItems instance ShoppingCatT (Cat Tr) where selectFirst = liftCat . SelectFirst select = liftCat . Select selectCard = liftCat . SelectCard confirm = liftCat Confirm placeOrder = liftCat PlaceOrder cancel = liftCat Cancel
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
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 represents the type of events and use the following version of
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
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
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.