Effect algebra for interaction trees

This module provides the algebra of effects used to combine and interpret interaction trees: natural transformations between effect families, the empty and sum effects (VoidE, SumE), the MonadIter class of iterable monads, the iter iteration combinator, and the interp interpretation of an ITree against an effect handler into an arbitrary iterable monad.

@[reducible, inline]

abbrev Lean4Itree.naturalTransformation (ε1 : Type u → Type v1) (ε2 : Type u → Type v2) : Type (max (max (u + 1) v1) v2)

A natural transformation between effect families: a uniform map ε1 α → ε2 α.

Equations

• Lean4Itree.naturalTransformation ε1 ε2 = ({α : Type ?u.3} → ε1 α → ε2 α)

def Lean4Itree.«term_⟶_» : Lean.TrailingParserDescr

Notation ε1 ⟶ ε2 for a natural transformation between effect families.

Equations

• Lean4Itree.«term_⟶_» = Lean.ParserDescr.trailingNode `Lean4Itree.«term_⟶_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟶ ") (Lean.ParserDescr.cat `term 50))

inductive Lean4Itree.VoidE : Type u → Type v

The empty effect family, with no operations.

inductive Lean4Itree.SumE (ε1 ε2 : Type u → Type v) : Type u → Type v

The sum of two effect families: an effect is either from ε1 or from ε2.

• inl {ε1 ε2 : Type u → Type v} {α : Type u} (e1 : ε1 α) : SumE ε1 ε2 α
• inr {ε1 ε2 : Type u → Type v} {α : Type u} (e2 : ε2 α) : SumE ε1 ε2 α

@[implicit_reducible]

instance Lean4Itree.instAddEffect : Add (Type u → Type v)

Addition of effect families is their sum SumE.

Equations

• Lean4Itree.instAddEffect = { add := Lean4Itree.SumE }

@[implicit_reducible]

instance Lean4Itree.instCoeSumEInl {α : Type u} {ε1 ε2 : Type u → Type v} : Coe (ε1 α) (SumE ε1 ε2 α)

Coerce a left effect into the sum SumE ε1 ε2.

Equations

• Lean4Itree.instCoeSumEInl = { coe := fun (e : ε1 α) => Lean4Itree.SumE.inl e }

@[implicit_reducible]

instance Lean4Itree.instCoeSumEInr {α : Type u} {ε1 ε2 : Type u → Type v} : Coe (ε2 α) (SumE ε1 ε2 α)

Coerce a right effect into the sum SumE ε1 ε2.

Equations

• Lean4Itree.instCoeSumEInr = { coe := fun (e : ε2 α) => Lean4Itree.SumE.inr e }

@[implicit_reducible]

instance Lean4Itree.instCoeAddInl {α : Type u} {ε1 ε2 : Type u → Type v} : Coe (ε1 α) ((ε1 + ε2) α)

Coerce a left effect into the sum (ε1 + ε2).

Equations

• Lean4Itree.instCoeAddInl = { coe := fun (e : ε1 α) => Lean4Itree.SumE.inl e }

@[implicit_reducible]

instance Lean4Itree.instCoeAddInr {α : Type u} {ε1 ε2 : Type u → Type v} : Coe (ε2 α) ((ε1 + ε2) α)

Coerce a right effect into the sum (ε1 + ε2).

Equations

• Lean4Itree.instCoeAddInr = { coe := fun (e : ε2 α) => Lean4Itree.SumE.inr e }

inductive Lean4Itree.IterState (ι : Type u) (ρ : Type v) : Type (max u v)

The result of one iteration step: either done with a result or recur with the next accumulator.

• done {ι : Type u} {ρ : Type v} (r : ρ) : IterState ι ρ
• recur {ι : Type u} {ρ : Type v} (i : ι) : IterState ι ρ

class Lean4Itree.MonadIter (m : Type u → Type v) : Type (max (u + 1) v)

The class of monads supporting tail-recursive iteration via iter.

• iter {ρ ι : Type u} : (ι → m (IterState ι ρ)) → ι → m ρ

  Iterate a step function until it returns done.

@[implicit_reducible]

instance Lean4Itree.instMonadIterStateT {σ : Type u} {m : Type u → Type u} [Monad m] [MI : MonadIter m] : MonadIter (StateT σ m)

StateT lifts MonadIter by threading the state through each iteration step.

Equations

• One or more equations did not get rendered due to their size.

inductive Lean4Itree.ITree.IterMode {ε : Type u_1 → Type u_2} {ρ : Type u_3} {ι : Type u_4} : Type (max (max (max (u_1 + 1) u_2) u_3) u_4)

The traversal mode used by iter: either start a new iteration (iterS) or continue binding the tree produced by a step (bindS).

• iterS {ε : Type u_1 → Type u_2} {ρ : Type u_3} {ι : Type u_4} (i : ι) : IterMode
• bindS {ε : Type u_1 → Type u_2} {ρ : Type u_3} {ι : Type u_4} (t : ITree ε (IterState ι ρ)) : IterMode

def Lean4Itree.ITree.iter {ε : Type u_1 → Type u_2} {ρ : Type u_3} {ι : Type u_4} (step : ι → ITree ε (IterState ι ρ)) (i : ι) : ITree ε ρ

Iterate step from the seed i, producing the interaction tree that loops until a step returns done.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean4Itree.ITree.instMonadIterITree {ε : Type u → Type v} : MonadIter (ITree ε)

Interaction trees iterate via the ITree.iter combinator.

Equations

• Lean4Itree.ITree.instMonadIterITree = { iter := fun {ρ ι : Type ?u.1} => Lean4Itree.ITree.iter }

def Lean4Itree.ITree.interp {ε : Type → Type} {m : Type 1 → Type 1} {ρ : Type} [Monad m] [MI : MonadIter m] (handler : {α : Type} → ε α → m (ULift.{1, 0} α)) (t : ITree ε ρ) : m (ULift.{1, 0} ρ)

Interpret an interaction tree by handling each effect with handler and running the resulting computation in an iterable monad m.

Equations

• One or more equations did not get rendered due to their size.