Monadic Handlers for Polynomial Functors

A PFunctor.Handler m q chooses a direction of q at each position, with the choice interpreted in the type constructor m. This is the generic interface consumed by FreeM.liftM; it does not depend on machines or dynamical systems. In particular, taking m := StateT σ n threads one shared runtime state through every handled position. That ambient state is distinct from a dynamical system's private operational state.

@[reducible, inline]

abbrev PFunctor.Handler (m : Type u → Type v) (q : PFunctor.{uA, u}) : Type (max v uA)

A handler for the interface q: a monadic choice of direction at each position (a Kleisli section of q). With m := Id this is an ordinary dependent choice of one direction at every position, while a probabilistic monad gives a randomized choice.

def PFunctor.Handler.mapTarget {m : Type u → Type v} {n : Type u → Type w} {q : PFunctor.{uA, u}} (transform : {α : Type u} → m α → n α) (handler : Handler m q) : Handler n q

Postcompose every answer computation of a handler by a polymorphic map between target type constructors. No monad laws are needed for this basic change-of-target operation.

@[simp]

theorem PFunctor.Handler.mapTarget_apply {m : Type u → Type v} {n : Type u → Type w} {q : PFunctor.{uA, u}} (transform : {α : Type u} → m α → n α) (handler : Handler m q) (position : q.A) : mapTarget (fun {α : Type u} => transform) handler position = transform (handler position)

@[simp]

theorem PFunctor.Handler.mapTarget_id {m : Type u → Type v} {q : PFunctor.{uA, u}} (handler : Handler m q) : mapTarget (fun {α : Type u} (computation : m α) => computation) handler = handler

theorem PFunctor.Handler.mapTarget_comp {m : Type u → Type v} {n : Type u → Type w} {o : Type u → Type uI} {q : PFunctor.{uA, u}} (second : {α : Type u} → n α → o α) (first : {α : Type u} → m α → n α) (handler : Handler m q) : mapTarget (fun {α : Type u} => second) (mapTarget (fun {α : Type u} => first) handler) = mapTarget (fun {α : Type u} (computation : m α) => second (first computation)) handler

@[reducible, inline]

abbrev PFunctor.Handler.Stateful (m : Type u → Type v) (S : Type u) (q : PFunctor.{uA, u}) : Type (max (max v u) uA)

An effectful stateful handler for q: on each position it reads a state, performs effects in m, and returns a direction together with the next state.

This is a transparent name for Handler (StateT S m) q, so it introduces no new data or laws. At m := Id it is the pure Kleisli--Mealy presentation used by Responder.equivStateHandler.

def PFunctor.Handler.sigma {I : Type uI} {P : I → PFunctor.{uA, u}} {m : Type u → Type v} (f : (i : I) → Handler m (P i)) : Handler m (PFunctor.sigma P)

Combine monadic handlers for an indexed family into a handler for its indexed coproduct.

@[simp]

theorem PFunctor.Handler.sigma_apply {I : Type uI} {P : I → PFunctor.{uA, u}} {m : Type u → Type v} (f : (i : I) → Handler m (P i)) (i : I) (a : (P i).A) : sigma f ⟨i, a⟩ = f i a