Modeling asynchronous transactions with types — Part 3

In the previous article, I discussed how indexed monads can leverage typelevel products and coproducts. This allowed us to leverage indices to structure complex asynchronous behavior. Products represent multiple simultaneous "forks" (or tracks, or lanes) and co-products act as joins, ie at the end of a transaction to do some sort of cleanup.

In this article, we'll consolidate this logic into a single state machine by using a typeclass.

Why state machines?

One of the trickiest aspects of typelevel programming is to know what parts of business logic to encode in types and what part to encode in plain old values. For example, consider the following bit of monadic code:

ticketPurchaser = do
  ticketId <- purchaseTicket
  sendTicketToClient ticketId

We can make it even more clear using the bind operator:

ticketPurchaser = purchaseTicket >>= sendTicketToClient

In this case, there is no indexed constraint, and it would be overkill to do so. Furthermore, even if there were an indexed monad that forced sendTicketToClient to happen directly after purchaseTicket, there is no way to indicate via indices that the output of a function must be consumed be another function. Meaning the following would be a perfectly legal, and perfectly incorrect, indexed program:

ticketPurchaser = Ix.do
  ticketId <- purchaseTicket
  sendTicketToClient "foo"

A different-but-related concept, called Substructural type systems, studies how often resources like ticketId can be consumed and by who. But realistically, constraining code to that degree is overkill: production and consumption of resources are rarely that tightly coupled, and when they are (ie writing to a log or analytics after every transaction), we tend to encode them in the internals of a monad, which means they happen "behind the scenes" of a monadic bind.

So indexed monads make the most sense when you want to enforce really important before/after relationships, and this is often the case when you have write-only logic that could theoretically happen in any order but, realistically, needs to happen in a certain order for it to make sense business-wise (ie writing "done" to a dashboard only if a certain request has not timed out). If the logic is that important, you don't want to scatter it all over your code base - you want those rules in one place. That is what a state machine is.

What is a state machine?

A state machine takes two inputs - a state and a payload, and returns a new state that may or may not have been updated in light of the payload.

myProgram :: Int -> M Int
myProgram input = do
  res1 <- stateMachine input
  res2 <- stateMachine (case res1 of
     Foo -> 0
     Bar -> 1)
  pure res2

On the typelevel, this works the same way.

foreign import kind StateInput

foreign import kind State

foreign import data Input1 :: StateInput

foreign import data Input2 :: StateInput

foreign import data State1 :: State

foreign import data State2 :: State

foreign import data State3 :: State

class StateMachine
  (input :: StateInput)
  (old :: StateMachine)
  (new :: StateMachine) | input old -> new

instance :: StateMachine Input1 State1 State2
instance :: StateMachine Input2 State1 State3
instance :: StateMachine Input1 State3 State1
instance :: StateMachine Input1 State2 State2

This state machine has a loop from State1 back to itself "jumping over" State2, and it has a sink at State2.

State machines in indexed monads

Let's see how a state machine can help consolidate the ad hoc logic from the previous article in a single typeclass called StateMachine.

module StateMachine where

import Prelude
import Control.Applicative.Indexed (class IxApplicative)
import Control.Apply.Indexed (class IxApply)
import Control.Bind.Indexed (class IxBind)
import Control.Monad.Indexed (class IxMonad)
import Control.Monad.Indexed.Qualified as Ix
import Data.Functor.Indexed (class IxFunctor)
import Data.Identity (Identity)
import Data.Newtype (class Newtype, unwrap)
import Prim.Row (class Cons)

newtype IdIxMo i o a
  = IdIxMo (Identity a)

derive instance newtypeIdIxMo :: Newtype (IdIxMo i o a) _

derive newtype instance freeProgramFunctor :: Functor (IdIxMo i o)

derive newtype instance freeProgramApply :: Apply (IdIxMo i o)

derive newtype instance freeProgramBind :: Bind (IdIxMo i o)

derive newtype instance freeProgramApplicative :: Applicative (IdIxMo i o)

derive newtype instance freeProgramMonad :: Monad (IdIxMo i o)

instance freeProgramIxFunctor :: IxFunctor IdIxMo where
  imap f (IdIxMo a) = IdIxMo (f <$> a)

instance freeProgramIxApplicative :: IxApply IdIxMo where
  iapply (IdIxMo f) (IdIxMo a) = IdIxMo (f <*> a)

instance freeProgramIxApply :: IxApplicative IdIxMo where
  ipure a = IdIxMo $ pure a

instance freeProgramIxBind :: IxBind IdIxMo where
  ibind (IdIxMo monad) function = IdIxMo (monad >>= (unwrap <<< function))

instance freeProgramIxMonad :: IxMonad IdIxMo

data Step1

data Step2

data Finished

class StateMachine input i o | input -> i o

data Track1Step1

data Track1Step2

data Track2Step1

data Track2Step2

instance track1Step1StateMachine :: (Cons "track1" Step1 prev rin, Cons "track1" Step2 prev rout) => StateMachine Track1Step1 { | rin } { | rout }

instance track1Step2StateMachine :: (Cons "track1" Step2 prev rin, Cons "track1" Finished prev rout) => StateMachine Track1Step2 { | rin } { | rout }

instance track2Step1StateMachine :: (Cons "track2" Step1 prev rin, Cons "track2" Step2 prev rout) => StateMachine Track2Step1 { | rin } { | rout }

instance track2Step2StateMachine :: (Cons "track2" Step2 prev rin, Cons "track2" Finished prev rout) => StateMachine Track2Step2 { | rin } { | rout }

track1Step1 :: forall i o. StateMachine Track1Step1 i o => IdIxMo i o Unit
track1Step1 = pure unit

track2Step1 :: forall i o. StateMachine Track2Step1 i o => IdIxMo i o Unit
track2Step1 = pure unit

track1Step2 :: forall i o. StateMachine Track1Step2 i o => IdIxMo i o Unit
track1Step2 = pure unit

track2Step2 :: forall i o. StateMachine Track2Step2 i o => IdIxMo i o Unit
track2Step2 = pure unit

myProg :: IdIxMo { track1 :: Step1, track2 :: Step1 } { track1 :: Finished, track2 :: Finished } Unit
myProg = Ix.do
  track1Step1
  track2Step1
  track1Step2
  track2Step2

While it's still possible to define functions that are not constrained by StateMachine, using a single state machine is a signal to colleagues and maintainers that all transitional logic of an indexed monad should be defined in a single spot.

In the next article, we'll colocate this transitional logic with the definition of the monad itself so that it's only ever possible to define monads with valid transitional states.