Free Monads

This file defines the free monad on an arbitrary mapping f : Type u → Type v. This has the undesirable property of raising the universe level by 1, which means we can't pass a FreeMonad f object as a continuation into an interactive protocol.

See PFunctor.FreeM for the free monad of a polynomial functor, which does not raise the universe level.

inductive FreeMonad (f : Type u → Type v) (α : Type w) : Type (max (u + 1) v w)

The free monad on a functor f is the type freely generated by values of type f α and the operations pure and bind. Implemented directly rather than as a quotient. Slightly different than constructions of free monads in Haskell because of universe issues.

• pure {f : Type u → Type v} {α : Type w} (x : α) : FreeMonad f α
• roll {f : Type u → Type v} {α : Type w} {β : Type u} (x : f β) (r : β → FreeMonad f α) : FreeMonad f α

@[inline]

def FreeMonad.lift {f : Type u → Type v} {α : Type u} (x : f α) : FreeMonad f α

Lift an element of the base functor to the free monad by directly returning the result.

@[implicit_reducible]

instance FreeMonad.instMonadLift {f : Type u → Type v} : MonadLift f (FreeMonad f)

@[simp]

theorem FreeMonad.monadLift_eq_lift {f : Type u → Type v} {α : Type u} (x : f α) : liftM x = lift x

@[implicit_reducible]

instance FreeMonad.instInhabited {f : Type u → Type v} {α : Type u} [Inhabited (f α)] : Inhabited (FreeMonad f α)

@[inline]

def FreeMonad.bind {f : Type u → Type v} {α β : Type u} : FreeMonad f α → (α → FreeMonad f β) → FreeMonad f β

Bind operator on OracleComp spec operation used in the monad definition.

@[simp]

theorem FreeMonad.bind_pure {f : Type u → Type v} {α β : Type u} (x : α) (r : α → FreeMonad f β) : (FreeMonad.pure x).bind r = r x

@[simp]

theorem FreeMonad.bind_roll {f : Type u → Type v} {α β γ : Type u} (x : f α) (r : α → FreeMonad f β) (g : β → FreeMonad f γ) : (roll x r).bind g = roll x fun (u : α) => (r u).bind g

@[simp]

theorem FreeMonad.bind_lift {f : Type u → Type v} {α β : Type u} (x : f α) (r : α → FreeMonad f β) : (lift x).bind r = roll x r

@[implicit_reducible]

instance FreeMonad.instMonad {f : Type u → Type v} : Monad (FreeMonad f)

@[simp]

theorem FreeMonad.monad_pure_def {f : Type u → Type v} {α : Type u} (x : α) : pure x = FreeMonad.pure x

@[simp]

theorem FreeMonad.monad_bind_def {f : Type u → Type v} {α β : Type u} (x : FreeMonad f α) (g : α → FreeMonad f β) : x >>= g = x.bind g

instance FreeMonad.instLawfulMonad {f : Type u → Type v} : LawfulMonad (FreeMonad f)

@[implicit_reducible]

instance FreeMonad.instMonadFunctor {f : Type u → Type v} : MonadFunctor f (FreeMonad f)

def FreeMonad.inductionOn {f : Type u → Type v} {α : Type u} {C : FreeMonad f α → Prop} (pure : ∀ (x : α), C (pure x)) (roll : ∀ {β : Type u} (x : f β) (r : β → FreeMonad f α), (∀ (y : β), C (r y)) → C (liftM x >>= r)) (oa : FreeMonad f α) : C oa

Proving something about FreeMonad f α only requires two cases:

• pure x for some x : α Note that we can't use Sort v instead of Prop due to universe levels.

def FreeMonad.construct {f : Type u → Type v} {α : Type u} {C : FreeMonad f α → Type u_1} (pure : (x : α) → C (pure x)) (roll : {β : Type u} → (x : f β) → (r : β → FreeMonad f α) → ((y : β) → C (r y)) → C (liftM x >>= r)) (oa : FreeMonad f α) : C oa

Shoulde be possible to unify with the above.

@[simp]

theorem FreeMonad.construct_pure {f : Type u → Type v} {α : Type u} {C : FreeMonad f α → Type u_1} (h_pure : (x : α) → C (pure x)) (h_roll : {β : Type u} → (x : f β) → (r : β → FreeMonad f α) → ((y : β) → C (r y)) → C (liftM x >>= r)) (y : α) : FreeMonad.construct h_pure (fun {β : Type u} => h_roll) (pure y) = h_pure y

