In the previous article in this series, we saw how to use a transition machine to consolidate transitional logic between indexed monads in one place. In this final article, we'll look at how these transitions can be built directly into the construction of the monad itself via free monads.

What are free monads?

Free monads are a way to define a monad using an ADT. You write the program's logic using the ADT and execute the logic in a monadic context. This has the advantage of decoupling logic and execution, which is useful in testing and in code reuse.

Here are some great online tutorials and discussions on how to use free monads:

Free monads have the additional advantage of allowing us to define a lexicon of indices as "part" of the monad in the same way that branches of an ADT define different actions that can be executed in the monaidc context.

Constructing free monads using state machines as indexed types

Let's go back to the two original examples from the first article - an S3 uploader and a price comparitor.

In both examples, a single function toIndexed processes the ADTs, turning them into indexed monads where their I/O is defined
by a typelevel state machine. They're a bit longer than the previous examples because I've copied a helper class ToIndexed into them. In our production code, we have ToIndexed in a separate file for reusability purposes.

S3 uploader

module FunTimesWithS3 where

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

data UploadAssetToS3I
  = UploadAssetToS3I

data PersistS3LocationToDBI
  = PersistS3LocationToDBI

instance semigroupPersistS3LocationToDBI :: Semigroup PersistS3LocationToDBI where
  append a b = b

instance monoidPersistS3LocationToDBI :: Monoid PersistS3LocationToDBI where
  mempty = PersistS3LocationToDBI

instance semigroupUploadAssetToS3I :: Semigroup UploadAssetToS3I where
  append a b = b

instance monoidUploadAssetToS3I :: Monoid UploadAssetToS3I where
  mempty = UploadAssetToS3I

data Yup
  = Yup

instance semigroupYup :: Semigroup Yup where
  append a b = b

instance monoidYup :: Monoid Yup where
  mempty = Yup

class StateMachine (ii :: Type) (i :: Type) (o :: Type) | ii i -> o

instance indexIndexUploadAssetToS3I :: (Cons "uploadAssetToS3" Yup rin rout) => StateMachine UploadAssetToS3I { | rin } { | rout }

instance indexIndexPersistS3LocationToDBI :: (Cons "uploadAssetToS3" Yup prev rin, Cons "persistS3LocationToDB" Yup rin rout) => StateMachine PersistS3LocationToDBI { | rin } { | rout }

data Program a
  = UploadAssetToS3 UploadAssetToS3I String String (Unit -> a)
  | PersistS3LocationToDB PersistS3LocationToDBI String String String (Unit -> a)

newtype IndexedProgram i o a
  = IndexedProgram (Free Program a)

derive instance newtypeIndexedProgram :: Newtype (IndexedProgram i o a) _

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

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

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

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

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

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

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

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

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

instance freeProgramIxMonad :: IxMonad IndexedProgram

type IndexedNaturalTransformation
  = forall f m i o. i -> o -> (forall a. f a -> m i o a)

newtype NIT f m i o
  = NIT (forall a. f a -> m i o a)

class ToIndexed ntrans a b | a -> b, b -> a where
  toIndexed :: ntrans -> a -> b

instance ti0 :: (Monoid ii, Monoid i, Monoid o, StateMachine ii i o) => ToIndexed (NIT f m i o) (ii -> (b -> b) -> f b) (m i o b) where
  toIndexed (NIT f) ctr = f (ctr mempty identity)
else instance ti1 :: (Monoid ii, Monoid i, Monoid o, StateMachine ii i o) => ToIndexed (NIT f m i o) (ii -> y -> (b -> b) -> f b) (y -> m i o b) where
  toIndexed (NIT f) ctr y = f (ctr mempty y identity)
else instance ti2 :: (Monoid ii, Monoid i, Monoid o, StateMachine ii i o) => ToIndexed (NIT f m i o) (ii -> x -> y -> (b -> b) -> f b) (x -> y -> m i o b) where
  toIndexed (NIT f) ctr x y = f (ctr mempty x y identity)
else instance ti3 :: (Monoid ii, Monoid i, Monoid o, StateMachine ii i o) => ToIndexed (NIT f m i o) (ii -> w -> x -> y -> (b -> b) -> f b) (w -> x -> y -> m i o b) where
  toIndexed (NIT f) ctr w x y = f (ctr mempty w x y identity)

uploadAssetToS3 = toIndexed (NIT (IndexedProgram <<< liftF)) UploadAssetToS3

persistS3LocationToDB = toIndexed (NIT (IndexedProgram <<< liftF)) PersistS3LocationToDB

prog ::
  String ->
  String ->
  String ->
  IndexedProgram
    (Record ())
    ( Record
        ( "uploadAssetToS3" :: Yup
        , "persistS3LocationToDB" :: Yup
        )
    )
    Unit
prog assetId bucket key = Ix.do
  uploadAssetToS3 bucket key
  persistS3LocationToDB assetId bucket key

