PlusCal is a formal specification language created to model concurrent systems, and recently I became obsessed with implementing PlusCal as an embedded domain-specific language (eDSL) in Haskell. In other words, I want to model PlusCal processes as Haskell subroutines and also implement the model checker in Haskell.

I’m not done implementing this PlusCal eDSL, but I’m writing this to share what I learned in the course of doing so. Specifically, what I learned was:

You can model individual PlusCal processes as non-deterministic finite-state automata (NFAs)

I believe this is well-understood by users of PlusCal, but I’m mentioning this for people who are new to PlusCal.

You can model concurrent processes in PlusCal by computing the Cartesian product of their NFAs

I’m not sure if this is widely understood or not.

Haskell’s

`Applicative`

abstraction can compute Cartesian products of NFAsThis is the novel insight that this post contributes.

There are two reasons why I’m keen on modeling PlusCal using Cartesian products of NFAs:

We can use this trick to combine any number of PlusCal processes into a composite process

The behavior of this composite process is indistinguishable from the original collection of processes.

This approach simplifies the implementation of the model checker

The model checker now only needs to accept a single process as its input. To model check more than one process you compose them into a single process and model check the composite process.

Also, it’s a theoretically elegant solution, and that’s good enough for me.

#### Scope

Like I mentioned before, I have not fully implemented all of PlusCal, but here are the features I will explain how to implement in this post:

Concurrent processes

Concurrent processes in PlusCal are essentially NFAs where PlusCal labels correspond to NFA states and state transitions represent atomic process changes.

To be pedantic, a PlusCal process is an NFA where the transitions are not labeled (or, equivalently, there is only one input symbol).

Labels

These are breakpoints within a PlusCal process where the process may be interrupted by another process. All other actions are uninterruptible, so anything that happens between two successive labels is atomic in PlusCal.

Note that a label in PlusCal is not the same as a label in traditional NFA terminology. PlusCal labels correspond to NFA states.

The

`either`

keywordPlusCal lets a process non-deterministically branch using the

`either`

keyword with one nested subroutine per branch. The model checker explores and verify all possible branches.The

`with`

keywordA process can non-deterministically choose from zero or more values. Just like with

`either`

the model checker explores and verifies all possible choices.The

`await`

keywordA process can wait until a condition is satisfied before proceeding using the

`await`

keyword.The

`while`

keywordA process can run in a loop until a condition is satisfied

The

`skip`

keywordA process can

`skip`

, which does nothing.

I am not (yet) explaining how to implement the following parts of `PlusCal`

:

Global or process-local state

Temporal expressions

Note that there is a Haskell package named

`spectacle`

for temporal logic in Haskell that a coworker of mine published, which I might be able to use for this purpose, but I haven’t attempted to incorporate that, yet.The

`print`

keywordThe

`assert`

keywordThe

`goto`

keywordThe model checker

We need to be able to model temporal expressions in order to implement the model checker and I haven’t yet incorporated temporal expressions into my implementation.

I believe the implementation I describe in this post can be extended with those missing features (with the exception of `goto`

) and I’ve already privately implemented some of them. However, I omit them because they would interfere with the subject of this post.

Also, some PlusCal features we’ll get for free by virtue of embedding PlusCal in Haskell:

(Non-temporal) Expressions

We get all of TLA+’s non-temporal functionality (e.g. scalars, functions, composite data structures) for free from the Haskell language and its standard library. Plus we also access new functionality (such as algebraic data types) via Haskell.

Procedures (including the

`call`

and`return`

keyword)We won’t need to explicitly implement support for these keywords. We can already define and invoke procedures in Haskell using

`do`

notation, which we can overload to work with PlusCal processes.Modules

We can model PlusCal modules using a combination of Haskell modules and Haskell functions.

#### User experience

The best way to illustrate what I have in mind is through some sample working Haskell code.

First, I’d like to be able to translate a PlusCal process like this:

```
begin
A:
skip;
B:
either
C:
skip;
or
skip;
end either;
D:
skip;
end process
```

… into a Haskell process like this:

```
strings :: Coroutine String
= Begin "A" do
strings "B"
yield either
"C"
[ yield
, skip
]"D"
yield end
```

The type of our `strings`

process is `Coroutine String`

, meaning that it is a `Coroutine`

whose labels are `String`

s. The reason we specify the type of the labels is because the Haskell eDSL permits labels of any type and these labels might not necessarily be strings.

For example, suppose PlusCal permitted integers for labels, like this:

```
begin
0:
with x \in { 1, 2, 3 } do
await (x % 2 = 0);
x: (* Suppose we can even create dynamic labels from values in scope *)
skip;
end process
```

Then, the equivalent Haskell process would be:

```
ints :: Coroutine Int
= Begin 0 do
ints <- with [ 1, 2, 3 ]
x even x)
await (
yield x end
```

I mentioned in the introduction that we will be able to combine processes into a composite process, which looks like this:

```
pairs :: Coroutine (String, Int)
= do
pairs <- strings
string <- ints
int return (string, int)
```

The Haskell code evaluates those three processes to canonical normal forms representing the evolution of labels for each process.

For example, the canonical normal form for the `strings`

process is:

`Begin "A" [ Yield "B" [ Yield "C" [ Yield "D" [] ] , Yield "D" [] ] ]`

… representing the following NFA with these labels and transitions:

```
A → B → D
↘ ↗
C
```

In other words, this normal form data structure uses lists to model non-determinism (one list element per valid transition) and nesting to model sequential transitions.

Similarly, the canonical normal form for the `ints`

process is:

`Begin 0 [ Yield 2 [] ]`

… representing the following NFA with these labels and transitions:

