Free Monad of a Polynomial Functor

We define the free monad on a polynomial functor (PFunctor), and prove some basic properties.

The free monad PFunctor.FreeM P extends the W-type construction with an extra pure constructor, yielding a monad that is free over the polynomial functor P.

Comparison with Cslib.FreeM

Cslib.FreeM F (in Cslib/Foundations/Control/Monad/Free.lean) builds a free monad over an arbitrary type constructor F : Type u → Type v, which need not be functorial. Its liftBind constructor abstracts over the intermediate type ι:

| liftBind {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : FreeM F α

PFunctor.FreeM P instead takes a polynomial functor P : PFunctor, where the shapes P.A and positions P.B a are given explicitly. Its liftBind constructor uses the shape and continuation directly:

| liftBind (a : P.A) (cont : P.B a → P.FreeM α) : P.FreeM α

When the effect signature is naturally polynomial (a fixed set of operations, each with a known return type), PFunctor.FreeM avoids the universe bump that the abstract ι in Cslib.FreeM introduces. Concretely, PFunctor.FreeM P is a genuine endofunctor on a single universe: for a ground P, P.FreeM α : Type whenever α : Type, whereas Cslib.FreeM F α : Type 1 for F : Type → Type, since liftBind stores the intermediate type ι : Type.

This matters when a program must itself be a first-class value of the same kind, i.e. for higher-order effects whose operations consume or return computations of the same monad (schedulers, exception handlers, staged interpreters, higher-order oracles). Such an effect's response type can be another P.FreeM computation, staying in one universe:

def coin : PFunctor.{0,0} := ⟨Bool, fun b => if b then Bool else Nat⟩
-- a `coin`-program is itself `Type 0`, so it can be another effect's response type:
def scheduler : PFunctor.{0,0} := ⟨Unit, fun _ => coin.FreeM Bool⟩  -- `Type 0`

With the abstract ι, the analogous program lives in Type 1, so an effect Type → Type cannot return it; bumping the effect to Type 1 → Type 1 pushes its programs to Type 2, and so on without bound.

This construction is ported from the VCV-io library.

Main Definitions

• PFunctor.FreeM: The free monad on a polynomial functor.
• PFunctor.FreeM.lift: Lift a shape of the base polynomial functor into the free monad.
• PFunctor.FreeM.liftObj: Lift an object of the base polynomial functor into the free monad.
• PFunctor.FreeM.liftM: Interpret FreeM P into any other monad.

inductive PFunctor.FreeM (P : PFunctor.{uA, uB}) : Type v → Type (max uA uB v)

The free monad on a polynomial functor. This extends WType with an extra pure constructor.

• pure {P : PFunctor.{uA, uB}} {α : Type v} (a : α) : P.FreeM α

  A leaf node wrapping a pure value.

• liftBind {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (cont : P.B a → P.FreeM α) : P.FreeM α

  Invoke the operation a : P.A with continuation cont : P.B a → P.FreeM α.

@[implicit_reducible]

instance PFunctor.instInhabitedFreeM {a✝ : PFunctor.{u_1, u_2}} {a✝¹ : Type u_3} [Inhabited a✝¹] : Inhabited (a✝.FreeM a✝¹)

Equations

• PFunctor.instInhabitedFreeM = { default := PFunctor.instInhabitedFreeM.default }

@[implicit_reducible]

instance PFunctor.FreeM.instPure {P : PFunctor.{uA, uB}} : Pure P.FreeM

Equations

• PFunctor.FreeM.instPure = { pure := fun {α : Type ?u.1} => PFunctor.FreeM.pure }

@[simp]

theorem PFunctor.FreeM.pure_eq_pure {P : PFunctor.{uA, uB}} {α : Type u_1} : FreeM.pure = pure

def PFunctor.FreeM.lift {P : PFunctor.{uA, uB}} (a : P.A) : P.FreeM (P.B a)

Lift a shape of the base polynomial functor into the free monad.

Equations

• PFunctor.FreeM.lift a = PFunctor.FreeM.liftBind a pure

@[simp]

theorem PFunctor.FreeM.lift_ne_pure {P : PFunctor.{uA, uB}} (a : P.A) (y : P.B a) : lift a ≠ pure y

@[simp]

theorem PFunctor.FreeM.pure_ne_lift {P : PFunctor.{uA, uB}} (a : P.A) (y : P.B a) : pure y ≠ lift a

def PFunctor.FreeM.bind {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} : P.FreeM α → (α → P.FreeM β) → P.FreeM β

Bind operation for the FreeM monad.

The builtin >>= notation should be preferred when α and β are in the same universe.

Equations

• (PFunctor.FreeM.pure a).bind x✝ = x✝ a
• (PFunctor.FreeM.liftBind a cont).bind x✝ = PFunctor.FreeM.liftBind a fun (u : P.B a) => (cont u).bind x✝

@[implicit_reducible]

instance PFunctor.FreeM.instBind {P : PFunctor.{uA, uB}} : Bind P.FreeM

Equations

• PFunctor.FreeM.instBind = { bind := fun {α β : Type ?u.1} => PFunctor.FreeM.bind }

@[simp]

theorem PFunctor.FreeM.bind_eq_bind {P : PFunctor.{uA, uB}} {α β : Type v} : FreeM.bind = bind

Note that this lemma does not always apply, as it is universe-constrained by Bind.bind.

def PFunctor.FreeM.map {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} (f : α → β) : P.FreeM α → P.FreeM β

Map a function over a FreeM computation.

The builtin <$> notation should be preferred when α and β are in the same universe.

Equations

• PFunctor.FreeM.map f (PFunctor.FreeM.pure a) = PFunctor.FreeM.pure (f a)
• PFunctor.FreeM.map f (PFunctor.FreeM.liftBind a cont) = PFunctor.FreeM.liftBind a fun (u : P.B a) => PFunctor.FreeM.map f (cont u)

@[implicit_reducible]

instance PFunctor.FreeM.instFunctor {P : PFunctor.{uA, uB}} : Functor P.FreeM

Equations

• PFunctor.FreeM.instFunctor = { map := fun {α β : Type ?u.1} => PFunctor.FreeM.map }

@[simp]

theorem PFunctor.FreeM.map_eq_map {P : PFunctor.{uA, uB}} {α β : Type v} : map = Functor.map

Note that this lemma does not always apply, as it is universe-constrained by Functor.map.

@[simp]

theorem PFunctor.FreeM.liftBind_eq {P : PFunctor.{uA, uB}} {α : Type u_1} (a : P.A) (cont : P.B a → P.FreeM α) : liftBind a cont = (lift a).bind cont

@[reducible, inline]

abbrev PFunctor.FreeM.liftObj {P : PFunctor.{uA, uB}} {α : Type u_1} (x : ↑P α) : P.FreeM α

Lift an object of the base polynomial functor into the free monad.

This lifts the shape x.1 with lift and relabels the responses with x.2. We use the universe-polymorphic FreeM.map rather than <$>, since the response type P.B x.1 and the target α need not lie in the same universe.

Equations

• PFunctor.FreeM.liftObj x = PFunctor.FreeM.map x.snd (PFunctor.FreeM.lift x.fst)

@[implicit_reducible]

instance PFunctor.FreeM.instMonadLiftObj {P : PFunctor.{uA, uB}} : MonadLift (↑P) P.FreeM

Equations

• PFunctor.FreeM.instMonadLiftObj = { monadLift := fun {α : Type ?u.1} (x : ↑P α) => PFunctor.FreeM.liftObj x }

@[simp]

theorem PFunctor.FreeM.liftObj_ne_pure {P : PFunctor.{uA, uB}} {α : Type u_1} (x : ↑P α) (y : α) : liftObj x ≠ pure y

@[simp]

theorem PFunctor.FreeM.pure_ne_liftObj {P : PFunctor.{uA, uB}} {α : Type u_1} (x : ↑P α) (y : α) : pure y ≠ liftObj x

theorem PFunctor.FreeM.monadLift_eq_liftObj {P : PFunctor.{uA, uB}} {α : Type u_1} (x : ↑P α) : liftM x = liftObj x

theorem PFunctor.FreeM.induction {P : PFunctor.{uA, uB}} {α : Type u_1} {motive : P.FreeM α → Prop} (pure : ∀ (a : α), motive (pure a)) (lift_bind : ∀ (a : P.A) (cont : P.B a → P.FreeM α), (∀ (i : P.B a), motive (cont i)) → motive ((lift a).bind cont)) (x : P.FreeM α) : motive x

An override for the default induction principle that is in simp-normal form.

Note that when α and P.B a are in the same universe, this simplifies slightly further.

theorem PFunctor.FreeM.bind_assoc {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : P.FreeM α) (f : α → P.FreeM β) (g : β → P.FreeM γ) : (x.bind f).bind g = x.bind fun (a : α) => (f a).bind g

@[simp]

theorem PFunctor.FreeM.pure_bind {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} (a : α) (f : α → P.FreeM β) : (pure a).bind f = f a

.pure a followed by bind collapses immediately.

@[simp]

theorem PFunctor.FreeM.bind_pure {P : PFunctor.{uA, uB}} {α : Type u_1} (x : P.FreeM α) : x.bind pure = x

@[simp]

theorem PFunctor.FreeM.bind_pure_comp {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} (f : α → β) (x : P.FreeM α) : x.bind (pure ∘ f) = map f x

@[simp]

theorem PFunctor.FreeM.liftBind_bind {P : PFunctor.{uA, uB}} {β : Type u_2} {γ : Type u_3} (a : P.A) (cont : P.B a → P.FreeM β) (f : β → P.FreeM γ) : ((lift a).bind cont).bind f = (lift a).bind fun (u : P.B a) => (cont u).bind f

@[simp]

theorem PFunctor.FreeM.liftObj_bind {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} (x : ↑P α) (f : α → P.FreeM β) : (liftObj x).bind f = liftBind x.fst fun (a : P.B x.fst) => f (x.snd a)

@[simp]

theorem PFunctor.FreeM.bind_eq_pure_iff {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} (x : P.FreeM α) (f : α → P.FreeM β) (b : β) : x.bind f = pure b ↔ ∃ (a : α), x = pure a ∧ f a = pure b

@[simp]

theorem PFunctor.FreeM.pure_eq_bind_iff {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} (x : P.FreeM α) (f : α → P.FreeM β) (b : β) : pure b = x.bind f ↔ ∃ (a : α), x = pure a ∧ pure b = f a

@[implicit_reducible]

instance PFunctor.FreeM.instMonad {P : PFunctor.{uA, uB}} : Monad P.FreeM

Equations

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

@[simp]

theorem PFunctor.FreeM.id_map {P : PFunctor.{uA, uB}} {α : Type u_1} (x : P.FreeM α) : map id x = x

theorem PFunctor.FreeM.comp_map {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (x : P.FreeM α) : map (h ∘ g) x = map h (map g x)

instance PFunctor.FreeM.instLawfulMonad {P : PFunctor.{uA, uB}} : LawfulMonad P.FreeM

@[simp]

theorem PFunctor.FreeM.pure_inj {P : PFunctor.{uA, uB}} {α : Type u_1} (a b : α) : pure a = pure b ↔ a = b

theorem PFunctor.FreeM.liftBind_inj {P : PFunctor.{uA, uB}} {α : Type u_1} (a a' : P.A) (cont : P.B a → P.FreeM α) (cont' : P.B a' → P.FreeM α) : liftBind a cont = liftBind a' cont' ↔ ∃ (h : a = a'), Eq.rec (motive := fun (x : P.A) (h : a = x) => P.B x → P.FreeM α) cont h = cont'

def PFunctor.FreeM.liftM {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : P.FreeM α → m α

Interpret a FreeM P computation into any monad m by providing an interpretation interp : (a : P.A) → m (P.B a) for each operation.

Equations

• PFunctor.FreeM.liftM interp (PFunctor.FreeM.pure a) = pure a
• PFunctor.FreeM.liftM interp (PFunctor.FreeM.liftBind a cont) = do let u ← interp a PFunctor.FreeM.liftM interp (cont u)

@[simp]

theorem PFunctor.FreeM.liftM_pure {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (interp : (a : P.A) → m (P.B a)) (a : α) : FreeM.liftM interp (pure a) = pure a

@[simp]

theorem PFunctor.FreeM.liftM_lift_bind {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (interp : (a : P.A) → m (P.B a)) (a : P.A) (cont : P.B a → P.FreeM α) : FreeM.liftM interp (lift a >>= cont) = do let u ← interp a FreeM.liftM interp (cont u)

structure PFunctor.FreeM.Interprets {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (handler : (a : P.A) → m (P.B a)) (eval : P.FreeM α → m α) : Prop

A predicate stating that eval : P.FreeM α → m α is an interpreter for the polynomial effect handler handler : (a : P.A) → m (P.B a).

This means that eval is a monad morphism from the free monad P.FreeM to the monad m, and that it extends the interpretation of individual operations given by handler.

• apply_pure (a : α) : eval (FreeM.pure a) = pure a
• apply_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) : eval ((lift a).bind cont) = do let x ← handler a eval (cont x)

theorem PFunctor.FreeM.Interprets.eq {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] {handler : (a : P.A) → m (P.B a)} {eval : P.FreeM α → m α} (h : Interprets handler eval) : eval = fun (x : P.FreeM α) => FreeM.liftM handler x

theorem PFunctor.FreeM.Interprets.liftM {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (handler : (a : P.A) → m (P.B a)) : Interprets handler fun (x : P.FreeM α) => FreeM.liftM handler x

theorem PFunctor.FreeM.Interprets.iff {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (handler : (a : P.A) → m (P.B a)) (eval : P.FreeM α → m α) : Interprets handler eval ↔ eval = fun (x : P.FreeM α) => FreeM.liftM handler x

The universal property of the free monad P.FreeM.

That is, liftM handler is the unique interpreter that extends the effect handler handler to interpret P.FreeM computations in a monad m.

@[simp]

theorem PFunctor.FreeM.liftM_bind {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] (interp : (a : P.A) → m (P.B a)) [LawfulMonad m] {α β : Type uB} (x : P.FreeM α) (f : α → P.FreeM β) : FreeM.liftM interp (x >>= f) = do let u ← FreeM.liftM interp x FreeM.liftM interp (f u)

@[simp]

theorem PFunctor.FreeM.liftM_map {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] (interp : (a : P.A) → m (P.B a)) [LawfulMonad m] {α β : Type uB} (f : α → β) (x : P.FreeM α) : FreeM.liftM interp (f <$> x) = f <$> FreeM.liftM interp x

@[simp]

theorem PFunctor.FreeM.liftM_seq {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] {α β : Type uB} (interp : (a : P.A) → m (P.B a)) (x : P.FreeM (α → β)) (y : P.FreeM α) : FreeM.liftM interp (x <*> y) = FreeM.liftM interp x <*> FreeM.liftM interp y

@[simp]

theorem PFunctor.FreeM.liftM_seqLeft {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] {α β : Type uB} (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) (y : P.FreeM β) : FreeM.liftM interp (x <* y) = FreeM.liftM interp x <* FreeM.liftM interp y

@[simp]

theorem PFunctor.FreeM.liftM_seqRight {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] {α β : Type uB} (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) (y : P.FreeM β) : FreeM.liftM interp (x *> y) = FreeM.liftM interp x *> FreeM.liftM interp y

@[simp]

theorem PFunctor.FreeM.liftM_lift {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (interp : (a : P.A) → m (P.B a)) (a : P.A) : FreeM.liftM interp (lift a) = interp a

@[simp]

theorem PFunctor.FreeM.liftM_liftObj {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] [LawfulMonad m] (interp : (a : P.A) → m (P.B a)) (x : ↑P α) : FreeM.liftM interp (liftObj x) = x.snd <$> interp x.fst