Price comparitor

module PriceComparitor where

import Prelude
import Control.Applicative.Indexed (class IxApplicative, class IxApply, ipure)
import Control.Bind.Indexed (class IxBind)
import Control.Monad.Free (Free, liftF)
import Control.Monad.Indexed (class IxMonad)
import Control.Monad.Indexed.Qualified as Ix
import Data.Functor.Indexed (class IxFunctor)
import Data.Newtype (class Newtype, unwrap)
import Data.Traversable (sequence)
import Prim.Row (class Cons)

data CheckVendor1I
  = CheckVendor1I

data CheckVendor2I
  = CheckVendor2I

data CheckVendor3I
  = CheckVendor3I

data ShowVendorResultsI
  = ShowVendorResultsI

instance semigroupShowVendorResultsI :: Semigroup ShowVendorResultsI where
  append a b = b

instance monoidShowVendorResultsI :: Monoid ShowVendorResultsI where
  mempty = ShowVendorResultsI

instance semigroupCheckVendor1I :: Semigroup CheckVendor1I where
  append a b = b

instance monoidCheckVendor1I :: Monoid CheckVendor1I where
  mempty = CheckVendor1I

instance semigroupCheckVendor2I :: Semigroup CheckVendor2I where
  append a b = b

instance monoidCheckVendor2I :: Monoid CheckVendor2I where
  mempty = CheckVendor2I

instance semigroupCheckVendor3I :: Semigroup CheckVendor3I where
  append a b = b

instance monoidCheckVendor3I :: Monoid CheckVendor3I where
  mempty = CheckVendor3I

data Yup
  = Yup

instance semigroupYup :: Semigroup Yup where
  append a b = b

instance monoidYup :: Monoid Yup where
  mempty = Yup

class StateMachine (ii :: Type) (i :: Type) (o :: Type) | ii i -> o

instance indexIndexCheckVendor1I :: (Cons "checkVendor1" Yup rin rout) => StateMachine CheckVendor1I { | rin } { | rout }

instance indexIndexCheckVendor2I :: (Cons "checkVendor2" Yup rin rout) => StateMachine CheckVendor2I { | rin } { | rout }

instance indexIndexCheckVendor3I :: (Cons "checkVendor3" Yup rin rout) => StateMachine CheckVendor3I { | rin } { | rout }

instance indexIndexShowVendorResultsI :: (Cons "checkVendor1" Yup prevA rin, Cons "checkVendor2" Yup prevB rin, Cons "checkVendor3" Yup prevC rin, Cons "showVendorResults" Yup rin rout) => StateMachine ShowVendorResultsI { | rin } { | rout }

data PureFiber a

data Program a
  = CheckVendor1 CheckVendor1I (String -> a)
  | CheckVendor2 CheckVendor2I (String -> a)
  | CheckVendor3 CheckVendor3I (String -> a)
  | ShowVendorResults ShowVendorResultsI (Array String) (Unit -> a)

newtype IndexedProgram i o a
  = IndexedProgram (Free Program a)

derive instance newtypeIndexedProgram :: Newtype (IndexedProgram i o a) _

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

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

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

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

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

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

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

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

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

instance freeProgramIxMonad :: IxMonad IndexedProgram

type IndexedNaturalTransformation
  = forall f m i o. i -> o -> (forall a. f a -> m i o a)

newtype NIT f m i o
  = NIT (forall a. f a -> m i o a)

class ToIndexed ntrans a b | a -> b, b -> a where
  toIndexed :: ntrans -> a -> b

instance ti0 :: (Monoid ii, Monoid i, Monoid o, StateMachine ii i o) => ToIndexed (NIT f m i o) (ii -> (b -> b) -> f b) (m i o b) where
  toIndexed (NIT f) ctr = f (ctr mempty identity)
else instance ti1 :: (Monoid ii, Monoid i, Monoid o, StateMachine ii i o) => ToIndexed (NIT f m i o) (ii -> y -> (b -> b) -> f b) (y -> m i o b) where
  toIndexed (NIT f) ctr y = f (ctr mempty y identity)
else instance ti2 :: (Monoid ii, Monoid i, Monoid o, StateMachine ii i o) => ToIndexed (NIT f m i o) (ii -> x -> y -> (b -> b) -> f b) (x -> y -> m i o b) where
  toIndexed (NIT f) ctr x y = f (ctr mempty x y identity)
else instance ti3 :: (Monoid ii, Monoid i, Monoid o, StateMachine ii i o) => ToIndexed (NIT f m i o) (ii -> w -> x -> y -> (b -> b) -> f b) (w -> x -> y -> m i o b) where
  toIndexed (NIT f) ctr w x y = f (ctr mempty w x y identity)
else instance ti4 :: (Monoid ii, Monoid i, Monoid o, StateMachine ii i o) => ToIndexed (NIT f m i o) (ii -> v -> w -> x -> y -> (b -> b) -> f b) (v -> w -> x -> y -> m i o b) where
  toIndexed (NIT f) ctr v w x y = f (ctr mempty v w x y identity)
