Safe Haskell	Safe
Language	GHC2021

LambdaUC.Syntax.Sync

Contents

Interactive Algorithm Monad
Syntax
Step-by-step Execution

Synopsis

newtype SyncT sch m a = SyncT {
- runSyncT :: Free (SyncActions sch m) a
}
freeSync :: SyncActions sch m a -> SyncT sch m a
lift :: (MonadTrans t, Monad m) => m a -> t m a
call :: PortInList x y down -> x -> SyncT down m y
data SyncActions (sch :: [Port]) (m :: Type -> Type) a where
- CallAction :: PortInList x y sch -> x -> (y -> a) -> SyncActions sch m a
- LiftAction :: m x -> (x -> a) -> SyncActions sch m a
runTillCall :: Monad m => SyncT sch m a -> m (CallRes sch m a)
data CallRes (sch :: [Port]) (m :: Type -> Type) a where
- CrCall :: PortInList x y sch -> x -> (y -> SyncT sch m a) -> CallRes sch m a
- CrHalt :: a -> CallRes sch m a

Interactive Algorithm Monad

newtype SyncT sch m a #

Non-indexed transformer that adds syncronous call (ports given by sch) to monad m (lifted with lift). You will often see Algo used as m, and SyncT will automatically implement its typeclasses such as Print or Rand.

If you need exceptions in SyncT, feel free to use regular monadic mechanisms such as ExceptT or MaybeT.

SyncT only adds syntax for synchronous interaction, therefore (unlike AsyncT) it is a regular monad, not an indexed one. Consider code below for an example. The function reportSum has access to to oracles: oracle A with requests of type String, and responses of type Int; and oracle B with request of type () and responses of type String.

  reportSum :: SyncT m '[P String Int, P () String] (Int, String)
  reportSum = do
    let a = Here
        b = There Here
    x <- call a "hello"
    y <- call a "world"
    z <- call b ()
    return (x + y, z)

To run the code above, implement the oracles and use runWithOracles2.

Constructors

SyncT
Fields runSyncT :: Free (SyncActions sch m) a

Instances

Instances details

MonadTrans (SyncT sch) #
Instance details Defined in LambdaUC.Syntax.Sync Methods lift :: Monad m => m a -> SyncT sch m a #
Applicative (SyncT sch m) #
Instance details Defined in LambdaUC.Syntax.Sync Methods pure :: a -> SyncT sch m a # (<>) :: SyncT sch m (a -> b) -> SyncT sch m a -> SyncT sch m b # liftA2 :: (a -> b -> c) -> SyncT sch m a -> SyncT sch m b -> SyncT sch m c # (>) :: SyncT sch m a -> SyncT sch m b -> SyncT sch m b # (<*) :: SyncT sch m a -> SyncT sch m b -> SyncT sch m a #
Functor (SyncT sch m) #
Instance details Defined in LambdaUC.Syntax.Sync Methods fmap :: (a -> b) -> SyncT sch m a -> SyncT sch m b # (<$) :: a -> SyncT sch m b -> SyncT sch m a #
Monad (SyncT sch m) #
Instance details Defined in LambdaUC.Syntax.Sync Methods (>>=) :: SyncT sch m a -> (a -> SyncT sch m b) -> SyncT sch m b # (>>) :: SyncT sch m a -> SyncT sch m b -> SyncT sch m b # return :: a -> SyncT sch m a #

freeSync :: SyncActions sch m a -> SyncT sch m a #

lift :: (MonadTrans t, Monad m) => m a -> t m a #

Lift a computation from the argument monad to the constructed monad.

call :: PortInList x y down -> x -> SyncT down m y #

Syntax

Actions are given in Free monad syntax.

data SyncActions (sch :: [Port]) (m :: Type -> Type) a where #

Constructors

CallAction :: PortInList x y sch -> x -> (y -> a) -> SyncActions sch m a	Perform a call to a child, immediately getting the result
LiftAction :: m x -> (x -> a) -> SyncActions sch m a	Run a local action in the inner monad.

Instances

Instances details

Functor (SyncActions sch m) #
Instance details Defined in LambdaUC.Syntax.Sync Methods fmap :: (a -> b) -> SyncActions sch m a -> SyncActions sch m b # (<$) :: a -> SyncActions sch m b -> SyncActions sch m a #

Step-by-step Execution

The following functions let you evaluate a synchronous algorithm step-by-step.

runTillCall :: Monad m => SyncT sch m a -> m (CallRes sch m a) #

Given SyncT action starting in True state (holding write token), run it until it does call or halts.

data CallRes (sch :: [Port]) (m :: Type -> Type) a where #

The result of runTillCall

Constructors

CrCall :: PortInList x y sch -> x -> (y -> SyncT sch m a) -> CallRes sch m a	Algorithm called `call`.
CrHalt :: a -> CallRes sch m a	Algorithm halted without a `call`