DEV Community

loading...
Cover image for Modeling asynchronous transactions with types — Part 2

Modeling asynchronous transactions with types — Part 2

mikesol profile image Mike Solomon ・7 min read

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
Enter fullscreen mode Exit fullscreen mode

but not

myprog = Ix.do
  void $ m2
  void $ m1
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

Here is a screenshot of the correct order.

Alt Text

Followed by the wrong order. The PS compiler tells VSCode to get angry, as it should!

Alt Text

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
Enter fullscreen mode Exit fullscreen mode

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

Alt Text

Alt Text

Alt Text

Alt Text

In the next example, the necessary ordering is broken.

Alt Text

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

Alt Text

In this way, row is a supercharged version of the canonical "product" (the Tuple) that has two advantages over vanilla tuples:

  1. They can be open, meaning we can ignore certain parts of the row and focus on others.
  2. 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
Enter fullscreen mode Exit fullscreen mode

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.

Alt Text

Alt Text

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

Alt Text

Alt Text

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.

Discussion (0)

pic
Editor guide