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

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
```

```
import Data.Kind (Type)
import Control.Arrow (Kleisli (..))
import Control.Category (Category (..))
import Control.Monad (void)
import Numeric.Natural (Natural)
import Data.Functor (($>))
import Data.Functor.Identity (Identity (..))
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
```

```
import Control.Algebra.Free (AlgebraType, AlgebraType0, proof)
import Control.Algebra.Free2 (FreeAlgebra2 (..))
```

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

```
data Cat :: (k -> k -> Type) -> k -> k -> Type where
Id :: Cat f a a
(:.:) :: f b c -> Cat f a b -> Cat f a c
```

Category instance for `Cat f`

is straightforward:

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

`Cat`

is a free construction, this means that we can

- embed the original graph
`f`

into`Cat f`

and - every graph morphisms, e.g. a morphism of type
`forall x y. f x y -> c x y`

can be extended uniquely to a functor from the category`Cat f`

to the category`c`

, i.e. a graph morphism which preserves identity arrows and composition.

These two propositions are proven by the following instance. `liftFree2`

gives us the embedding and `foldNatFree2`

transforms graph morphisms into functors.

```
type instance AlgebraType0 Cat f = ()
type instance AlgebraType Cat c = Category c
instance FreeAlgebra2 Cat where
liftFree2 :: f x y -> Cat f x y
liftFree2 = (:.: Id)
foldNatFree2 :: Category c
=> (forall x y. f x y -> c x y)
-> Cat f x y
-> c x y
foldNatFree2 _ Id = id
foldNatFree2 fun (bc :.: ab) = fun bc . foldNatFree2 fun ab
codom2 = proof
forget2 = proof
```

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:

- monadic (onion like) composition
- categorical (sequential) composition

```
-- | Categories which can lift monadic actions, i.e. categories
-- with monadic effects.
--
class Category c => EffCategory c m | c -> m where
lift :: m (c a b) -> c a b
```

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

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

.

```
instance Monad m => EffCategory (Kleisli m) m where
lift m = Kleisli (\a -> m >>= \(Kleisli f) -> f a)
```

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

```
-- | Category transformer, which adds @'EffCategory'@ instance to the
-- underlying base category.
--
data FreeEffCat
:: (Type -> Type)
-> (k -> k -> Type)
-> (k -> k -> Type)
where
Base :: c a b -> FreeEffCat m c a b
Lift :: m (FreeEffCat m c a b) -> FreeEffCat m c a b
```

Let us first prove that `FreeEffCat`

is a category, under the assumption that `m`

is a functor and `c`

is a category:

```
instance (Functor m, Category c) => Category (FreeEffCat m c) where
id = Base id
Base f . Base g = Base $ f . g
f . Lift mg = Lift $ (f .) <$> mg
Lift mf . g = Lift $ (. g) <$> mf
```

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.

```
type instance AlgebraType0 (FreeEffCat m) c = (Monad m, Category c)
type instance AlgebraType (FreeEffCat m) c = EffCategory c m
instance Monad m => FreeAlgebra2 (FreeEffCat m) where
liftFree2 :: Category c
=> c x y
-> FreeEffCat m c x y
liftFree2 = Base
foldNatFree2 :: ( Category f
, EffCategory c m
)
=> (forall x y. f x y -> c x y)
-> FreeEffCat m f x y
-> c x y
foldNatFree2 nat (Base cab) = nat cab
foldNatFree2 nat (Lift mcab) = lift $ foldNatFree2 nat <$> mcab
codom2 = proof
forget2 = proof
```

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.

```
-- | Wrap a transition into a free category @'Cat'@ and then in
-- @'FreeEffCat'@
--
-- prop> liftCat tr = Base (tr :.: Id)
--
liftCat :: Monad m => tr a b -> FreeEffCat m (Cat tr) a b
liftCat = liftFree2 . liftFree2
```

```
-- | Fold @'FreeEffCat'@ category based on a free category @'Cat' tr@
-- using a functor @tr x y -> c x y@.
--
foldNatLift
:: (Monad m, EffCategory c m)
=> (forall x y. tr x y -> c x y)
-> FreeEffCat m (Cat tr) a b
-> c a b
foldNatLift nat = foldNatFree2 (foldNatFree2 nat)
```

```
-- | Functor from @'->'@ category to @'Kleisli' m@. If @m@ is @Identity@
-- then it will respect @'lift'@ i.e.
-- @liftKleisli (lift ar) = lift (liftKleisli <$> -- ar).
--
liftKleisli :: Applicative m => (a -> b) -> Kleisli m a b
liftKleisli f = Kleisli (pure . f)
```

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.

```
-- | Type level representation of the states.
--
data StateType where
LoggedInType :: StateType
LoggedOutType :: StateType
```

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.

```
data SStateType (a :: StateType) where
SLoggedIn :: SStateType 'LoggedInType
SLoggedOut :: SStateType 'LoggedOutType
```

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.

```
data State (st :: StateType) a where
LoggedIn :: State 'LoggedInType a
LoggedOut :: Maybe a -> State 'LoggedOutType a
```

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

```
data Tr a from to where
Login :: SStateType to
-> Tr a (State 'LoggedOutType a) (State to a)
Logout :: Maybe a
-> Tr a (State 'LoggedInType a) (State 'LoggedOutType a)
Access :: Tr a (State 'LoggedInType a) (State 'LoggedInType a)
```

```
login :: Monad m
=> SStateType st
-> FreeEffCat m (Cat (Tr a))
(State 'LoggedOutType a)
(State st a)
login = liftCat . Login
```

```
logout :: Monad m
=> Maybe a
-> FreeEffCat m (Cat (Tr a))
(State 'LoggedInType a)
(State 'LoggedOutType a)
logout = liftCat . Logout
```

```
access :: Monad m
=> FreeEffCat m (Cat (Tr a))
(State 'LoggedInType a)
(State 'LoggedInType a)
access = liftCat Access
```

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

- it self, in case of login failure; so that one can retry
- or a success handler
`HandleAccess`

.

```
data HandleLogin m authtoken a = HandleLogin {
handleLogin
:: m (Either (HandleLogin m authtoken a) (HandleAccess m a)),
-- ^ either failure with a login continuation or handle access
-- to the secret data
handleAccessDenied
:: m ()
-- ^ handle access denied
}
```

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.

```
data HandleAccess m a where
AccessHandler
:: m a -- access secret
-> (a -> m (HandleAccess m a)) -- handle secret
-> HandleAccess m a
LogoutHandler :: HandleAccess m a -- logout
```

An example `HandleLogin`

, which protects the secret with a simple password.

```
handleLoginIO
:: String
-> HandleLogin IO String String
handleLoginIO passwd = HandleLogin
{ handleLogin
, handleAccessDenied
}
where
handleLogin = do
passwd' <- putStrLn "Provide a password:" >> getLine
if passwd' == passwd
then return $ Right handleAccess
else return $ Left $ handleLoginIO passwd
```

Pure `HandleLogin`

, which is very useful for testing (e.g. `accessSecret`

function).

```
handleLoginPure
:: NonEmpty String -- ^ passwords to try (cyclically, ad infinitum)
-> String -- ^ auth token
-> String -- ^ secret
-> HandleLogin Identity String String
handleLoginPure passwds passwd secret = HandleLogin
{ handleLogin = handleLogin passwds
, handleAccessDenied = pure ()
}
where
handleLogin (passwd' :| rest) =
if passwd' == passwd
then return $ Right handleAccess
else case rest of
[] -> return $ Left $ handleLoginPure passwds passwd secret
_ -> return $ Left $ handleLoginPure (NE.fromList rest) passwd secret
```

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

```
accessSecret
:: forall m a . Monad m
=> Natural
-- ^ how many times one can try to login; this could be
-- implemented inside `HandleLogin` (with a small
-- modifications) but this way we are able to test it
-- with a pure `HandleLogin` (see `handleLoginPure`).
-> HandleLogin m String a
-> FreeEffCat m (Cat (Tr a))
(State 'LoggedOutType a)
(State 'LoggedOutType a)
accessSecret 0 HandleLogin{handleAccessDenied} =
lift $ handleAccessDenied $> id
accessSecret n HandleLogin{handleLogin} = lift $ do
st <- handleLogin
case st of
-- login success
Right accessHandler
-> return $ handle accessHandler Nothing . login SLoggedIn
-- login failure
Left handler'
-> return $ accessSecret (pred n) handler'
where
handle :: HandleAccess m a
-> Maybe a
-> FreeEffCat m (Cat (Tr a))
(State 'LoggedInType a)
(State 'LoggedOutType a)
handle LogoutHandler ma = logout ma
handle (AccessHandler accessHandler dataHandler) _ = lift $ do
a <- accessHandler
accessHandler' <- dataHandler a
return $ handle accessHandler' (Just a)
```

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.

```
getData
:: forall m a . Monad m
=> (forall x y. Tr a x y -> Kleisli m x y)
-> Natural
-> HandleLogin m String a
-> m (Maybe a)
getData nat n handleLogin =
case foldNatLift nat (accessSecret n handleLogin) of
Kleisli fn ->
runLoggedOut <$> fn (LoggedOut Nothing)
```

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

```
natPure :: forall m a from to.
Monad m
=> Tr a from to
-> Kleisli m from to
natPure = liftKleisli . nat
where
-- a natural transformation to @'->'@
nat :: Tr a from to -> (from -> to)
nat (Login SLoggedIn) = \_ -> LoggedIn
nat (Login SLoggedOut) = \_ -> LoggedOut Nothing
nat (Logout ma) = \_ -> LoggedOut ma
nat Access = \_ -> LoggedIn
```

We can capture a QuickCheck property of `getData`

and run it in a pure setting, thanks to `EffCategory`

instance for `->`

and the `Identity`

functor.

```
prop_getData
:: NonEmptyList String
-> String
-> String
-> Positive Int
-> Property
prop_getData (NonEmpty passwds) passwd secret (Positive n)=
let res = runIdentity
$ getData natPure
(fromIntegral n)
(handleLoginPure (NE.fromList passwds) passwd secret)
in if passwd `elem` take n passwds
then res === Just secret
else res === Nothing
```

Putting this all together we get a simple program:

```
main :: IO ()
main = do
putStrLn ""
quickCheck prop_getData
putStrLn ""
void $ getData natPure 3 (handleLoginIO "password")
```

When one executes this program one will get:

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