Categories with Monadic Effects and State Machines

In this posts we will present categories which can run monadic actions, which we call categories with monadic effects (abr. EffCategories). It turns out that one can build them in an abstract way, much the same way as free monads, and use them to specify state machines in a succinct and type-safe manner.

Most of the abstractions presented in this blog posts are included in the following Hackage packages:

Though this posts is self contained, you might want to first read my earlier posts on finite state machines and categories.

Free categories

Cat is a free category generated by a transition graph, which itself is represented as a type of kind k -> k -> Type. Since a graph does not have identity morphisms and lacks composition, the Cat constructors fill in the gap. Note that there are other representations of free categories, but this one is the most straightforward to work with. But if you need a condensity transformed version check out free-category package.

Category instance for Cat f is straightforward:

Cat is a free construction, this means that we can

These two propositions are proven by the following instance. liftFree2 gives us the embedding and foldNatFree2 transforms graph morphisms into functors.

Let us check that foldNatFree2 indeed preserves identity morphisms and composition. The first one is obvious, since this is how we defined foldNatFree2, so we are only left with the former claim. We need to consider two cases, following the definition on composition in Cat f.

foldNatFree2 f (Id . ys)
  = foldNatFree2 f ys      -- since `Id` is an identity
  = id . foldNatFree2 f ys -- since `id` is an identity
  = foldNatFree2 f Id . foldNatFree2 ys -- by definition of `foldNatFree`

and

foldNatFree2 f ((x :.: xs) . ys)
  -- by definition of multiplication in `Cat f`
  = foldNatFree f (x :.: (xs . yx))
  -- by definition of `foldNatFree2` 
  = f x . foldNatFree2 f (xs . yx)
  -- by induction hypothesis
  = f x . ((foldNatFree2 f xs) . foldNatFree f ys))
  -- by associativy of composition
  = (f x . foldNatFree2 f xs) . foldNatFree f ys
  -- by definition of `foldNatFree2`
  = foldNatFree2 f (x :.: xs) . foldNatFree f ys

Categories with monadic effects

Since Haskell is bound to monadic IO, if we want to represent a state machine that runs IO actions, we need a way to run monadic computations in the context of categorical composition. The following class is an attempt to give access to both:

We start with two basic instances. First the pure one:

And another very useful in our context, which is the prototypical example of EffCategory.

We can actually define a category of EffCategories, in which objects are categories with monadic effects, while morphisms are functors f :: c a b -> c' a b which satisfy the following property:

f (lift mcab) = lift $ f <$> mcab

You can even define a 2-Category, where natural transformations play the role of 1-morphisms (like the category of categories is defined), but this goes beyond this post.

Free monads are very successful to represent DSLs in an abstract way, and we’d like to have an analog way for building categories with monadic effects. The following definition gives us a free construction of such a category.

It is build abstractly, and its semantics / interpretation is free to be defined in any category with effects, e.g. the pure -> or in Kleisli IO or in any other category with effects (in the same monad).

Let us first prove that FreeEffCat is a category, under the assumption that m is a functor and c is a category:

The EffCategory instance is trivial (which is not a coincidence, this is a common pattern across many free constructions; check out instances in free-algebras):

Since a free object requires two operations: the embedding of the original structure plus the required operations (in this case just lift), FreeEffCat has two constructors which corresponds to these two operations. With this we can build an instance which proves that FreeEffCat is indeed a free category with effects.

There is one law that we need to prove, that foldNatFree2 is a morphism between categories with monadic effects, i.e.

foldNatFree2 nat (lift mab) = lift $ foldNatFree2 nat <$> mab

And as you can see it is a straightforward consequence of the definition:

foldNatFree2 nat (lift mcab)
  -- by definition of `lift` in `FreeEffCat`
  = foldNatFree2 nat (Lift mcab)
  -- by definition of `foldNatFree2`
  = lift $ foldNatFree2 nat <$> mcab

You can see that it’s actually the only way that foldNatFree2 could be defined so that it satisfies this property.

This is enough of abstract constructions, now’s the time to make some concrete usage, and a good point for a break and a walk to digest the contents.

Example state machine

The following example is based on: State Machines All The Way Down by Edwin Brady, youtube The idea is to define a state machine for a logging system, with a strong type properties: let the type checker prove that only logged in user have access to secret data.

StateType is a promoted kind with two types. It represents two possible states of the login system: logged in or logged out.

We also define singletons for these promoted types to be able reason about the types on the term level. In Idris, Edwin Brady, could define all the needed machinery on the type level, thanks to stronger type system.

We will also need term level representation of states. LoggedOut will let us carry out a value which we gained access to when we were logged in. This is a design choice that we want to leak the secret out of the safe zone.

Next we define a graph of transitions in the state machine.

Data representation of the state machine.

Let us build now a data type representation of the state machine. It is good to have an unsafe representation, and we should be able to map it into the safe one. We build a recursive representation of how the state machine can evolve.

For login we need a handler that returns either

Upon a successful login, we should be able to access the secret data, AccessHandler is contains an action to get the data (e.g. read it from disc or a database, likely some IO operation) and a handler which let us use it in some way. We should be able to logout from the system and for that we have a second constructor.

An example HandleLogin, which protects the secret with a simple password.

Pure HandleLogin, which is very useful for testing (e.g. accessSecret function).

Type safe representation

Abstract access function, which takes any HandleLogin representation and maps it into our type safe state machine. Note that the result is guaranteed, by the type system, to have access to the secret only after a successful login.

Get data following the protocol defined by the state machine.

Note: in GHC-8.6.1 we’d need MonadFail which prevents from running this in Identity monad. To avoid this we use the runLoggedOut function.

Interpreters

To write an interpreter it is enough to supply a natural transformation from Tr a from to to Kleisli m for some monad m.

A pure natural transformation from Tr to Kleisli m for some Monad m. Note, that even though Kleisli category seems redundant here, as we don’t use the monad in the transformation, we need a transformation into a category that satisfies the EffCategory constraint. This is because we will need the monad when foldNatLift will walk over the constructors of the FreeEffCat category.

We can capture a QuickCheck property of getData and run it in a pure setting, thanks to EffCategory instance for -> and the Identity functor.

Putting this all together we get a simple program:

When one executes this program one will get:

Provide a password:
test
Provide a password:
password
secret: 44