Instrumenting Monadic Handlers

This module provides effect-generic constructions for polynomial-functor handlers. liftTarget changes the target monad through MonadLiftT, while preInsert and postInsert add a side effect before or after each handled operation. The writer specializations record response-independent or response-dependent traces without depending on any oracle-specific API.

def PFunctor.Handler.liftTarget {P : PFunctor.{uA, u}} {m : Type u → Type v} (n : Type u → Type w) [MonadLiftT m n] (handler : Handler m P) : Handler n P

Lift every operation of a handler into a new target monad.

@[simp]

theorem PFunctor.Handler.liftTarget_apply {P : PFunctor.{uA, u}} {m : Type u → Type v} (n : Type u → Type w) [MonadLiftT m n] (handler : Handler m P) (operation : P.A) : liftTarget n handler operation = liftM (handler operation)

@[simp]

theorem PFunctor.Handler.liftTarget_self {P : PFunctor.{uA, u}} {m : Type u → Type v} (handler : Handler m P) : liftTarget m handler = handler

Lifting a handler to its current target has no effect.

def PFunctor.Handler.preInsert {P : PFunctor.{uA, u}} {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {α : Type u} (handler : Handler m P) (before : P.A → n α) : Handler n P

Run an effect before handling each operation.

The inserted effect is sequenced before the underlying handler. Whether its effects remain observable if that handler subsequently fails depends on the target monad's transformer order; for example, WriterT over Option discards the log together with a failed result. The inserted effect's value is discarded.

@[simp]

theorem PFunctor.Handler.preInsert_apply {P : PFunctor.{uA, u}} {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {α : Type u} (handler : Handler m P) (before : P.A → n α) (operation : P.A) : handler.preInsert before operation = before operation *> liftM (handler operation)

def PFunctor.Handler.postInsert {P : PFunctor.{uA, u}} {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {α : Type u} (handler : Handler m P) (after : (operation : P.A) → P.B operation → n α) : Handler n P

Run an effect after handling each operation.

The inserted effect may depend on the response and is skipped if the underlying handler fails. Its result is discarded.

@[simp]

theorem PFunctor.Handler.postInsert_apply {P : PFunctor.{uA, u}} {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {α : Type u} (handler : Handler m P) (after : (operation : P.A) → P.B operation → n α) (operation : P.A) : handler.postInsert after operation = do let response ← liftM (handler operation) let _ ← after operation response pure response

Writer traces

def PFunctor.Handler.withTraceBefore {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] (handler : Handler m P) (trace : P.A → ω) : Handler (WriterT ω m) P

Record a response-independent trace before each handled operation.

@[simp]

theorem PFunctor.Handler.withTraceBefore_apply {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] (handler : Handler m P) (trace : P.A → ω) (operation : P.A) : handler.withTraceBefore trace operation = do tell (trace operation) liftM (handler operation)

theorem PFunctor.Handler.withTraceBefore_eq_preInsert {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] (handler : Handler m P) (trace : P.A → ω) : handler.withTraceBefore trace = handler.preInsert fun (operation : P.A) => tell (trace operation)

Response-independent writer tracing is before-insertion of tell.

def PFunctor.Handler.withTrace {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) : Handler (WriterT ω m) P

Record a response-dependent trace after each handled operation.

@[simp]

theorem PFunctor.Handler.withTrace_apply {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) (operation : P.A) : handler.withTrace trace operation = do let response ← liftM (handler operation) tell (trace operation response) pure response

theorem PFunctor.Handler.withTrace_eq_postInsert {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) : handler.withTrace trace = handler.postInsert fun (operation : P.A) (response : P.B operation) => tell (trace operation response)

Response-dependent writer tracing is after-insertion of tell.

def PFunctor.Handler.withTraceAppendBefore {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] (handler : Handler m P) (trace : P.A → ω) : Handler (WriterT ω m) P

Append-flavoured response-independent tracing.

@[simp]

theorem PFunctor.Handler.withTraceAppendBefore_apply {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] (handler : Handler m P) (trace : P.A → ω) (operation : P.A) : handler.withTraceAppendBefore trace operation = do tell (trace operation) liftM (handler operation)

theorem PFunctor.Handler.withTraceAppendBefore_eq_preInsert {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] (handler : Handler m P) (trace : P.A → ω) : handler.withTraceAppendBefore trace = handler.preInsert fun (operation : P.A) => tell (trace operation)

Append-flavoured before-tracing is before-insertion of tell.

def PFunctor.Handler.withTraceAppend {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) : Handler (WriterT ω m) P

Append-flavoured response-dependent tracing.

@[simp]

theorem PFunctor.Handler.withTraceAppend_apply {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) (operation : P.A) : handler.withTraceAppend trace operation = do let response ← liftM (handler operation) tell (trace operation response) pure response

theorem PFunctor.Handler.withTraceAppend_eq_postInsert {P : PFunctor.{uA, u}} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) : handler.withTraceAppend trace = handler.postInsert fun (operation : P.A) (response : P.B operation) => tell (trace operation response)

Append-flavoured after-tracing is after-insertion of tell.