```
0
↓
2
```

Finally, the canonical normal form for the composite `pairs`

process is:

```
Begin ( "A" , 0 )
Yield ( "B" , 0 )
[ Yield ( "C" , 0 )
[ Yield ( "D" , 0 ) [ Yield ( "D" , 2 ) [] ]
[ Yield ( "C" , 2 ) [ Yield ( "D" , 2 ) [] ]
,
]Yield ( "D" , 0 ) [ Yield ( "D" , 2 ) [] ]
, Yield ( "B" , 2 )
, Yield ( "C" , 2 ) [ Yield ( "D" , 2 ) [] ]
[ Yield ( "D" , 2 ) []
,
]
]Yield ( "A" , 2 )
, Yield ( "B" , 2 )
[ Yield ( "C" , 2 ) [ Yield ( "D" , 2 ) [] ]
[ Yield ( "D" , 2 ) []
,
]
] ]
```

… which is the Cartesian product of the two smaller NFAs:

```
(A,0) → (B,0) → (D,0)
↘ ↗
(C,0)
↓ ↓ ↓ ↓
(C,2)
↗ ↘
(A,2) → (B,2) → (D,2)
```

… and if we convert the Haskell composite process to the equivalent PlusCal process we would get:

```
begin
(A,0):
skip;
either
(B,0):
either
(C,0):
either
(D,0):
skip;
(D,2):
skip;
or
(C,2):
skip;
(D,2):
skip;
end either;
or
(D,0):
skip;
(D,2):
skip;
end either;
or
(A,2):
skip;
(B,2):
skip;
either
(C,2):
skip;
(D,2):
skip;
or
(D,2):
skip;
end either;
end either;
end process
```

This composite process is indistinguishable from the two input processes, meaning that:

This composite process is interruptible whenever one of the two original input processes is interruptible

This composite process performs an atomic state transition whenever one of the two input processes performs a state transition

The current label of the composite process is a function of the current label of the two original input processes

#### The `Process`

type

Now I’ll explain how to implement this subset of PlusCal as an eDSL in Haskell.

First, we begin from the following two mutually-recursive types which represent NFAs where there are zero more labeled states but the transitions are unlabeled:

```
newtype Process label result = Choice [Step label result]
data Step label result = Yield label (Process label result) | Done result
```

The `Process`

type handles the non-deterministic transitions for our NFA: a `Process`

stores zero or more valid state transitions (represented as a list of valid next `Step`

s).

The `Step`

type handles the labeled states for our NFA: a `Step`

can either `Yield`

or be `Done`

:

A step that

`Yield`

s includes the label for the current state and the remainder of the`Process`

A step that is

`Done`

includes a`result`

This

`result`

is used to thread data bound by one step to subsequent steps. For example, this is how our previous example was able to pass the`x`

bound by`with`

to the subsequent`yield`

command:`= Begin 0 do ints <- with [ 1, 2, 3 ] x … yield x …`

We’ll add support for rendering the data structures for debugging purposes:

```
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.Exts (IsList(..))
newtype Process label result = Choice [Step label result]
deriving newtype (IsList, Show)
data Step label result = Yield label (Process label result) | Done result
deriving stock (Show)
```

I make use of a small trick here where I derive `IsList`

for the `Process`

type This lets can omit the `Choice`

constructor when creating or rendering values of type `Process`

. That simplifies Haskell code like this:

```
Begin "A"
Choice
(Yield "B"
[ Choice
(Yield "C" (Choice [ Yield "D" (Choice []) ])
[ Yield "D" (Choice [])
,
]) ])
```

… to this more ergonomic syntax if we enable the `OverloadedLists`

extension:

`Begin "A" [ Yield "B" [ Yield "C" [ Yield "D" [] ] , Yield "D" [] ] ]`

`do`

notation

However, we don’t expect users to author these data structures by hand. Instead, we can use Haskell’s support for overloading `do`

notation so that users can author `Process`

values using subroutine-like syntax. In order to do this we need to implement the `Monad`

class for `Process`

, like this:

```
{-# LANGUAGE BlockArguments #-}
import qualified Control.Monad as Monad
instance Monad (Process label) where
Choice ps >>= f = Choice do
<- ps
p case p of
Yield label rest -> do
return (Yield label (rest >>= f))
Done result -> do
let Choice possibilities = f result
possibilities
instance Applicative (Process label) where
pure result = Choice (pure (Done result))
<*>) = Monad.ap
(
instance Functor (Process label) where
fmap = Monad.liftM
```

… and we also need to provide the following utility function:

```
yield :: label -> Process label ()
= Choice [Yield label (pure ())] yield label
```

Equipped with that `Monad`

instance we can now author code like this:

```
example :: Process Int ()
= do
example 1
yield 2
yield 3 yield
```

… and that superficially imperative code actually evaluates to a pure data structure:

`Yield 1 [ Yield 2 [ Yield 3 [ Done () ] ] ] ] [ `

The reason that works is because any type that implements `Monad`

can be sequenced using `do`

notation, because `do`

notation is syntactic sugar for the `(>>=)`

operator we defined in our `Monad`

instance. To learn more, read:

We can also now implement `skip`

, which is just a synonym for `pure ()`

(i.e. “do nothing”):

```
skip :: Process label ()
= pure () skip
```

Unlike PlusCal, we don’t need to use `skip`

most of the time. In particular, we don’t need to add a skip in between two labels if nothing happens. For example, suppose we try to translate this PlusCal code:

```
1:
skip;
2:
skip;
```

… to Haskell:

```
example :: Process Int ()
= do
example 1
yield
skip2
yield skip
```

We don’t actually need those `skip`