else instance ti5 :: (Monoid ii, Monoid i, Monoid o, StateMachine ii i o) => ToIndexed (NIT f m i o) (ii -> u -> v -> w -> x -> y -> (b -> b) -> f b) (u -> v -> w -> x -> y -> m i o b) where
  toIndexed (NIT f) ctr u v w x y = f (ctr mempty u v w x y identity)

checkVendor1 = toIndexed (NIT (IndexedProgram <<< liftF)) CheckVendor1

checkVendor2 = toIndexed (NIT (IndexedProgram <<< liftF)) CheckVendor2

checkVendor3 = toIndexed (NIT (IndexedProgram <<< liftF)) CheckVendor3

showVendorResults = toIndexed (NIT (IndexedProgram <<< liftF)) ShowVendorResults

ismoosh__ :: forall m a b c f s. IxMonad m => Semigroup (f s) => Apply f => Applicative f => m a b (f s) -> m b c s -> m a c (f s)
ismoosh__ a b = Ix.do
  coll <- a
  sing <- b
  ipure (coll <> pure sing)

ismoosh_ :: forall m a b c f s. IxMonad m => Semigroup (f s) => Apply f => Applicative f => m a b s -> m b c s -> m a c (f s)
ismoosh_ a b = Ix.do
  l <- a
  r <- b
  ipure (pure l <> pure r)

infixl 4 ismoosh__ as <!>

infixl 4 ismoosh_ as <!!>

prog ::
  IndexedProgram
    (Record ())
    ( Record
        ( "checkVendor1" :: Yup
        , "checkVendor2" :: Yup
        , "checkVendor3" :: Yup
        , "showVendorResults" :: Yup
        )
    )
    Unit
prog = Ix.do
  results <- checkVendor3 <!!> checkVendor1 <!> checkVendor2
  showVendorResults results

A word on existential qualification

In both programs above, the use of a typeclass StateMachine allows us to build transitions into the definition of a free monad. So why pass through a typeclass instead of building indexed constraints directly into the ADT? If we did with the S3 program, it may look something like this:

data Program' a
  = UploadAssetToS3' (forall rin rout. Cons "uploadAssetToS3" Yup rin rout) => Tuple (Proxy { | rin }) (Proxy { | rout })) String String (Unit -> a)
  | PersistS3LocationToDB' (forall rin rout. (Cons "uploadAssetToS3" Yup prev rin, Cons "persistS3LocationToDB" Yup rin rout) => Tuple (Proxy { | rin }) (Proxy { | rout })) String String String (Unit -> a)

When a function or constructor consumes an argument with a forall, we are in the world of existential types. For example, the first argument to UploadAssetToS3' has an existential type. That means that we can't specify its actual type - all we know is that the type exists. When applied, UploadAssetToS3' would need to accept an open-ended entity: one that is open enough that it can handle any rin and rout given this signature: forall rin rout. Cons "uploadAssetToS3" Yup rin rout) => Tuple (Proxy { | rin }) (Proxy { | rout }). But indexed monad function signatures like that of prog above specialize indices at the moment of instantiation, which means that they become too specific to satisfy the general constraint of the existential type. Instead, we need a way to "lift" our existential constraint into a function signature, and that's exactly what typeclasses afford us. At the moment when the function is created, it uses the state machine to "look up" correct signature, and the existential qualifier is "lifted" to a universal qualifier.

I use quotation marks around "lifted" because it's not quite true: we cannot peek inside an existential type and lift its constraint to a higher scope. Existential types need to be hermetic precisely because, if we knew what specific type they operated on, they would lose their existential quality (ie forall a. a) and instead be a known entity (ie String). We are able to "lift" the constraint associated with UploadAssetToS3I to a function signature because typeclasses exist at a global scope, meaning above all functions, all ADTs, etc. This is a particularity of the design of Haskell and PureScript that creates the effect of a typelevel event-bus. Instead of instantiating an existential type deep within a structure, we can use a type like UploadAssetToS3I as input to a class constraint at the point of definition of a universally-qualified function, ie uploadAssetToS3 above.

Parting shot

Indexed monads allow us to encode sequential, transactional and asynchronous business logic into a type system. As we saw in part 2, they are flexible enough to accommodate indeterminate orders of execution and multiple possible outcomes. As we saw in part 3, they can be encoded into a typeclass. And lastly, as we saw in this part, they can be encoded directly into the creation of the monad itself via free monad constructors.

I hope you enjoy working with indexed monads! We use them parsimoniously throughout the Meeshkan codebase to enforce certain business-critical relationships, like making sure our asset cache is up-to-date and that our reporters send correct information about things like videos being ready or tests completing.

Blog

Modeling asynchronous transactions with types — Part 4

Mike Solomon