Safe Haskell	Safe
Language	GHC2021

LambdaUC.Syntax.Async

Contents

Interactive Algorithm Monad
Syntax
Interactive Computations
Step-by-step Execution
- Helper lemmas

Synopsis

type AsyncT = AsyncExT '[]
newtype AsyncExT ex ports bef aft a = AsyncExT {
- runInterT :: XFree (AsyncActions ex ports) bef aft a
}
data Exception = Type :@ Index
data Index
escapeAsyncT :: AsyncT '[] NextSend NextSend a -> PrAlgo a
xfreeAsync :: AsyncActions ex ports bef aft a -> AsyncExT ex ports bef aft a
data AsyncActions (ex :: [Exception]) (ports :: [Port]) (bef :: Index) (aft :: Index) (a :: Type) where
- RecvAction :: (SomeRxMess ports -> a) -> AsyncActions ex ports NextRecv NextSend a
- SendAction :: SomeTxMess ports -> a -> AsyncActions ex ports NextSend NextRecv a
- LiftAction :: PrAlgo x -> (x -> a) -> AsyncActions ex ports b b a
- ThrowAction :: InList ex (e :@ i) -> e -> AsyncActions ex ports i j a
send :: InList ports p -> PortTxType p -> AsyncExT ex ports NextSend NextRecv ()
sendMess :: SomeTxMess ports -> AsyncExT ex ports NextSend NextRecv ()
recvAny :: AsyncExT ex ports NextRecv NextSend (SomeRxMess ports)
xlift :: PrAlgo a -> AsyncExT ex ports i i a
xthrow :: InList ex (e :@ i) -> e -> AsyncExT ex ports i j a
xcatch :: forall ex ex' ports bef aft a. AsyncExT ex ports bef aft a -> (forall e b. InList ex (e :@ b) -> e -> AsyncExT ex' ports b aft a) -> AsyncExT ex' ports bef aft a
asyncGetIndex :: (XMonad m, KnownIndex b) => m b b (SIndex b)
asyncGuard :: XMonad m => SIndex b -> m b b ()
recvOneEx :: InList ex (e :@ NextSend) -> e -> PortInList x y ports -> AsyncExT ex ports NextRecv NextSend y
recvOne :: AsyncExT ex '[x :> y] NextRecv NextSend y
sendOne :: x -> AsyncExT ex '[x :> y] NextSend NextRecv ()
runTillSend :: AsyncT ports NextSend b a -> PrAlgo (SendRes ports b a)
data SendRes ports aft a where
- SrSend :: SomeTxMess ports -> AsyncT ports NextRecv aft a -> SendRes ports aft a
- SrHalt :: a -> SendRes ports NextSend a
runTillRecv :: AsyncT ports NextRecv b a -> PrAlgo (RecvRes ports b a)
data RecvRes ports aft a where
- RrRecv :: (SomeRxMess ports -> AsyncT ports NextSend aft a) -> RecvRes ports aft a
- RrHalt :: a -> RecvRes ports NextRecv a
mayOnlyRecvVoidPrf :: RecvRes ports aft Void -> SomeRxMess ports -> AsyncT ports NextSend aft Void
mayOnlySendVoidPrf :: SendRes ports aft Void -> (SomeTxMess ports, AsyncT ports NextRecv aft Void)

Interactive Algorithm Monad

type AsyncT = AsyncExT '[] #

newtype AsyncExT ex ports bef aft a #

The monad for expressing interactive algorithms.

By instantiating AsyncT with different parameters, you can finely control what side-effects you allow:

Asynchronous (send and recvAny) communcation over interfaces defined in ports.

Asynchronous communcation depends on the Index state of AsyncT. There are two possible index states which are interpreted as follows.

NextSend means that it's our turn to send.
NextRecv means that it's our turn to receive (we currently have one message in our inbox).

The states NextSend and NextRecv are toggled with send and recvAny. Any asyncronous algorithm will alternate between send and recvAny some number of times, until it terminates. Such algorithm's indices tell which of the two operations must be first and last.

Additionally, you may sample random values in AsyncT using rand.

Constructors

AsyncExT
Fields runInterT :: XFree (AsyncActions ex ports) bef aft a

Instances

Instances details