s. The following code without `skip`

s is the exact same `Process`

:

```
example :: Process Int ()
= do
example 1
yield 2 yield
```

Both ways of writing the `Process`

produce the same result, which is:

`Yield 1 [ Yield 2 [ Done () ] ] ] [ `

Finally, we can implement the `while`

keyword as an ordinary Haskell function:

```
while :: Process label Bool -> Process label () -> Process label ()
= do
while condition body <- condition
bool Monad.when bool do
body while condition body
```

In fact, there’s nothing really PlusCal-specific about this utility; this functionality already exists as `Control.Monad.Loops.whileM_`

.

#### Alternation

So far we can only sequence commands, but we’d also like to be able to branch non-deterministically. Fortunately, Haskell has a standard API for doing that, too, which is the `Alternative`

class. We can implement `Alternative`

for our `Process`

type like this:

```
import Control.Applicative (Alternative(..))
instance Alternative (Process label) where
= Choice empty
empty
Choice stepsL <|> Choice stepsR = Choice (stepsL <|> stepsR)
```

We’ll also define `end`

to be a synonym for `empty`

:

```
end :: Process label a
= empty end
```

In other words, if you `end`

a `Process`

there are no more valid transitions.

When we implement this `Alternative`

instance we can make use of several general-purpose utilities that work for any type that implements `Alternative`

. One such utility is `Data.Foldable.asum`

, which behaves exactly the same as PlusCal’s `either`

keyword:

```
import Prelude hiding (either)
import qualified Data.Foldable as Foldable
either :: [Process label result] -> Process label result
either = Foldable.asum
```

We could also write the implementation of `either`

by hand if we wanted to, which would be:

```
either (process : processes) = process <|> either processes
either [] = empty
```

… which is exact same behavior as using `asum`

.

In other words, given a list of `Process`

es, we can try all of them in parallel using `either`

. All that `either`

does is concatenate the lists of valid `Step`

s for each of the input `Process`

es.

`Control.Monad.guard`

is another utility we get for free by virtue of implementing `Alternative`

and `guard`

behaves in the exact same way as PlusCal’s `await`

keyword:

```
await :: Bool -> Process label ()
= Monad.guard await
```

We could also write the implementation of `await`

by hand if we wanted to, which would be:

```
True = skip
await False = end await
```

… which is the same behavior as using `guard`

.

Finally, we can implement `with`

in terms of `either`

, like this:

```
with :: [result] -> Process label result
= either (map pure results) with results
```

In other words, you can implement `with`

as if it were an `either`

statement with one branch per value that you want to bind. However, you have to promote each value to a trivial `Process`

(using `pure`

) in order to combine them using `either`

.

#### Cartesian product of NFAs

In the introduction I noted that we can model multiple processes in PlusCal by computing the Cartesian product of their NFAs. This section explains that in more detail, first as prose and then followed by Haskell code.

Informally, the Cartesian product of zero or more “input” NFAs creates a composite “output” NFA where:

The set of possible states for the output NFA is the Cartesian product of the set of possible states for each input NFA

In other words, if we have two input NFAs and the first NFA permits the following states:

`A, B, C ] [`

… and the second NFA permits the following states:

`0, 1, 2 ] [`

… then the Cartesian product of those two sets of states is:

`A,0), (B,0), (C,0), (A,1), (B,1), (C,1), (A,2), (B,2), (C,2) ] [ (`

… which is our composite set of possible states.

The starting state for our output NFA is the Cartesian product of the starting states for each input NFA

In other words, if our first NFA has a starting state of:

`A`

… and our second has a starting state of:

`0`

… then the Cartesian product of those two starting states is:

`A,0) (`

… which is our composite starting state.

The set of valid transitions for any output state is the union of the set of valid transitions for the input sub-states

In other words, if the state

`A`

can transition to either state`B`

or`C`

:`B, C ] [`

… and the state

`0`

can transition to only state`2`

:`2 ] [`

… then the state

`(A,0)`

can transition to any of these states:`B, 0), (C, 0), (A, 2) ] [ (`

… and this is because:

If state

`A`

transitions to state`B`

, then our composite state`(A,0)`

transitions to state`(B,0)`

If state

`A`

transitions to state`C`

, then our composite state`(B,0)`

transitions to state`(C,0)`

If state

`0`

transitions to state`2`

, then our composite state`(A,0)`

transitions to state`(A,2)`

`Applicative`

as Cartesian product

Haskell’s standard library defines the following `Applicative`

class:

```
class Applicative f where
pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b
```

…and you can think of Haskell’s `Applicative`

class as (essentially) an interface for arbitrary N-ary Cartesian products, meaning that any type that implements an `Applicative`

instance gets the following family of functions for free:

```
-- The 0-ary Cartesian product
join0 :: Applicative f => f ()
= pure ()
join0
-- The unary Cartesian product
join1 :: Applicative f => f a -> f a
= pure id <*> as
join1 as
-- The binary Cartesian product
join2 :: Applicative f => f a -> f b -> f (a, b)
= pure (,) <*> as <*> bs
join2 as bs
-- The trinary Cartesian product
join3 :: Applicative f => f a -> f b -> f c -> f (a, b, c)
= pure (,,) <*> as <*> bs <*> cs
join3 as bs cs
…
```

… and so on. I deliberately implemented some of those functions in a weird way to illustrate the overall pattern.

This means that if we implement `Applicative`

for our NFA type then we can use that interface to create arbitrary N-ary Cartesian products of NFAs.

#### The `Coroutine`

type

The `Process`

type does implement an `Applicative`

instance, but this is a different (more boring) Cartesian product and not the one we’re interested in. In fact, the `Process`