@[simp]

theorem FreeMonad.construct_roll {f : Type u → Type v} {α β : Type u} {C : FreeMonad f α → Type u_1} (h_pure : (x : α) → C (pure x)) (h_roll : {β : Type u} → (x : f β) → (r : β → FreeMonad f α) → ((y : β) → C (r y)) → C (liftM x >>= r)) (x : f β) (r : β → FreeMonad f α) : FreeMonad.construct h_pure (fun {β : Type u} => h_roll) (roll x r) = h_roll x r fun (u : β) => FreeMonad.construct h_pure (fun {β : Type u} => h_roll) (r u)

def FreeMonad.mapM_aux {f : Type u → Type v} {α : Type u} {m : Type u → Type w} [Pure m] [Bind m] (s : {α : Type u} → f α → m α) (oa : FreeMonad f α) : m α

def FreeMonad.mapM' {f : Type u → Type v} (m : Type u → Type w) [Monad m] [LawfulMonad m] (s : {α : Type u} → f α → m α) : FreeMonad f →ᵐ m

@[simp]

theorem FreeMonad.mapM'_lift {f : Type u → Type v} {α : Type u} {m : Type u → Type w} [Monad m] [LawfulMonad m] (s : {α : Type u} → f α → m α) (x : f α) : (fun {α : Type u} (x : FreeMonad (fun {α : Type u} => f α) α) => (FreeMonad.mapM' m fun {α : Type u} => s).toFun α x) (lift x) = s x

def FreeMonad.mapM {f : Type u → Type v} {α : Type u} {m : Type u → Type w} [Pure m] [Bind m] (oa : FreeMonad f α) (s : {α : Type u} → f α → m α) : m α

Canonical mapping of a free monad into any other monad, given a map on the base functor.

@[simp]

theorem FreeMonad.mapM_pure {f : Type u → Type v} {α : Type u} {m : Type u → Type w} (s : {α : Type u} → f α → m α) [Monad m] (x : α) : ((FreeMonad.pure x).mapM fun {α : Type u} => s) = pure x

@[simp]

theorem FreeMonad.mapM_roll {f : Type u → Type v} {α β : Type u} {m : Type u → Type w} (s : {α : Type u} → f α → m α) [Monad m] (x : f α) (r : α → FreeMonad f β) : ((roll x r).mapM fun {α : Type u} => s) = do let u ← s x (r u).mapM fun {α : Type u} => s

noncomputable def FreeMonad.depth {f : Type u → Type v} {α : Type u} : FreeMonad f α → ℕ∞

The depth of a free monad as a potentially infinite natural number, defined recursively as the maximum depth of its children.

@[simp]

theorem FreeMonad.depth_pure {f : Type u → Type v} {α : Type u} {x : α} : (pure x).depth = 0

@[simp]

theorem FreeMonad.depth_pure' {f : Type u → Type v} {α : Type u} {x : α} : (FreeMonad.pure x).depth = 0

@[simp]

theorem FreeMonad.depth_roll {f : Type u → Type v} {α β : Type u} {x : f α} {r : α → FreeMonad f β} : (roll x r).depth = 1 + ⨆ (u : α), (r u).depth

noncomputable def FreeMonad.depthBindAux {f : Type u → Type v} {α β : Type u} : FreeMonad f α → (α → FreeMonad f β) → ℕ∞

theorem FreeMonad.depth_bind_eq {f : Type u → Type v} {α β : Type u} {x : FreeMonad f α} {g : α → FreeMonad f β} : (x >>= g).depth = x.depthBindAux g

The depth of a bind computation can be defined exactly using the definition of bind (but might not be very revealing)

theorem FreeMonad.depth_bind_le {f : Type u → Type v} {α β : Type u} {x : FreeMonad f α} {g : α → FreeMonad f β} : (x >>= g).depth ≤ x.depth + ⨆ (u : α), (g u).depth

theorem FreeMonad.depth_eq_zero_iff {f : Type u → Type v} {α : Type u} {x : FreeMonad f α} : x.depth = 0 ↔ ∃ (y : α), x = pure y

theorem FreeMonad.depth_eq_one_iff {f : Type u → Type v} {α : Type u} {x : FreeMonad f α} : x.depth = 1 ↔ ∃ (β : Type u) (y : f β) (r : β → FreeMonad f α), x = roll y r ∧ ∀ (u : β), (r u).depth = 0