XApplicative (AsyncExT ex ports :: Index -> Index -> Type -> Type) #
Instance details Defined in LambdaUC.Syntax.Async Methods xpure :: forall a (p :: k). a -> AsyncExT ex ports p p a # (<>:) :: forall (p :: k) (q :: k) a b (r :: k). AsyncExT ex ports p q (a -> b) -> AsyncExT ex ports q r a -> AsyncExT ex ports p r b # xliftA2 :: forall a b c (p :: k) (q :: k) (r :: k). (a -> b -> c) -> AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r c # (>:) :: forall (p :: k) (q :: k) a (r :: k) b. AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r b # (<*:) :: forall (p :: k) (q :: k) a (r :: k) b. AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r a #
XMonad (AsyncExT ex ports :: Index -> Index -> Type -> Type) #
Instance details Defined in LambdaUC.Syntax.Async Methods (>>=:) :: forall a b (p :: k) (q :: k) (r :: k). AsyncExT ex ports p q a -> (a -> AsyncExT ex ports q r b) -> AsyncExT ex ports p r b # (>>:) :: forall a b (p :: k) (q :: k) (r :: k). AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r b # xreturn :: forall a (p :: k). a -> AsyncExT ex ports p p a #
bef ~ aft => Applicative (AsyncExT ex ports bef aft) #
Instance details Defined in LambdaUC.Syntax.Async Methods pure :: a -> AsyncExT ex ports bef aft a # (<>) :: AsyncExT ex ports bef aft (a -> b) -> AsyncExT ex ports bef aft a -> AsyncExT ex ports bef aft b # liftA2 :: (a -> b -> c) -> AsyncExT ex ports bef aft a -> AsyncExT ex ports bef aft b -> AsyncExT ex ports bef aft c # (>) :: AsyncExT ex ports bef aft a -> AsyncExT ex ports bef aft b -> AsyncExT ex ports bef aft b # (<*) :: AsyncExT ex ports bef aft a -> AsyncExT ex ports bef aft b -> AsyncExT ex ports bef aft a #
Functor (AsyncExT ex ports bef aft) #
Instance details Defined in LambdaUC.Syntax.Async Methods fmap :: (a -> b) -> AsyncExT ex ports bef aft a -> AsyncExT ex ports bef aft b # (<$) :: a -> AsyncExT ex ports bef aft b -> AsyncExT ex ports bef aft a #
bef ~ aft => Monad (AsyncExT ex ports bef aft) #
Instance details Defined in LambdaUC.Syntax.Async Methods (>>=) :: AsyncExT ex ports bef aft a -> (a -> AsyncExT ex ports bef aft b) -> AsyncExT ex ports bef aft b # (>>) :: AsyncExT ex ports bef aft a -> AsyncExT ex ports bef aft b -> AsyncExT ex ports bef aft b # return :: a -> AsyncExT ex ports bef aft a #
MonadRand (AsyncExT ex ports i i) #
Instance details Defined in LambdaUC.Syntax.Async Methods rand :: AsyncExT ex ports i i Bool #

data Exception #

Constructors

Type :@ Index

data Index #

Next operation of the asyncronous algorithm

Instances

Instances details

XApplicative (AsyncExT ex ports :: Index -> Index -> Type -> Type) #
Instance details Defined in LambdaUC.Syntax.Async Methods xpure :: forall a (p :: k). a -> AsyncExT ex ports p p a # (<>:) :: forall (p :: k) (q :: k) a b (r :: k). AsyncExT ex ports p q (a -> b) -> AsyncExT ex ports q r a -> AsyncExT ex ports p r b # xliftA2 :: forall a b c (p :: k) (q :: k) (r :: k). (a -> b -> c) -> AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r c # (>:) :: forall (p :: k) (q :: k) a (r :: k) b. AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r b # (<*:) :: forall (p :: k) (q :: k) a (r :: k) b. AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r a #
XMonad (AsyncExT ex ports :: Index -> Index -> Type -> Type) #
Instance details Defined in LambdaUC.Syntax.Async Methods (>>=:) :: forall a b (p :: k) (q :: k) (r :: k). AsyncExT ex ports p q a -> (a -> AsyncExT ex ports q r b) -> AsyncExT ex ports p r b # (>>:) :: forall a b (p :: k) (q :: k) (r :: k). AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r b # xreturn :: forall a (p :: k). a -> AsyncExT ex ports p p a #

escapeAsyncT :: AsyncT '[] NextSend NextSend a -> PrAlgo a #

Interactive action with no free ports can be interpreted as local.

Apply this function once you've bound all the free ports to run the execution.

xfreeAsync :: AsyncActions ex ports bef aft a -> AsyncExT ex ports bef aft a #

Syntax

Actions are given in Free monad syntax.

data AsyncActions (ex :: [Exception]) (ports :: [Port]) (bef :: Index) (aft :: Index) (a :: Type) where #

bef and aft are the states before and after the given action. The meaning of possible states is as follows:

Constructors

RecvAction :: (SomeRxMess ports -> a) -> AsyncActions ex ports NextRecv NextSend a	Receive a message from some channel
SendAction :: SomeTxMess ports -> a -> AsyncActions ex ports NextSend NextRecv a	Send a message to the chosen channel
LiftAction :: PrAlgo x -> (x -> a) -> AsyncActions ex ports b b a	Run a local action in the inner monad.
ThrowAction :: InList ex (e :@ i) -> e -> AsyncActions ex ports i j a	Throw one of the allowed exceptions

Instances

Instances details

