Reader Selection Monad

A pure mathematical monad: a family of functions indexed by ι, composed with a data-dependent selector. This is the Reader monad with indexed selection.

The three monad laws hold definitionally (by rfl).

This structure underlies MeasurableBatchLearner composition in the learning theory layer, but the monad itself is pure mathematics with zero dependencies.

structure ReaderSel (ι : Type u) (α : Type v) (γ : Type w) : Type (max (max u v) w)

A reader-selection computation: family indexed by ι, selected by data.

• family : ι → α → γ

  Family of functions available to the selector.

• sel : α → ι

  Data-dependent selector for the family index.

def ReaderSel.eval {ι : Type u} {α : Type v} {γ : Type w} (r : ReaderSel ι α γ) (a : α) : γ

Evaluate: apply the selected family member.

Equations

• r.eval a = r.family (r.sel a) a

def ReaderSel.pure {ι : Type u} {α : Type v} {γ : Type w} (i₀ : ι) (f : α → γ) : ReaderSel ι α γ

Pure: constant family (selector is irrelevant).

Equations

• ReaderSel.pure i₀ f = { family := fun (x : ι) => f, sel := fun (x : α) => i₀ }

def ReaderSel.bind {ι : Type u} {α : Type v} {γ : Type w} (r : ReaderSel ι α γ) (f : γ → ReaderSel ι α γ) : ReaderSel ι α γ

Bind: the second computation may depend on the first's output. eval (bind r f) a = eval (f (eval r a)) a

Equations

• r.bind f = { family := fun (i : ι) (a : α) => (f (r.family (r.sel a) a)).family i a, sel := fun (a : α) => (f (r.family (r.sel a) a)).sel a }

theorem ReaderSel.left_unit {ι : Type u} {α : Type v} {γ : Type w} (i₀ : ι) (f : α → γ) (g : γ → ReaderSel ι α γ) (a : α) : ((pure i₀ f).bind g).eval a = (g (f a)).eval a

Left unit: bind (pure f) g a = (g (f a)).eval a

theorem ReaderSel.right_unit {ι : Type u} {α : Type v} {γ : Type w} (r : ReaderSel ι α γ) (i₀ : ι) (a : α) : (r.bind fun (v : γ) => pure i₀ fun (x : α) => v).eval a = r.eval a

Right unit: bind r (fun v => pure (const v)) a = r.eval a

theorem ReaderSel.assoc {ι : Type u} {α : Type v} {γ : Type w} (r : ReaderSel ι α γ) (f g : γ → ReaderSel ι α γ) (a : α) : ((r.bind f).bind g).eval a = (r.bind fun (v : γ) => (f v).bind g).eval a

Associativity: bind (bind r f) g = bind r (fun v => bind (f v) g)