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.
Top comments (0)