Query Implementations with State Monads #
This file gives lemmas about QueryImpl spec m when m is something like StateT σ n.
TODO: should generalize things to MonadState once laws for it exist.
def
QueryImpl.addReaderT
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
{m : Type (max u_3 u_4) → Type u_5}
{ρ₁ ρ₂ : Type (max u_3 u_4)}
(impl₁ : QueryImpl spec₁ (ReaderT ρ₁ m))
(impl₂ : QueryImpl spec₂ (ReaderT ρ₂ m))
:
Given implementations for oracles in spec₁ and spec₂ in terms of reader monads for
two different contexts ρ₁ and ρ₂, implement the combined set spec₁ + spec₂ in terms
of a combined ρ₁ × ρ₂ state.
dtumad: should we call this an addition or multiplication operation?
Equations
Instances For
def
QueryImpl.sigmaReaderT
{τ : Type}
{ι : τ → Type u_1}
{spec : (t : τ) → OracleSpec (ι t)}
{m : Type u_2 → Type u_3}
{ρ : τ → Type u_2}
(impl : (t : τ) → QueryImpl (spec t) (ReaderT (ρ t) m))
:
QueryImpl (OracleSpec.sigma spec) (ReaderT ((t : τ) → ρ t) m)
Indexed version of QueryImpl.prodReader. Note that m cannot vary with t.