Oracle-signature inclusions #
Polynomial lenses implement oracle-signature inclusions. Cartesian response translations preserve operational possibilities; semantic preservation is expressed separately by the chosen measures.
Inclusion of one set of oracles into another, packaged as a polynomial-functor
lens between the underlying OracleSpecs. Carries the forward translation
onQuery on query inputs and the fiberwise backward translation onResponse
on query responses, plus the resulting MonadLift action.
The MonadLift action and the lens data are related by the public coherence equation
liftM_eq_lift. Concrete inclusions supply their query action alongside the query and response
translations. SubSpec.liftQuery and SubSpec.toLens expose those constructions independently of
any measure interpretation.
Informally, spec ⊂ₒ superSpec says that any query to an oracle of spec
can be perfectly simulated by a query to an oracle of superSpec. We avoid
the built-in Subset notation because we care about the actual data of the
mapping (it is needed when defining type coercions), not just its existence.
Forward translation on query inputs (oracle indices).
Fiberwise backward translation on query responses.
- liftM_eq_lift {β : Type w} (q : OracleQuery spec β) : MonadLift.monadLift q = ⟨onQuery q.input, q.cont ∘ onResponse q.input⟩
Instances
Inclusion of one set of oracles into another, packaged as a polynomial-functor
lens between the underlying OracleSpecs. Carries the forward translation
onQuery on query inputs and the fiberwise backward translation onResponse
on query responses, plus the resulting MonadLift action.
The MonadLift action and the lens data are related by the public coherence equation
liftM_eq_lift. Concrete inclusions supply their query action alongside the query and response
translations. SubSpec.liftQuery and SubSpec.toLens expose those constructions independently of
any measure interpretation.
Informally, spec ⊂ₒ superSpec says that any query to an oracle of spec
can be perfectly simulated by a query to an oracle of superSpec. We avoid
the built-in Subset notation because we care about the actual data of the
mapping (it is needed when defining type coercions), not just its existence.
Instances For
The lens action on a single query: forward on the input, post-compose the
backward fiber on the continuation. Used as the canonical reduced form of
liftM q for proofs that need to inspect the resulting query.
Instances For
The polynomial-functor lens between the underlying PFunctors carried by
a SubSpec instance. This is the lens-level view of the data; concrete
properties (like cartesianness via LawfulSubSpec) are stated on this lens.
The other half of the data, monadLift, is fixed by liftM_eq_lift to be
the standard action of this lens on OracleQuery.
Instances For
Transitivity of SubSpec: lens composition.
Instances For
LawfulSubSpec extends SubSpec with the requirement that the backward
translation onResponse is bijective on every fiber. Equivalently: the
underlying lens SubSpec.toLens is cartesian in the sense of
PFunctor.Lens.IsCartesian, i.e. it is a fiberwise isomorphism over an
arbitrary forward map on positions.
This is strictly weaker than PFunctor.Lens.Equiv, which would also force
onQuery to be a bijection. We intentionally only require fiberwise
bijectivity because the canonical SubSpec instances embed a small spec
into a larger one (e.g. spec₁ ⊂ₒ (spec₁ + spec₂) with onQuery = Sum.inl),
and these embeddings are essential to the API.
Cartesianness preserves operational possibilities and permits transport of uniform measures.
Preservation of arbitrary weighted measures is a separate semantic contract. The public
LawfulSubSpec.toLens_isCartesian equation exposes the polynomial lens certificate.
- onResponse_bijective (t : spec.Domain) : Function.Bijective (SubSpec.onResponse t)
The backward translation is bijective on every fiber.
Instances
Lawful oracle-spec inclusion: a SubSpec whose response translation is
bijective on every fiber.
Instances For
The lens-level statement of LawfulSubSpec: the underlying
PFunctor.Lens is cartesian. This makes the dictionary between the
oracle-spec layer and the polynomial-functor lens layer explicit.
Two oracle-spec inclusions into the same ambient spec have disjoint query images.
Lawfulness concerns bijective response translations, while disjointness says the two lifted query namespaces do not overlap inside the ambient interface.
The two forward query maps have disjoint images.
Instances
Oracle-spec inclusions with disjoint query images in an ambient interface.
Instances For
Lifting a primitive query through a signature inclusion first translates the query and then inserts it into the target free program.
Lift a computation from spec to superSpec using a SubSpec instance on queries.
Usually liftM should be preferred but this can allow more explicit annotation.
Instances For
Signature translation of a primitive query is its query lift.
bind-pure form of liftComp_map, matching the term shape produced by do-notation
(do let a ← oa; pure (f a)) before any bind_pure_comp normalization.
One-directional, assumption-light variant of mem_support_liftComp_iff: under just a
query-level lift (no SubSpec or lawfulness assumptions), the support of a lifted computation
is bounded by the support of the original. The reverse inclusion can fail without lawfulness,
since an arbitrary embedding need not reach all responses of the original oracles.
Support is preserved by liftComp: lifting a computation to a larger oracle spec
does not change which outputs are reachable. This is the support analogue of
the native uniform-measure lifting law.
Extend a lifting on OracleQuery to a lifting on OracleComp.
Registered as a low-priority MonadLift (not MonadLiftT) so that:
For
spec = superSpec, Lean's built-inMonadLiftT.refl(which is definitionallyid) wins typeclass resolution. This is whatStd.Do.Spec.UnfoldLift.monadLift_refl(arfl-based lemma) needs in order to peel off spurious self-lifts insidemvcgen-elaborated terms.For
MonadLiftT (OracleQuery spec) (OracleComp superSpec), the built-in high-priorityMonadLift (OracleQuery superSpec) (OracleComp superSpec)is tried first bymonadLiftTransand succeeds via theSubSpecchain onOracleQuery, never reaching this instance. Single-query lifts therefore go through the standard "lift query then embed" path with no spurious walk throughliftComp.For
MonadLiftT (OracleComp spec) (OracleComp superSpec)withspec ≠ superSpec, the high-priority built-in fails (noMonadLiftT (OracleComp _) (OracleQuery _)), Lean backtracks to this low-priority instance, and the recursive subgoal collapses viaMonadLiftT.refl. The result is a singleliftComp mx superSpec.
We choose to actively rewrite liftComp as liftM to enable LawfulMonadLift lemmas.
Peel the outermost step off a chained OracleComp-level lift: a liftM whose
MonadLiftT (OracleComp spec) (OracleComp spec₃) instance is the transitive composition of
the query-keyed MonadLift (OracleComp superSpec) (OracleComp spec₃) step with a remaining
chain MonadLiftT (OracleComp spec) (OracleComp superSpec) is the liftComp of the
remaining lift. Typeclass resolution builds exactly this shape (via
instMonadLiftTOfMonadLift) when lifting across two or more OracleSpec.add layers, e.g.
OracleComp spec₂ → OracleComp (spec + (spec₁ + spec₂)) through the intermediate
spec + spec₂. None of the single-step lemmas (liftComp_eq_liftM, liftComp_query, …)
can engage such a chain directly, since their statements bake in the one-step instance.
Not @[simp]: with spec = superSpec the remaining chain can be MonadLiftT.refl, and the
right-hand side would then re-match the left-hand side. Use via explicit rw, then rewrite
the inner lift with ← liftComp_eq_liftM and proceed with the liftComp API.
Self-lift on OracleComp is definitionally id, supplied by Lean's
built-in MonadLiftT.refl thanks to the low-priority MonadLift instance
above (which causes the parametric path to lose typeclass resolution to
MonadLiftT.refl when spec = superSpec).
Regression smoke-tests for the instance-priority invariants above. The
rfl proofs are the load-bearing signal: if priority drifts so that the
parametric MonadLift beats MonadLiftT.refl, the self-lift stops being
definitionally id and the rfl below breaks. Similarly, the
MonadLiftT synthesis check guards against future refactors that would
remove the transitive lift chain.
Coherence: lifting an OracleComp to a superspec and then into OptionT via the standard
MonadLift equals lifting directly through the transitive MonadLiftT chain (which goes
through the simulateQ-based OptionT MonadLift instance).