Query Implementations with Reader Monads #
This file gives lemmas about QueryImpl spec m when m is something like ReaderT ρ n.
TODO: should generalize things to MonadReader 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?
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.
Instances For
def
QueryImpl.flattenReaderT
{ι : Type u_1}
{spec : OracleSpec ι}
{m : Type (max u_2 u_3) → Type u_4}
{ρ₁ ρ₂ : Type (max u_2 u_3)}
(impl : QueryImpl spec (ReaderT ρ₁ (ReaderT ρ₂ m)))
:
Reassociate a nested reader transformer into one product context.
The outer context is the first component of the product; the inner/base context is the
second. This is the reader-transformer analogue of flattenStateT and flattenWriterT.