type *cannot* implement the instance we’re interested in (the Cartesian product of NFAs), because our `Process`

type is not a complete NFA: our `Process`

type is missing a starting state.

This is what the following `Coroutine`

type fixes by extending our `Process`

type with an extra field for the starting state:

```
import Data.Void (Void)
data Coroutine label = Begin label (Process label Void)
deriving stock (Show)
```

We also constrain the `Process`

inside of a `Coroutine`

to return `Void`

(the impossible/uninhabited type). Any `Process`

that ends with no valid transitions will satisfy this type, such as a process that concludes with an `end`

or `empty`

:

```
example :: Coroutine Int
= Begin 0 do
example 1
yield 2
yield end
```

Once we add in the starting state we can implement `Applicative`

for our `Coroutine`

type, which is essentially the same thing as implementing the Cartesian product of NFAs:

```
instance Applicative Coroutine where
-- The empty (0-ary) Cartesian product has only a single valid state, which
-- is also the starting state, and no possible transitions.
pure label = Begin label empty
-- The (sort of) binary Cartesian product …
<*>)
(-- … of a first NFA …
@(Begin label0F (Choice fs))
f-- … and a second NFA …
@(Begin label0X (Choice xs)) =
xBegin
-- … has a starting state which is (sort of) the product of the
-- first and second starting states
(label0F label0X)-- … and the set of valid transitions is the union of valid
-- transitions for the first and second NFAs
Choice (fmap adaptF fs <|> fmap adaptX xs))
(where
-- If the first NFA transitions, then we don't disturb the state
-- of the second NFA
Done result) = Done result
adaptF (Yield labelF restF) = Yield labelFX restFX
adaptF (where
Begin labelFX restFX = Begin labelF restF <*> x
-- If the second NFA transitions, then we don't disturb the state
-- of the first NFA
Done result) = Done result
adaptX (Yield labelX restX) = Yield labelFX restFX
adaptX (where
Begin labelFX restFX = f <*> Begin labelX restX
```

I use “sort of” in the comments to indicate that `(<*>)`

is not actually the binary Cartesian product, but it’s spiritually similar enough.

Moreover, we can reassure ourselves that this `Applicative`

instance is well-behaved because this instance satisfies the `Applicative`

laws. See Appendix D for the proof of all four laws for the above instance.

`ApplicativeDo`

Haskell is not the only language that defines an `Applicative`

abstraction. For example, the `Cats`

package in the Scala ecosystem also defines an `Applicative`

abstraction, too.

However, the Haskell ecosystem has one edge over other languages (including Scala), which is language support for types that only implement `Applicative`

and not `Monad`

.

Specifically, Haskell has an `ApplicativeDo`

extension, which we can use to combine values for any `Applicative`

type using `do`

notation. In fact, this is why the original example using `pairs`

worked, because of that extension:

```
{-# LANGUAGE ApplicativeDo #-}
pairs :: Coroutine (String, Int)
= do
pairs <- strings
string <- ints
int return (string, int)
```

When we enable that extension the Haskell compiler desugars that `do`

notation to something like this:

```
= f <$> strings <*> ints
pairs where
= (string, int) f string int
```

… and in my opinion the version using `do`

notation is more readable and ergonomic.

Normally `do`

notation only works on types that implement `Monad`

, but when we enable the `ApplicativeDo`

extension then a subset of `do`

notation works for types that implement `Applicative`

(which is superset of the types that implement `Monad`

).

Our `Coroutine`

type is one such type that benefits from this `ApplicativeDo`

extension. The `Coroutine`

type can implement `Applicative`

, but not `Monad`

, so the only way we can use `do`

notation for `Coroutine`

s is if we enable `ApplicativeDo`

.

The `ApplicativeDo`

extension also plays very nicely with Haskell’s support for `NamedFieldPuns`

or `RecordWildCards`

. For example, instead of packing the labels into a tuple we could instead slurp them into a record as fields of the same name:

```
{-# LANGUAGE RecordWildCards #-}
data Status = Status
string :: String
{ int :: Int
,
}
pairs :: Coroutine Status
= do
pairs <- strings
string <- ints
int return Status{..}
```

… and this scales really well to a large number of `Coroutine`

s.

#### Conclusion

I’ve included the complete implementation from this post in Appendix A if you want to test this code out on your own. Once I’m done with the complete embedding of PlusCal in Haskell I’ll publish something a bit more polished.

If you enjoyed this post, you’ll probably also enjoy this paper:

… which was the original paper that introduced the `Applicative`

abstraction.

I also left some “bonus commentary” in Appendix B and Appendix C for a few digressions that didn’t quite make the cut for the main body of this post.

#### Appendix A - Complete implementation

The following module only depends on the `pretty-show`

package (and not even that if you delete the `main`

subroutine).

