First steps towards modeling PlusCal as a Haskell eDSL

HasCal.hs

{-# LANGUAGE ApplicativeDo               #-}
{-# LANGUAGE BlockArguments             #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances       #-}

module HasCal where

import Control.Applicative (Alternative(..), liftA2)
import Data.Void (Void)
import GHC.Exts (IsList(..))
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

{-| This is like the following PlusCal process code:

> begin
> A:
>   skip;
> B:
>   skip;
> C:
>   skip;
> end process
  
    Right now the only thing these Haskell processes can model from PlusCal is
    yielding at labeled checkpoints and `either`.  I'm still working on adding
    the other PlusCal features (like process-local state)
-}
strings :: Coroutine String
strings = Begin "A" do
    -- These skips are not necessary.  I only include them to make the Haskell
    -- code look more like the PlusCal code
    skip
    yield "B"
    skip
    yield "C"
    skip
    end

{-| Unlike PlusCal, we don't limit labels to strings.  They can be numbers, as
    in this example process

> begin
> 0:
>   skip;
> 1:
>   skip;
> 2:
>   skip;
> end process
-}
ints :: Coroutine Int
ints = Begin 0 do
    -- Here I omit the skips to show that they're really not necessary
    yield 1
    yield 2
    end

{-| You can combine processes in parallel using the `Applicative` instance for
    `Coroutine`.  This creates a new composite `Coroutine` with a composite
    label derived from their original labels.  The composite label can be
    any type we want, and in this case we just stick the primitive labels in a
    tuple for simplicity
-}
example :: Coroutine (String, Int)
example = do
    string <- strings
    int    <- ints
    return (string, int)

{-| If you run this file it will print the above composite process, which is
    essentially a tree of all possible timelines that the processes could take
    (i.e. all possible orders in which the processes interleave their valid
    atomic steps).  Along each path within the tree you can see how the
    composite label evolves:

> Begin
>   ( "A" , 0 )
>   [ Yield
>       ( "B" , 0 )
>       [ Yield ( "C" , 0 ) [ Yield ( "C" , 1 ) [ Yield ( "C" , 2 ) [] ] ]
>       , Yield
>           ( "B" , 1 )
>           [ Yield ( "C" , 1 ) [ Yield ( "C" , 2 ) [] ]
>           , Yield ( "B" , 2 ) [ Yield ( "C" , 2 ) [] ]
>           ]
>       ]
>   , Yield
>       ( "A" , 1 )
>       [ Yield
>           ( "B" , 1 )
>           [ Yield ( "C" , 1 ) [ Yield ( "C" , 2 ) [] ]
>           , Yield ( "B" , 2 ) [ Yield ( "C" , 2 ) [] ]
>           ]
>       , Yield ( "A" , 2 ) [ Yield ( "B" , 2 ) [ Yield ( "C" , 2 ) [] ] ]
>       ]
>   ]

    If you translate that `Coroutine` back into PlusCal, you get the following
    composite process (if you pretend that PlusCal can have labels other than
    strings):

> begin
> (A,0):
>   either
>     (B,0):
>       either
>         (C,0):
>           skip;
>         (C,1):
>           skip
>         (C,2):
>           skip
>       or
>         (B,1):
>           either
>             (C,1):
>               skip;
>             (C,2):
>           or
>             (B,2):
>               skip;
>             (C,2):
>               skip;
>           end either;
>       end either;
>   or
>     (A,1):
>       either
>         (B,1):
>           either
>             (C,1):
>               skip;
>             (C,2):
>               skip;
>           or
>             (B,2):
>               skip;
>             (C,2):
>               skip;
>           end either;
>       or
>         (A,2):
>           skip;
>         (B,2):
>           skip;
>         (C,2):
>           skip;
>       end either;
>   end either;
> end process
-}
main :: IO ()
main = Pretty.pPrint example

-- … and here is how the above examples work under the hood:

-- | A `Process` is a sequence of atomic steps, each of which can branch
--   non-deterministically (i.e. just like the `either` keyword in PlusCal)
--
--   PlusCal processes also have process-local state (not yet modeled here), so
--   currently all these Haskell processes can do is yield control and branch
--   non-deterministically
--
--   We model non-deterministic choice as a list of 0 or more valid atomic
--   `Step`s that the process could take
newtype Process label result = Choice [Step label result]
    deriving stock (Functor)
    deriving newtype (IsList, Show)

instance Applicative (Process label) where
    pure result = Choice (pure (Pure result))

    (<*>) = Monad.ap

instance Semigroup result => Semigroup (Process label result) where
    (<>) = liftA2 (<>)

instance Monoid result => Monoid (Process label result) where
    mempty = pure mempty

-- | The `Monad` instance for `Process` models sequencing actions in PlusCal
--
--   This instance obeys all of the `Monad` laws because it's isomorphic to the
--   `Monad` instance for `FreeT ((,) label) []`
instance Monad (Process label) where
    Choice ps >>= f = Choice do
        p <- ps
        case p of
            Yield label rest -> do
                return (Yield label (rest >>= f))
            Pure result -> do
                let Choice possibilities = f result
                possibilities

instance Alternative (Process label) where
    empty = Choice []

    Choice psL <|> Choice psR = Choice (psL <|> psR)

-- | At the end of each atomic `Step` we either `Yield` control with a
--   typed label or the process is `Pure`
--
--   Note that `Pure` is not the same thing as the `end` keyword in PlusCal.
--   `Pure` behaves like `pure`/`return` in Haskell, meaning "no-op"
data Step label result = Yield label (Process label result) | Pure result
    deriving stock (Functor, Show)

-- | A `Coroutine` is a `Process` enriched with a starting label
--
--   Just like in PlusCal, we need a starting label for each coroutine.  It
--   turns out that the starting label is also required from a theoretical
--   standpoint: the `Applicative` instance for `Coroutine` doesn't work without
--   it.
data Coroutine label = Begin label (Process label Void)
    deriving stock (Show)

instance Functor Coroutine where
    fmap = Applicative.liftA

-- | The `Applicative` instance for `Coroutine` models parallel composition
--   in such a way that the composite `Coroutine` has a composite label derived
--   from the input `Coroutine`s
--
--   Intuitively, parallel composition allows any `Coroutine` to make progress
--   whenever any `Coroutine` `yield`s control, just like in PlusCal
--
--   This is a novel `Applicative` instance that I haven't seen in the wild
--   before and this obeys all of the `Applicative` laws (I checked)
instance Applicative Coroutine where
    pure label = Begin label (Choice [])

    (<*>)
        f@(Begin label0F (Choice fs))
        x@(Begin label0X (Choice xs)) =
        Begin (label0F label0X) (Choice (fmap adaptF fs <|> fmap adaptX xs))
          where
            adaptF (Pure resultF) = Pure resultF
            adaptF (Yield labelF restF) = Yield labelFX restFX
              where
                Begin labelFX restFX = Begin labelF restF <*> x

            adaptX (Pure resultX) = Pure resultX
            adaptX (Yield labelX restX) = Yield labelFX restFX
              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

-- | This `yield` utility behaves just like a label in a PlusCal process
--
--   I call it `yield` since (just like in PlusCal) labels are the points at
--   which processes yield control to other processes.
yield :: label -> Process label ()
yield label = Choice [Yield label (pure ())]

{-| This plays the same role as the @skip@ keyword for a PlusCal process

    `skip` is just a synonym for `mempty`, meaning that the process only has
    a single valid transition that does nothing
-}
skip :: Process label ()
skip = mempty

{-| This plays the same role as the @end@ keyword for a PlusCal process

    `end` is just a synonym for `empty`, meaning that no additional transitions
    are possible (i.e. the empty set of 0 possible transitions)
-}
end :: Process label a
end = empty

{-| This plays the same role as the @either@ keyword for a PlusCal process

    `either` is just a synonym for `Foldable.asum`, which combines all of the
    possible transitions for each branch using (`<|>`)
-}
either :: [Process label result] -> Process label result
either = Foldable.asum

{-| This plays the same role as the @with@ keyword for a PlusCal process

    `with` non-deterministically chooses between the inputs, creating one
    branch per input
-}
with :: [result] -> Process label result
with results = either (map pure results)

{-| This plays the same role as the @while@ keyword for a PlusCal process

    @`while` condition body@ keeps running the @body@ of the loop until the
    condition fails
-}
while :: Process label Bool -> Process label () -> Process label ()
while condition body = do
    bool <- condition
    Monad.when bool do
        body
        while condition body

{-| This plays the same role as the @await@ keyword for a PlusCal process

    `await` is just a synonym for `Monad.guard`, which permits one transition
    if the condition is satisfied and no transition if the condition fails
-}
await :: Bool -> Process label ()
await = Monad.guard