Free Monad of a Polynomial Functor

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

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

The free monad on a polynomial functor. This extends the W-type construction with an extra pure constructor.

• pure {P : PFunctor.{uA, uB}} {α : Type v} (x : α) : P.FreeM α
• roll {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (r : P.B a → P.FreeM α) : P.FreeM α

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

def PFunctor.instInhabitedFreeM.default {a✝ : PFunctor.{u_1, u_2}} {a✝¹ : Type u_3} [Inhabited a✝¹] : a✝.FreeM a✝¹

@[reducible, inline]

def PFunctor.FreeM.lift {P : PFunctor.{uA, uB}} {α : Type v} (x : ↑P α) : P.FreeM α

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

@[reducible, inline]

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

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

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

@[simp]

theorem PFunctor.FreeM.lift_ne_pure {P : PFunctor.{uA, uB}} {α : Type v} (x : ↑P α) (y : α) : lift x ≠ pure y

@[simp]

theorem PFunctor.FreeM.pure_ne_lift {P : PFunctor.{uA, uB}} {α : Type v} (x : ↑P α) (y : α) : pure y ≠ lift x

theorem PFunctor.FreeM.monadLift_eq_lift {P : PFunctor.{uA, uB}} {α : Type v} (x : ↑P α) : liftM x = lift x

@[inline]

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

Bind operator on FreeM P operation used in the monad definition.

@[simp]

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

@[simp]

theorem PFunctor.FreeM.bind_roll {P : PFunctor.{uA, uB}} {β γ : Type v} (a : P.A) (r : P.B a → P.FreeM β) (g : β → P.FreeM γ) : (roll a r).bind g = roll a fun (u : P.B a) => (r u).bind g

@[simp]

theorem PFunctor.FreeM.bind_lift {P : PFunctor.{uA, uB}} {α β : Type v} (x : ↑P α) (r : α → P.FreeM β) : (lift x).bind r = roll x.fst fun (a : P.B x.fst) => r (x.snd a)

@[simp]

theorem PFunctor.FreeM.bind_eq_pure_iff {P : PFunctor.{uA, uB}} {α β : Type v} (x : P.FreeM α) (y : α → P.FreeM β) (y' : β) : x.bind y = pure y' ↔ ∃ (x' : α), x = pure x' ∧ y x' = pure y'

@[simp]

theorem PFunctor.FreeM.pure_eq_bind_iff {P : PFunctor.{uA, uB}} {α β : Type v} (x : P.FreeM α) (y : α → P.FreeM β) (y' : β) : pure y' = x.bind y ↔ ∃ (x' : α), x = pure x' ∧ pure y' = y x'

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

theorem PFunctor.FreeM.monad_pure_def {P : PFunctor.{uA, uB}} {α : Type v} (x : α) : pure x = pure x

theorem PFunctor.FreeM.monad_bind_def {P : PFunctor.{uA, uB}} {α β : Type v} (x : P.FreeM α) (g : α → P.FreeM β) : x >>= g = x.bind g

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

theorem PFunctor.FreeM.pure_inj {P : PFunctor.{uA, uB}} {α : Type v} (x y : α) : pure x = pure y ↔ x = y

@[simp]

theorem PFunctor.FreeM.roll_inj {P : PFunctor.{uA, uB}} {α : Type v} (x x' : P.A) (y : P.B x → P.FreeM α) (y' : P.B x' → P.FreeM α) : roll x y = roll x' y' ↔ ∃ (h : x = x'), Eq.rec (motive := fun (x_1 : P.A) (h : x = x_1) => P.B x_1 → P.FreeM α) y h = y'

def PFunctor.FreeM.inductionOn {P : PFunctor.{uA, uB}} {α : Type v} {C : P.FreeM α → Prop} (pure : ∀ (x : α), C (pure x)) (roll : ∀ (x : P.A) (r : P.B x → P.FreeM α), (∀ (y : P.B x), C (r y)) → C (roll x r)) (oa : P.FreeM α) : C oa

Proving a predicate C of FreeM P α requires two cases:

• pure x for some x : α
• roll x r h for some x : P.A, r : P.B x → FreeM P α, and h : ∀ y, C (r y) Note that we can't use Sort v instead of Prop due to universe levels.

def PFunctor.FreeM.construct {P : PFunctor.{uA, uB}} {α : Type v} {C : P.FreeM α → Type u_1} (pure : (x : α) → C (pure x)) (roll : (x : P.A) → (r : P.B x → P.FreeM α) → ((y : P.B x) → C (r y)) → C (roll x r)) (oa : P.FreeM α) : C oa

Shoulde be possible to unify with the above

@[simp]

theorem PFunctor.FreeM.construct_pure {P : PFunctor.{uA, uB}} {α : Type v} {C : P.FreeM α → Type u_1} (h_pure : (x : α) → C (pure x)) (h_roll : (x : P.A) → (r : P.B x → P.FreeM α) → ((y : P.B x) → C (r y)) → C (roll x r)) (y : α) : FreeM.construct h_pure h_roll (pure y) = h_pure y

@[simp]

theorem PFunctor.FreeM.construct_roll {P : PFunctor.{uA, uB}} {α : Type v} {C : P.FreeM α → Type u_1} (h_pure : (x : α) → C (pure x)) (h_roll : (x : P.A) → (r : P.B x → P.FreeM α) → ((y : P.B x) → C (r y)) → C (roll x r)) (x : P.A) (r : P.B x → P.FreeM α) : FreeM.construct h_pure h_roll (roll x r) = h_roll x r fun (u : P.B x) => FreeM.construct h_pure h_roll (r u)

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

Canonical mapping of FreeM P into any other monad, given a map s : (a : P.A) → m (P.B a).

@[simp]

theorem PFunctor.FreeM.mapM_pure' {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (s : (a : P.A) → m (P.B a)) (x : α) : FreeM.mapM s (pure x) = Pure.pure x

@[simp]

theorem PFunctor.FreeM.mapM_roll {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (s : (a : P.A) → m (P.B a)) (x : P.A) (r : P.B x → P.FreeM α) : FreeM.mapM s (roll x r) = do let u ← s x FreeM.mapM s (r u)

@[simp]

theorem PFunctor.FreeM.mapM_pure {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (s : (a : P.A) → m (P.B a)) (x : α) : FreeM.mapM s (Pure.pure x) = Pure.pure x

@[simp]

theorem PFunctor.FreeM.mapM_bind {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] (s : (a : P.A) → m (P.B a)) [LawfulMonad m] {α β : Type uB} (x : P.FreeM α) (y : α → P.FreeM β) : FreeM.mapM s (x.bind y) = do let u ← FreeM.mapM s x FreeM.mapM s (y u)

@[simp]

theorem PFunctor.FreeM.mapM_bind' {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] (s : (a : P.A) → m (P.B a)) [LawfulMonad m] {α β : Type uB} (x : P.FreeM α) (y : α → P.FreeM β) : FreeM.mapM s (x >>= y) = do let u ← FreeM.mapM s x FreeM.mapM s (y u)

@[simp]

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

@[simp]

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

@[simp]

theorem PFunctor.FreeM.mapM_lift {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) (x : ↑P α) : FreeM.mapM s (lift x) = do let u ← s x.fst FreeM.mapM s (pure (x.snd u))

@[simp]

theorem PFunctor.FreeM.mapM_liftA {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) (x : P.A) : FreeM.mapM s (liftA x) = s x

def PFunctor.FreeM.mapMHom {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) : P.FreeM →ᵐ m

FreeM.mapM as a monad homomorphism.

@[simp]

theorem PFunctor.FreeM.mapMHom_toFun_eq {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) : (FreeM.mapMHom s).toFun α = FreeM.mapM s

def PFunctor.FreeM.mapMHom' {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (s : NatHom (↑P) m) : P.FreeM →ᵐ m

@[simp]

theorem PFunctor.FreeM.mapMHom'_toFun_eq {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] [LawfulMonad m] (s : NatHom (↑P) m) : (FreeM.mapMHom' s).toFun α = FreeM.mapM fun (t : P.A) => (fun {α : Type uB} (x : ↑P α) => s.toFun α x) ⟨t, id⟩