```
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.Exts (IsList(..))
import Control.Applicative (Alternative(..), liftA2)
import Data.Void (Void)
import Prelude hiding (either)
import qualified Control.Applicative as Applicative
import qualified Control.Monad as Monad
import qualified Data.Foldable as Foldable
import qualified Text.Show.Pretty as Pretty
newtype Process label result = Choice [Step label result]
deriving newtype (IsList, Show)
data Step label result = Yield label (Process label result) | Done result
deriving stock (Show)
instance Functor (Process label) where
fmap = Monad.liftM
instance Applicative (Process label) where
pure result = Choice (pure (Done result))
<*>) = Monad.ap
(
instance Monad (Process label) where
Choice ps >>= f = Choice do
<- ps
p case p of
Yield label rest -> do
return (Yield label (rest >>= f))
Done result -> do
let Choice possibilities = f result
possibilities
instance Semigroup result => Semigroup (Process label result) where
<>) = liftA2 (<>)
(
instance Monoid result => Monoid (Process label result) where
mempty = pure mempty
instance Alternative (Process label) where
= Choice empty
empty
Choice stepsL <|> Choice stepsR = Choice (stepsL <|> stepsR)
data Coroutine label = Begin label (Process label Void)
deriving stock (Show)
instance Functor Coroutine where
fmap = Applicative.liftA
instance Applicative Coroutine where
pure label = Begin label empty
<*>)
(@(Begin label0F (Choice fs))
f@(Begin label0X (Choice xs)) =
xBegin (label0F label0X) (Choice (fmap adaptF fs <|> fmap adaptX xs))
where
Done result) = Done result
adaptF (Yield labelF restF) = Yield labelFX restFX
adaptF (where
Begin labelFX restFX = Begin labelF restF <*> x
Done result) = Done result
adaptX (Yield labelX restX) = Yield labelFX restFX
adaptX (where
Begin labelFX restFX = f <*> Begin labelX restX
instance Semigroup label => Semigroup (Coroutine label) where
<>) = liftA2 (<>)
(
instance Monoid label => Monoid (Coroutine label) where
mempty = pure mempty
yield :: label -> Process label ()
= Choice [Yield label (pure ())]
yield label
either :: [Process label result] -> Process label result
either = Foldable.asum
await :: Bool -> Process label ()
= Monad.guard
await
with :: [result] -> Process label result
= either (map pure results)
with results
end :: Process label a
= empty
end
skip :: Process label ()
= mempty
skip
strings :: Coroutine String
= Begin "A" do
strings "B"
yield either
"C"
[ yield
, skip
]"D"
yield
end
ints :: Coroutine Int
= Begin 0 do
ints <- with [ 1, 2, 3 ]
x even x)
await (
yield x
end
pairs :: Coroutine (String, Int)
= do
pairs <- strings
string <- ints
int return (string, int)
main :: IO ()
= do
main
Pretty.pPrint strings
Pretty.pPrint ints Pretty.pPrint pairs
```

If you run that it will print:

```
Begin
"A" [ Yield "B" [ Yield "C" [ Yield "D" [] ] , Yield "D" [] ] ]
Begin 0 [ Yield 2 [] ]
Begin
"A" , 0 )
( Yield
[ "B" , 0 )
( Yield
[ "C" , 0 )
( Yield ( "D" , 0 ) [ Yield ( "D" , 2 ) [] ]
[ Yield ( "C" , 2 ) [ Yield ( "D" , 2 ) [] ]
,
]Yield ( "D" , 0 ) [ Yield ( "D" , 2 ) [] ]
, Yield
, "B" , 2 )
( Yield ( "C" , 2 ) [ Yield ( "D" , 2 ) [] ]
[ Yield ( "D" , 2 ) []
,
]
]Yield
, "A" , 2 )
( Yield
[ "B" , 2 )
( Yield ( "C" , 2 ) [ Yield ( "D" , 2 ) [] ]
[ Yield ( "D" , 2 ) []
,
]
] ]
```

#### Appendix B - Free Monads

The implementation for `Process`

is actually a special case of a free monad transformer, except that I’ve hand-written the types and instances so that the types are easier to inspect. However, if we really wanted to code golf all of this we could have replaced all of that code with just these three lines:

```
import Control.Monad.Trans.Free (FreeT, liftF)
type Process label = FreeT ((,) label) []
= liftF (label, ()) yield label
```

… and that would have behaved the exact same (including the same `Monad`

and `Alternative`

instances). You can read that as essentially saying: “A `Process`

is a subroutine that alternates between emitting a `label`

(i.e. `(,) label`

) and branching non-deterministically (i.e. `[]`

)”.

#### Appendix C - `Monoid`

/ `Semigroup`

If we want to be extra clever, we can implement `Semigroup`

and `Monoid`

instances for `Process`

as suggested in this post:

… which we would do like this:

```
import Control.Applicative (liftA2)
instance Semigroup result => Semigroup (Process label result) where
<>) = liftA2 (<>)
(
instance Monoid result => Monoid (Process label result) where
mempty = pure mempty
```

… and then we can simplify `skip`

a tiny bit further to:

`= mempty skip `

#### Appendix D - Proof of the `Applicative`

laws

The first `Applicative`

law requires that:

`pure id <*> v = v`

Proof:

