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

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module CategoriesWithMonadicEffects where

import           Prelude hiding (id, (.))

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

import           Test.QuickCheck

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 a b -> Cat f a b
  liftFree2 = (:.: Id)

  foldNatFree2 :: Category c
               => (forall x y. f x y -> c x y)
               -> Cat f a b
               -> c a b
  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:

instance EffCategory (->) Identity where
  lift = runIdentity

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

instance (Functor m, Category c) => EffCategory (FreeEffCat m c) m where
  lift = Lift

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 :: c a b
            -> FreeEffCat m c a b
  liftFree2    = Base

  foldNatFree2 :: ( Category f
                  , EffCategory c m
                  )
               => (forall x y. f x y -> c x y)
               -> FreeEffCat m f a b
               -> c a b
  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

runLoggedOut :: State 'LoggedOutType a -> Maybe a
runLoggedOut (LoggedOut a) = 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

type Username = String

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

  handleAccess = AccessHandler (pure "44") $
    \s -> do
      putStrLn ("secret: " ++ s)
      return LogoutHandler

  handleAccessDenied = putStrLn "AccessDenied"

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

  handleAccess = AccessHandler (pure secret) $ \_ -> return LogoutHandler

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