Functor (AsyncActions ex ports bef aft) #
Instance details Defined in LambdaUC.Syntax.Async Methods fmap :: (a -> b) -> AsyncActions ex ports bef aft a -> AsyncActions ex ports bef aft b # (<$) :: a -> AsyncActions ex ports bef aft b -> AsyncActions ex ports bef aft a #

Interactive Computations

Side-effects available to both syncronous and asynchronous interactive algorithms: reading the current state of the write token, throwing write-token-aware exceptions.

Side-effects of an asynchronous interactive algorithm. Such an algorithm can:

send a message to a chosen recepient,
receive message from a receiver.

Note that sending a message does not require the recepient to respond (now or later). When receiving a message, we must be ready that it can arrive from anyone — as the exact order of messages can not be predicted at compile time.

send :: InList ports p -> PortTxType p -> AsyncExT ex ports NextSend NextRecv () #

Curried version of sendMess.

sendMess :: SomeTxMess ports -> AsyncExT ex ports NextSend NextRecv () #

Send a message to the port it is marked with.

recvAny :: AsyncExT ex ports NextRecv NextSend (SomeRxMess ports) #

Receive the next message which can arrive from any of port ports.

xlift :: PrAlgo a -> AsyncExT ex ports i i a #

xthrow :: InList ex (e :@ i) -> e -> AsyncExT ex ports i j a #

xcatch #

Arguments

:: forall ex ex' ports bef aft a. AsyncExT ex ports bef aft a	The computation that may throw an exception
-> (forall e b. InList ex (e :@ b) -> e -> AsyncExT ex' ports b aft a)	How to handle the exception
-> AsyncExT ex' ports bef aft a

asyncGetIndex :: (XMonad m, KnownIndex b) => m b b (SIndex b) #

Wrapper around getSIndex that tells you what context you're in.

asyncGuard :: XMonad m => SIndex b -> m b b () #

The following definitions specialize AsyncT for narrower use-cases. These definitions should suffice for most of the programs you'd want to write.

recvOneEx :: InList ex (e :@ NextSend) -> e -> PortInList x y ports -> AsyncExT ex ports NextRecv NextSend y #

recvOne :: AsyncExT ex '[x :> y] NextRecv NextSend y #

sendOne :: x -> AsyncExT ex '[x :> y] NextSend NextRecv () #

Step-by-step Execution

The following functions let you evaluate an interactive algorithm step-by-step. An algorithm in NextSend state can be ran until it sends something (or halts, or does an oracle call) via runTillSend, and an algorithm in NextRecv state can be executed until it reqests a message for reception (or halts, or does an oracle call) via runTillRecv.

Functions runTillSend and runTillRecv correspond to activation of an Interactive Turing Machine.

runTillSend :: AsyncT ports NextSend b a -> PrAlgo (SendRes ports b a) #

Given AsyncT action starting in NextSend state (holding write token), run it until it does send or halts.

data SendRes ports aft a where #

The result of runTillSend

Constructors

SrSend :: SomeTxMess ports -> AsyncT ports NextRecv aft a -> SendRes ports aft a	Algorithm called `send`.
SrHalt :: a -> SendRes ports NextSend a	Algorithm called `sendFinal`.

runTillRecv :: AsyncT ports NextRecv b a -> PrAlgo (RecvRes ports b a) #

Given an action that starts in a NextRecv state (no write token), run it until it receives the write token via recvAny or halts.

data RecvRes ports aft a where #

The result of runTillRecv.

Constructors

RrRecv :: (SomeRxMess ports -> AsyncT ports NextSend aft a) -> RecvRes ports aft a	Algorithm ran `recvAny`.
RrHalt :: a -> RecvRes ports NextRecv a	Algorithm has halted without accepting a message

Helper lemmas

These lemmas make it easier to extract the contents of RecvRes and SendRes in cases when types guarrantee that these values can be deconstructed in only one way (i.e. there is only one value constrctor that could have produces the value of this type).

These helpers allow (when applicable) you to write a sequence of runTillRecv and runTillSend in a linear fashion. You can do

do
  x <- mayOnlyRecvVoidPrf <$> runTillRecv _ _
  (y, cont) <- mayOnlySendVoidPrf <$> runTillSend _
  _

instead of manually proving that some constructors are impossible as below.

do
  runTillRecv _ _ >>= case
    RrHalt contra -> case contra of {}
    RrRecv x -> do
      runTillSend _ >>= case
        SrHalt contra -> case contra of {}
        SrSend y cont -> do
          _

mayOnlyRecvVoidPrf :: RecvRes ports aft Void -> SomeRxMess ports -> AsyncT ports NextSend aft Void #

Proof: A program with sync ports and return type Void may not terminate; if it starts from NextRecv state, it will inevitably request an rx message.

mayOnlySendVoidPrf :: SendRes ports aft Void -> (SomeTxMess ports, AsyncT ports NextRecv aft Void) #

Proof: A program with sync ports and return type Void may not terminate; if it starts from NextSend state, it will inevitably request to send a message.