```
pure id <*> v
-- Definition of `pure`:
--
-- pure label = Begin label empty
= Begin id empty <*> v
-- Define:
--
-- v = Begin label0X (Choice xs)
= Begin id empty <*> Begin label0X (Choice xs)
-- Definition of `(<*>)`
= Begin (id label0X) (Choice (fmap adaptF empty <|> fmap adaptX xs))
where
Done result) = Done result
adaptF (Yield labelF restF) = Yield labelFX restFX
adaptF (where
Begin labelFX restFX = Begin labelF restF <*> Begin label0X (Choice xs)
Done result) = Done result
adaptX (Yield labelX restX) = Yield labelFX restFX
adaptX (where
Begin labelFX restFX = Begin id empty <*> Begin labelX restX
-- fmap f empty = empty
= Begin (id label0X) (Choice (empty <|> fmap adaptX xs))
where
Done result) = Done result
adaptX (Yield labelX restX) = Yield labelFX restFX
adaptX (where
Begin labelFX restFX = Begin id empty <*> Begin labelX restX
-- empty <|> xs = xs
= Begin (id label0X) (Choice (fmap adaptX xs))
where
Done result) = Done result
adaptX (Yield labelX restX) = Yield labelFX restFX
adaptX (where
Begin labelFX restFX = Begin id empty <*> Begin labelX restX
-- Definition of `pure`, in reverse
--
-- pure label = Begin label empty
= Begin (id label0X) (Choice (fmap adaptX xs))
where
Done result) = Done result
adaptX (Yield labelX restX) = Yield labelFX restFX
adaptX (where
Begin labelFX restFX = pure id <*> Begin labelX restX
-- Induction: pure id <*> v = v
= Begin (id label0X) (Choice (fmap adaptX xs))
where
Done result) = Done result
adaptX (Yield labelX restX) = Yield labelFX restFX
adaptX (where
Begin labelFX restFX = Begin labelX restX
-- Simplify
= Begin (id label0X) (Choice (fmap adaptX xs))
where
Done result) = Done result
adaptX (Yield labelX restX) = Yield labelX restX
adaptX (
-- Simplify
= Begin (id label0X) (Choice (fmap adaptX xs))
where
= id
adaptX
-- Functor identity law:
--
-- fmap id = id
= Begin (id label0X) (Choice (id xs))
-- Definition of `id`:
--
-- id x = x
= Begin label0X (Choice xs)
-- Definition of `v`, in reverse
--
-- v = Begin label0X (Choice xs)
= v
```

The second `Applicative`

law requires that:

`pure (.) <*> u <*> v <*> w = u <*> (v <*> w)`

Proof:

