# 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**.

```
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
```

`module FiniteStateMachines where`

```
import Prelude hiding (id, foldMap, (.))
import Control.Category (Category (..), (<<<))
import Control.Monad ((>=>))
import Data.List.NonEmpty (NonEmpty (..), (<|))
import Data.Void (Void)
import Unsafe.Coerce (unsafeCoerce)
```

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

```
data Cat :: (* -> * -> *) -> * -> * -> * where
Id :: Cat f a a
(:.:) :: f b c -> Cat f a b -> Cat f a c
instance Category (Cat f) where
id = Id
Id . ys = ys
:.: xs) . ys = x :.: (xs . ys) (x
```

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 `Cat f`

.

For each `a`

we have an embedding:

```
endo :: [f a a] -> Cat f a a
= Id
endo [] : xs) = x :.: endo xs endo (x
```

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.

```
liftCat :: f a b -> Cat f a b
= fab :.: Id liftCat fab
```

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:

```
foldFunCat :: forall f g a b . Category g
=> (forall x y. f x y -> g x y)
-- ^ a map of graphs
-> (Cat f a b -> g a b)
-- ^ a functor from 'Cat f' to 'g'
Id = id
foldFunCat _ :.: ab)
foldFunCat fun (bc = fun bc <<< foldFunCat fun ab
```

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.

```
newtype Kleisli m a b =
Kleisli { runKleisli :: a -> m b }
instance Monad m => Category (Kleisli m) where
id = Kleisli return
Kleisli f . Kleisli g = Kleisli (g >=> f)
```

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

```
arr :: Monad m => (a -> b) -> Kleisli m a b
= Kleisli $ return . f arr f
```

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:

```
foldFunKleisli :: forall f m a b . Monad m
=> (forall x y. f x y -> Kleisli m x y)
-> (Cat f a b -> Kleisli m a b)
= foldFunCat foldFunKleisli
```

if you expand `Kleisli`

newtype wrapper we will get

```
foldFunKleisli' :: Monad m
=> (forall x y. f x y -> x -> m y)
-> Cat f a b
-> a -> m b
= runKleisli $ foldFunKleisli (Kleisli . fun) cab foldFunKleisli' fun cab
```

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:

```
data Endo c a where
Endo :: Category c => c a a -> Endo c a
instance Semigroup (Endo c a) where
Endo f <> Endo g = Endo (f <<< g)
instance Category c => Monoid (Endo c a) where
mempty = Endo id
```

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:

```
data Single e v a b where
Single :: e -> Single e v v v
VoidSingle :: Void -> Single e v a b
```

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`

):

```
toList :: Cat (Single e v) v v -> [e]
Id = []
toList Single e :.: es) = e : toList es
toList (VoidSingle e :.: _) = undefined toList (
```

Whenever `e`

is a `Monoid`

, `Single e v`

is a `Category`

:

```
idSingle :: Monoid e => Single e v v v
= Single mempty
idSingle
composeSingle :: Monoid e
=> Single e v b c
-> Single e v a b
-> Single e v a c
Single a) (Single b) = Single (a <> b)
composeSingle (VoidSingle _) _ = undefined
composeSingle (VoidSingle _) = undefined composeSingle _ (
```

```
instance Monoid e => Category (Single e v) where
id :: forall a . Monoid e => Single e v a a
id = unsafeCoerce (idSingle @e)
.) = composeSingle (
```

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 `foldMap`

:

```
foldMap :: Monoid m => (a -> m) -> [a] -> m
foldMap _ [] = mempty
foldMap f (a : as) = f a <> foldMap f as
```

First let us see how `foldFuncCat`

specializes:

```
_foldFunCat :: forall e f v a b .
Monoid e
=> (forall x y . f x y -> Single e v x y)
-> Cat f a b
-> Single e v a b
= foldFunCat _foldFunCat
```

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

```
foldFunCat' :: forall e f v.
Monoid e
=> (f v v -> Single e v v v) -- ≅ f v v -> e
-> Cat f v v -- ≅ [f v v]
-> Single e v v v -- ≅ e
= foldFunCat (unsafeCoerce f) c foldFunCat' f c
```

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

```
data NoItems = NoItems
newtype HasItems = HasItems (NonEmpty CartItem)
newtype NoCard = NoCard (NonEmpty CartItem)
data CardSelected = CardSelected Card (NonEmpty CartItem)
data CardConfirmed = CardConfirmed Card (NonEmpty CartItem)
data OrderPlaced = OrderPlaced
```

The shop only sells unit objects (better than seling `Void`

terms ;) )

`type CartItem = ()`

Accepted credit cards:

`type Card = String`

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

```
data Tr s t where
SelectFirst :: CartItem -> Tr NoItems HasItems
Select :: CartItem -> Tr HasItems HasItems
SelectCard :: Card -> Tr HasItems CardSelected
Confirm :: Tr CardSelected CardConfirmed
PlaceOrder :: Tr CardConfirmed OrderPlaced
Cancel :: Tr s NoItems
```

Category generated by the `Tr`

graph.

`type ShoppingCat a b = Cat Tr a b`

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:

```
natPure :: Tr a b -> a -> b
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 natPure
```

Interpretation of `ShoppingCat`

in `(->)`

(a functor between two categories):

```
checkoutPure :: ShoppingCat a b -> a -> b
= foldFunCat natPure checkoutPure
```

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.

```
checkoutM :: forall m a b . Monad m
=> ShoppingCat a b
-> Kleisli m a b
= foldFunCat nat
checkoutM where
nat :: Tr x y -> Kleisli m x y
= arr $ natPure xy nat xy
```

Unpacking the `Kleisli`

category gives us:

```
chechoutM' :: Monad m => ShoppingCat a b -> a -> m b
= runKleisli . checkoutM chechoutM'
```

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 (`IOException`

s …). 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:

```
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
= liftCat . SelectFirst
selectFirst = liftCat . Select
select = liftCat . SelectCard
selectCard = liftCat Confirm
confirm = liftCat PlaceOrder
placeOrder = liftCat Cancel 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 `ShoppingCatT`

category.

```
embed :: forall c a b. ShoppingCatT c
=> ShoppingCat a b
-> c a b
= foldFunCat nat
embed where
nat :: Tr x y -> c x y
SelectFirst i) = selectFirst i
nat (Select i) = select i
nat (SelectCard c) = selectCard c
nat (Confirm = confirm
nat PlaceOrder = placeOrder
nat Cancel = cancel nat
```

## 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:

```
foldMapKleisli :: Monad m
=> (e -> Kleisli m v v)
-> [e]
-> Kleisli m v v
= id
foldMapKleisli _ [] : es) = f e <<< foldMapKleisli f es foldMapKleisli f (e
```

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.