Modeling asynchronous transactions with types โ Part 2
Mike Solomon
Posted on February 26, 2021
In the previous article, I showed some examples of how complex transactional business logic can be encoded with a type system so that errors in building up transactions turn into red squiggles in an IDE. The pattern under the hood that makes this all possible is called an indexed monad.
In this article, we'll look at how to create products and co-products (rows and instances) in indexed types to represent aggregated outcomes (rows) and one of several different possible outcomes (instances).
Indexed monad - the basics
An indexed monad establishes a compiler-enforced before-after relationship between values in a monadic context. Its signature is m i o a, where m is the constructor, i is the input index, o is the output index and a is the value inside the monad.
If I have a value m1 = Moo Foo Bar String and a value m2 = Moo Bar Baz Boolean, m1 can be ibind-ed with m2 because the output type of m1, or Bar, is the same as the input type of m2, or Baz. Note that this i/o is not runtime i/o - it is compile-tile i/o. The types don't need to have a runtime representation, and they are strictly used to sequence monads at compile time. That means that we can do:
myprog = Ix.do
void $ m1
void $ m2
but not
myprog = Ix.do
void $ m2
void $ m1
Here is a minimum-viable-indexed monad program.
module IdIxMo1 where
import Prelude
import Control.Applicative.Indexed (class IxApplicative)
import Control.Apply.Indexed (class IxApply)
import Control.Monad.Indexed.Qualified as Ix
import Control.Bind.Indexed (class IxBind)
import Control.Monad.Indexed (class IxMonad)
import Data.Functor.Indexed (class IxFunctor)
import Data.Identity (Identity)
import Data.Newtype (class Newtype, unwrap)
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
doFirstThing :: IdIxMo Step1 Step2 Unit
doFirstThing = pure unit
doSecondThing :: IdIxMo Step2 Finished Unit
doSecondThing = pure unit
myProg :: IdIxMo Step1 Finished Unit
myProg = Ix.do
doFirstThing
doSecondThing
Here is a screenshot of the correct order.
Followed by the wrong order. The PS compiler tells VSCode to get angry, as it should!
Making products using rows
If indexed monads represent before/after relationships, it's often the case in asynchronous context that before/after happens in different "lanes". For example, a write operation followed by a verification operation may have nothing to do with a price-check operation followed by a logging operation, but both may need to happen before a final write saying "this transaction is done."
Rows are indexed heterogenous types that allow you to establish "tracks" or lanes where multiple simultaneous aspects of a transaction can coexist in the same type. Let's see how by modifying our example above.
module IdIxMo1 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
track1Step1 :: forall prev rin rout. Cons "track1" Step1 prev rin => Cons "track1" Step2 prev rout => IdIxMo { | rin } { | rout } Unit
track1Step1 = pure unit
track2Step1 :: forall prev rin rout. Cons "track2" Step1 prev rin => Cons "track2" Step2 prev rout => IdIxMo { | rin } { | rout } Unit
track2Step1 = pure unit
track1Step2 :: forall prev rin rout. Cons "track1" Step2 prev rin => Cons "track1" Finished prev rout => IdIxMo { | rin } { | rout } Unit
track1Step2 = pure unit
track2Step2 :: forall prev rin rout. Cons "track2" Step2 prev rin => Cons "track2" Finished prev rout => IdIxMo { | rin } { | rout } Unit
track2Step2 = pure unit
myProg :: IdIxMo { track1 :: Step1, track2 :: Step1 } { track1 :: Finished, track2 :: Finished } Unit
myProg = Ix.do
track1Step1
track2Step1
track1Step2
track2Step2
Let's see what happens in the IDE when we change the order a bit. The following four screenshots are all fine because they preserve the correct order of Step1 in "track1" before Step2 in "track1" and Step1 in "track2" before Step2 in "track2".
In the next example, the necessary ordering is broken.
Not only do we see where the error is, but it also points to exactly which "lane" is off ("track1"), what it received (Step2) and what it was expecting (Step1).
In this way, row is a supercharged version of the canonical "product" (the Tuple) that has two advantages over vanilla tuples:
- They can be open, meaning we can ignore certain parts of the row and focus on others.
- They are indexed by keys, allowing a lookup mechanism similar to dictionaries.
These properties of rows are asserted above using the Cons typeclass.
Making co-products using typeclass instances
If indices with products can be created using rows, what about co-products. Co-products are the dual of products and are traditionally represented by Either or by using Variants.
What would a co-product mean in the world of indices? To imagine this, a motivating example would help of a real-world use case. Imagine a function that does some sort of "cleanup" for several different indexed monads. How can we have one function that accepts several different input types?
One answer is typeclasses, where co-products are expressed as instances of a typeclass. Let's see how, again using the example above.
module IdIxMo3 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
track1Step1 :: forall prev rin rout. Cons "track1" Step1 prev rin => Cons "track1" Step2 prev rout => IdIxMo { | rin } { | rout } Unit
track1Step1 = pure unit
track2Step1 :: forall prev rin rout. Cons "track2" Step1 prev rin => Cons "track2" Step2 prev rout => IdIxMo { | rin } { | rout } Unit
track2Step1 = pure unit
track1Step2 :: forall prev rin rout. Cons "track1" Step2 prev rin => Cons "track1" Finished prev rout => IdIxMo { | rin } { | rout } Unit
track1Step2 = pure unit
track2Step2 :: forall prev rin rout. Cons "track2" Step2 prev rin => Cons "track2" Finished prev rout => IdIxMo { | rin } { | rout } Unit
track2Step2 = pure unit
class SetAtStart i where
setAtStart :: IdIxMo i { track1 :: Step1, track2 :: Step1 } Unit
data FromPlaceA
data FromPlaceB
data FromPlaceC
instance setAtStartFromPlaceA :: SetAtStart FromPlaceA where
setAtStart = pure unit
instance setAtStartFromPlaceB :: SetAtStart FromPlaceB where
setAtStart = pure unit
prog1 ::
forall setAtStart.
SetAtStart setAtStart =>
IdIxMo
setAtStart
{ track1 :: Finished, track2 :: Finished }
Unit
prog1 = Ix.do
setAtStart
track2Step1
track1Step1
track1Step2
track2Step2
prog2 ::
IdIxMo
FromPlaceA
{ track1 :: Finished, track2 :: Finished }
Unit
prog2 = prog1
In this example, the instances of SetAtStart are a typelevel case statement, and the use of setAtStart invokes the case at the top of Ix.do.
In VSCode, I can use FromPlaceA or FromPlaceB and the result is the same.
However, if I try to use FromPlaceC it gets angry and tells me there is no instance for typeclass SetAtStart (there is no appropriate "branch" in our variant).
Next step
Now that our asynchronous transactions are using typelevel products and co-products, the next thing we'd like to do is encode this logic in one place. In the example above, all of the logic is written ad hoc in function definitions, which means that the constraints can be established in any direction so long as you create the right function signature. It would be more convenient if we had a one-stop shop for transactional logic, and in the next article, I'll show you how to create a typelevel transition machine that acts as this central broker.
Posted on February 26, 2021
Join Our Newsletter. No Spam, Only the good stuff.
Sign up to receive the latest update from our blog.
Related