```
pure (.) <*> u <*> v <*> w
-- Define:
--
-- u = Begin label0U (Choice us)
-- v = Begin label0V (Choice vs)
-- w = Begin label0W (Choice ws)
= pure (.)
<*> Begin label0U (Choice us)
<*> Begin label0V (Choice vs)
<*> Begin label0W (Choice ws)
-- Definition of `pure`:
= Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin label0V (Choice vs)
<*> Begin label0W (Choice ws)
-- Definition of `(<*>)`
= Begin ((.) label0U) (Choice (fmap adaptF empty <|> fmap adaptU us))
<*> Begin label0V (Choice vs)
<*> Begin label0W (Choice ws)
where
Done result) = Done result
adaptF (Yield labelF restF) = Yield labelFX restFX
adaptF (where
Begin labelFX restFX = Begin labelF restF <*> Begin label0U (Choice us)
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFU restFU
adaptU (where
Begin labelFU restFU = Begin (.) empty <*> Begin labelU restU
-- fmap f empty = empty
= Begin ((.) label0U) (Choice (fmap adaptU us))
<*> Begin label0V (Choice vs)
<*> Begin label0W (Choice ws)
where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFU restFU
adaptU (where
Begin labelFU restFU = Begin (.) empty <*> Begin labelU restU
-- Definition of `(<*>)`
= Begin (label0U . label0V)
Choice (fmap adaptFU (fmap adaptU us) <|> fmap adaptV vs))
(<*> Begin label0W (Choice ws)
where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFU restFU
adaptU (where
Begin labelFU restFU = Begin (.) empty <*> Begin labelU restU
Done result) = Done result
adaptFU (Yield labelFU restFU) = Yield labelFUV restFUV
adaptFU (where
Begin labelFUV restFUV =
Begin labelFU restFU <*> Begin label0V (Choice vs)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
Begin ((.) label0U) (Choice (fmap adaptU us))
<*> Begin labelV restV
-- Definition of `(<*>)`, in reverse
= Begin (label0U . label0V)
Choice (fmap adaptFU (fmap adaptU us) <|> fmap adaptV vs))
(<*> Begin label0W (Choice ws)
where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFU restFU
adaptU (where
Begin labelFU restFU = Begin (.) empty <*> Begin labelU restU
Done result) = Done result
adaptFU (Yield labelFU restFU) = Yield labelFUV restFUV
adaptFU (where
Begin labelFUV restFUV =
Begin labelFU restFU <*> Begin label0V (Choice vs)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin labelV restV
-- fmap f (fmap g x) = fmap (f . g) x
= Begin (label0U . label0V)
Choice (fmap (adaptFU . adaptU) us <|> fmap adaptV vs))
(<*> Begin label0W (Choice ws)
where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFU restFU
adaptU (where
Begin labelFU restFU = Begin (.) empty <*> Begin labelU restU
Done result) = Done result
adaptFU (Yield labelFU restFU) = Yield labelFUV restFUV
adaptFU (where
Begin labelFUV restFUV =
Begin labelFU restFU <*> Begin label0V (Choice vs)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin labelV restV
-- Consolidate (adaptFU . adaptU)
= Begin (label0U . label0V) (Choice (fmap adaptU us <|> fmap adaptV vs))
<*> Begin label0W (Choice ws)
where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFUV restFUV
adaptU (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin labelU restU
<*> Begin label0V (Choice vs)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin labelV restV
-- Definition of `(<*>)`
= Begin (label0U (label0V label0W))
Choice
(fmap adaptFUV (fmap adaptU us <|> fmap adaptV vs)
( <|> fmap adaptW ws
)
)where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFUV restFUV
adaptU (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin labelU restU
<*> Begin label0V (Choice vs)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin labelV restV
Done result) = Done result
adaptFUV (Yield labelFUV restFUV) = Yield labelFUVW restFUVW
adaptFUV (where
Begin labelFUVW restFUVW =
Begin labelFUV restFUV
<*> Begin label0W (Choice ws)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelFUVW restFUVW
adaptW (where
Begin labelFUVW restFUVW =
Begin (label0U . label0V)
Choice (fmap adaptU us <|> fmap adaptV vs))
(<*> Begin labelW restW
-- Definition of `(<*>)`, in reverse
= Begin (label0U (label0V label0W))
Choice
(fmap adaptFUV (fmap adaptU us <|> fmap adaptV vs)
( <|> fmap adaptW ws
)
)where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFUV restFUV
adaptU (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin labelU restU
<*> Begin label0V (Choice vs)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin labelV restV
Done result) = Done result
adaptFUV (Yield labelFUV restFUV) = Yield labelFUVW restFUVW
adaptFUV (where
Begin labelFUVW restFUVW =
Begin labelFUV restFUV
<*> Begin label0W (Choice ws)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelFUVW restFUVW
adaptW (where
Begin labelFUVW restFUVW =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin label0V (Choice vs)
<*> Begin labelW restW
-- fmap f (x <|> y) = fmap f x <|> fmap f y
= Begin (label0U (label0V label0W))
Choice
(fmap adaptFUV (fmap adaptU us)
( <|> fmap adaptFUV (fmap adaptV vs)
<|> fmap adaptW ws
)
)where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFUV restFUV
adaptU (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin labelU restU
<*> Begin label0V (Choice vs)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin labelV restV
Done result) = Done result
adaptFUV (Yield labelFUV restFUV) = Yield labelFUVW restFUVW
adaptFUV (where
Begin labelFUVW restFUVW =
Begin labelFUV restFUV
<*> Begin label0W (Choice ws)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelFUVW restFUVW
adaptW (where
Begin labelFUVW restFUVW =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin label0V (Choice vs)
<*> Begin labelW restW
-- fmap f (fmap g x) = fmap (f . g) x
= Begin (label0U (label0V label0W))
Choice
(fmap (adaptFUV . adaptU) us
( <|> fmap (adaptFUV . adaptV) vs
<|> fmap adaptW ws
)
)where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFUV restFUV
adaptU (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin labelU restU
<*> Begin label0V (Choice vs)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin labelV restV
Done result) = Done result
adaptFUV (Yield labelFUV restFUV) = Yield labelFUVW restFUVW
adaptFUV (where
Begin labelFUVW restFUVW =
Begin labelFUV restFUV
<*> Begin label0W (Choice ws)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelFUVW restFUVW
adaptW (where
Begin labelFUVW restFUVW =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin label0V (Choice vs)
<*> Begin labelW restW
-- Consolidate (adaptFUV . adaptU) and (adaptFUV . adaptV)
= Begin (label0U (label0V label0W))
Choice
(fmap adaptU us
( <|> fmap adaptV vs
<|> fmap adaptW ws
)
)where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFUV restFUV
adaptU (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin labelU restU
<*> Begin label0V (Choice vs)
<*> Begin label0W (Choice ws)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin labelV restV
<*> Begin label0W (Choice ws)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelFUVW restFUVW
adaptW (where
Begin labelFUVW restFUVW =
Begin (.) empty
<*> Begin label0U (Choice us)
<*> Begin label0V (Choice vs)
<*> Begin labelW restW
-- Definition of `pure`, in reverse
--
-- pure label = Begin label empty
= Begin (label0U (label0V label0W))
Choice
(fmap adaptU us
( <|> fmap adaptV vs
<|> fmap adaptW ws
)
)where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFUV restFUV
adaptU (where
Begin labelFUV restFUV =
pure (.)
<*> Begin labelU restU
<*> Begin label0V (Choice vs)
<*> Begin label0W (Choice ws)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
pure (.)
<*> Begin label0U (Choice us)
<*> Begin labelV restV
<*> Begin label0W (Choice ws)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelFUVW restFUVW
adaptW (where
Begin labelFUVW restFUVW =
pure (.)
<*> Begin label0U (Choice us)
<*> Begin label0V (Choice vs)
<*> Begin labelW restW
-- Induction: pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
= Begin (label0U (label0V label0W))
Choice
(fmap adaptU us
( <|> fmap adaptV vs
<|> fmap adaptW ws
)
)where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelFUV restFUV
adaptU (where
Begin labelFUV restFUV =
Begin labelU restU
<*> ( Begin label0V (Choice vs)
<*> Begin label0W (Choice ws)
)
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelFUV restFUV
adaptV (where
Begin labelFUV restFUV =
Begin label0U (Choice us)
<*> ( Begin labelV restV
<*> Begin label0W (Choice ws)
)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelFUVW restFUVW
adaptW (where
Begin labelFUVW restFUVW =
Begin label0U (Choice us)
<*> ( Begin label0V (Choice vs)
<*> Begin labelW restW
)
-- Unfactor up `adaptV` into `adaptVW . adaptV` and `adaptW` into
-- `adaptVW . adaptW`
= Begin (label0U (label0V label0W))
Choice
(fmap adaptU us
( <|> fmap adaptVW (fmap adaptV vs)
<|> fmap adaptVW (adaptW ws)
)
)where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelUVW restUVW
adaptU (where
Begin labelUVW restUVW =
Begin labelU (Choice us)
<*> ( Begin label0V (Choice vs)
<*> Begin label0W (Choice ws)
)
Done result) = Done result
adaptVW (Yield labelVW restVW) = Yield labelUVW restUVW
adaptVW (where
Begin labelUVW restUVW =
Begin label0U (Choice us)
<*> Begin labelVW restVW
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelVW restVW
adaptV (where
Begin labelVW restVW = Begin labelV restV <*> Begin label0W (Choice ws)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelVW restVW
adaptV (where
Begin lableVW restVW = Begin label0V (Choice vs) <*> Begin labelW restW
-- fmap f (x <|> y) = fmap f x <|> fmap f y
= Begin (label0U (label0V label0W))
Choice
(fmap adaptU us
( <|> fmap adaptVW (fmap adaptV vs <|> fmap adaptW ws)
)
)where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelUVW restUVW
adaptU (where
Begin labelUVW restUVW =
Begin labelU (Choice us)
<*> ( Begin label0V (Choice vs)
<*> Begin label0W (Choice ws)
)
Done result) = Done result
adaptVW (Yield labelVW restVW) = Yield labelUVW restUVW
adaptVW (where
Begin labelUVW restUVW =
Begin label0U (Choice us)
<*> Begin labelVW restVW
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelVW restVW
adaptV (where
Begin labelVW restVW = Begin labelV restV <*> Begin label0W (Choice ws)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelVW restVW
adaptV (where
Begin lableVW restVW = Begin label0V (Choice vs) <*> Begin labelW restW
-- Definition of `(<*>)`
= Begin (label0U (label0V label0W))
Choice
(fmap adaptU us
( <|> fmap adaptVW (fmap adaptV vs <|> fmap adaptW ws)
)
)where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelUVW restUVW
adaptU (where
Begin labelUVW restUVW =
Begin labelU (Choice us)
<*> Begin (label0V label0W)
Choice (fmap adaptV vs <|> fmap adaptW ws))
(
Done result) = Done result
adaptVW (Yield labelVW restVW) = Yield labelUVW restUVW
adaptVW (where
Begin labelUVW restUVW =
Begin label0U (Choice us)
<*> Begin labelVW restVW
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelVW restVW
adaptV (where
Begin labelVW restVW = Begin labelV restV <*> Begin label0W (Choice ws)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelVW restVW
adaptV (where
Begin lableVW restVW = Begin label0V (Choice vs) <*> Begin labelW restW
-- Definition of `(<*>)`, in reverse
= Begin label0U (Choice us)
<*> Begin (label0V label0W)
Choice (fmap adaptV vs <|> fmap adaptW ws))
(where
Done result) = Done result
adaptV (Yield labelV restV) = Yield labelVW restVW
adaptV (where
Begin labelVW restVW = Begin labelV restV <*> Begin label0W (Choice ws)
Done result) = Done result
adaptW (Yield labelW restW) = Yield labelVW restVW
adaptV (where
Begin lableVW restVW = Begin label0V (Choice vs) <*> Begin labelW restW
-- Definition of `(<*>)`, in reverse
= Begin label0U (Choice us)
<*> ( Begin label0V (Choice vs)
<*> Begin label0W (Choice ws)
)
-- Definition of `u`, `v`, `w`, in reverse:
--
-- u = Begin label0U (Choice us)
-- v = Begin label0V (Choice vs)
-- w = Begin label0W (Choice ws)
= u <*> (v <*> w)
```

