| Safe Haskell | Safe |
|---|---|
| Language | GHC2021 |
LambdaUC.Syntax.Sync.Eval
Contents
Synopsis
- runWithOracles :: forall m (down :: [Port]) (rets :: [Type]) a. SameLen down rets => OracleCaller down a -> HList2 OracleWrapper down rets -> MaybeT PrAlgo (a, HList Identity rets)
- type OracleCaller down = SyncT down PrAlgo
- newtype OracleWrapper (up :: Port) (ret :: Type) = OracleWrapper {
- runOracleWrapper :: Oracle up ret
- type Oracle (up :: Port) = AsyncT '[PortRxType up :> OracleReq (PortTxType up)] NextRecv NextSend
- data OracleReq a
- = OracleReqHalt
- | OracleReq a
- runWithOracles1 :: OracleCaller '[x :> y] a -> OracleWrapper (x :> y) b -> MaybeT PrAlgo (a, b)
- runWithOracles2 :: OracleCaller '[x :> y, x' :> y'] a -> OracleWrapper (x :> y) b -> OracleWrapper (x' :> y') b' -> MaybeT PrAlgo (a, b, b')
Execution with Oracle
The following are definitions related to running an algorithm with an given
oracle. The runWithOracles executes an algorithm with an oracle, while
OracleCaller and OracleWrapper are convenient type synonyms
for the interactive algorithms that define the oracle caller and oracle
respectively.
The oracle is expected to terminate and produce the result s right after
receiving special request OracleReqHalt, but not before then. If the
oracle violates this condition, the runWithOracles fails with mzero. To
differentiate between service OracleReqHalt and the regular queries from
the algorithm, we wrap the latter in OracleReq type.
Arguments
| :: forall m (down :: [Port]) (rets :: [Type]) a. SameLen down rets | |
| => OracleCaller down a | The oracle caller algorithm |
| -> HList2 OracleWrapper down rets | The implementations of oracles available to caller |
| -> MaybeT PrAlgo (a, HList Identity rets) | The outputs of caller and oracle. Fails with |
Given main algorithm top and a list of oracle algorithms bot,
`runWithOracles top bot` will run them together (top querying any oracle
the oracles in bot) and return their results.
The top returns its result directly when terminating, then a special
OracleReqHalt message is sent to all of bot to ask them to terminate and
return their results.
We throw a mzero error in case an oracle does not follow the termination
condition: terminates before receiving OracleReqHalt or tries to respond
to OracleReqHalt instead of terminating.
Note that runWithOracles passes all the messages between the running
interactive algorithms, therefore its result is a non-interactive algorithm.
type OracleCaller down = SyncT down PrAlgo #
An algorithm with no parent and with access to child oracles given by
down.
newtype OracleWrapper (up :: Port) (ret :: Type) #
Constructors
| OracleWrapper | |
Fields
| |
type Oracle (up :: Port) = AsyncT '[PortRxType up :> OracleReq (PortTxType up)] NextRecv NextSend #
An algorithm serving oracle calls from parent, but not having access to any oracles of its own.
Constructors
| OracleReqHalt | |
| OracleReq a |
runWithOracles1 :: OracleCaller '[x :> y] a -> OracleWrapper (x :> y) b -> MaybeT PrAlgo (a, b) #
Version of runWithOracles that accepts only one oracle
runWithOracles2 :: OracleCaller '[x :> y, x' :> y'] a -> OracleWrapper (x :> y) b -> OracleWrapper (x' :> y') b' -> MaybeT PrAlgo (a, b, b') #
Version of runWithOracles that accepts two oracles