The third `Applicative`

law requires that:

`pure f <*> pure x = pure (f x)`

Proof:

```
pure f <*> pure x
-- Definition of `pure`
--
-- pure label = Begin label empty
= Begin f empty <*> Begin x empty
-- Definition of `(<*>)`
= Begin (f x) (fmap adaptF empty <|> fmap adaptX empty)
where
Done resultF) = Done resultF
adaptF (Yield labelF restF) = Yield labelFX restFX
adaptF (where
Begin labelFX restFX = Begin labelF restF <*> Begin x empty
Done resultX) = Done resultX
adaptX (Yield labelX restX) = Yield labelFX restFX
adaptX (where
Begin labelFX restFX = Begin f empty <*> Begin labelX restX
-- fmap f empty = empty
= Begin (f x) (empty <|> empty)
-- empty <|> empty = empty
= Begin (f x) empty
-- Definition of `pure`, in reverse
--
-- pure label = Begin label empty
= pure (f x)
```

The fourth `Applicative`

law requires that:

`<*> pure y = pure ($ y) <*> u u `

Proof:

```
<*> pure y
u
-- Define:
--
-- u = Begin labelU0 (Choice us)
= Begin labelU0 (Choice us) <*> pure y
-- Definition of `pure`
--
-- pure label = Begin label empty
= Begin labelU0 (Choice us) <*> Begin y empty
-- Definition of `(<*>)`
= Begin (labelU0 y) (Choice (fmap adaptU us <|> fmap adaptY empty)
where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelUY restUY
adaptU (where
Yield labelUY restUY = Begin labelU restU <*> Begin y empty
Done result) = Done result
adaptY (Yield labelY restY) = Yield labelUY restUY
adaptY (where
Yield labelUY restUY = Begin labelU0 (Choice us) <*> Begin labelY restY
-- fmap f empty = empty
= Begin (labelU0 y) (Choice (fmap adaptU us))
where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelUY restUY
adaptU (where
Yield labelUY restUY = Begin labelU restU <*> Begin y empty
-- Definition of `pure`, in reverse
--
-- pure label = Begin label empty
= Begin (labelU0 y) (Choice (fmap adaptU us))
where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelUY restUY
adaptU (where
Yield labelUY restUY = Begin labelU restU <*> pure y
-- Induction: u <*> pure y = pure ($ y) <*> u
= Begin (labelU0 y) (Choice (fmap adaptU us))
where
Done result) = Done result
adaptU (Yield labelU restU) = Yield labelUY restUY
adaptU (where
Yield labelUY restUY = pure ($ y) <*> Begin labelU restU
-- Definition of `(<*>)`, in reverse
= Begin ($ y) empty <*> Begin labelU0 (Choice us)
-- Definition of `pure`, in reverse
= pure ($ y) <*> Begin labelU0 (Choice us)
-- Definition of `u`, in reverse:
--
-- u = Begin labelU0 (Choice us)
= pure ($ y) <*> u
```