Continuation Monad

Monad encapsulating continuation passing programming style, similar to Haskell's Cont, ContT and MonadCont: http://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Cont.html

structure MonadCont.Label (α : Type w) (m : Type u → Type v) (β : Type u) : Type (max v w)

• apply : α → m β

def MonadCont.goto {α : Type u_1} {β : Type u} {m : Type u → Type v} (f : ContT.Label α m β) (x : α) : m β

Equations

• ContT.goto f x = MonadCont.Label.apply f x

class MonadCont (m : Type u → Type v) : Type (max (u + 1) v)

• callCC : {α β : Type u} → (ContT.Label α m β → m α) → m α

class LawfulMonadCont (m : Type u → Type v) [Monad m] [MonadCont m] extends LawfulMonad : Prop

• map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
• id_map : ∀ {α : Type u} (x : m α), id <$> x = x
• comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α), (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
• seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
• pure_seq : ∀ {α β : Type u} (g : α → β) (x : m α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
• map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
• seq_pure : ∀ {α β : Type u} (g : m (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
• seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun x => g) fun x_1 => x
• bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α), (do let a ← x pure (f a)) = f <$> x
• bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α), (do let x_1 ← f x_1 <$> x) = Seq.seq f fun x_1 => x
• pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
• bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
• callCC_bind_right : ∀ {α ω γ : Type u} (cmd : m α) (next : ContT.Label ω m γ → α → m ω), (MonadCont.callCC fun f => cmd >>= next f) = do let x ← cmd MonadCont.callCC fun f => next f x
• callCC_bind_left : ∀ {α : Type u} (β : Type u) (x : α) (dead : ContT.Label α m β → β → m α), (MonadCont.callCC fun f => ContT.goto f x >>= dead f) = pure x
• callCC_dummy : ∀ {α β : Type u} (dummy : m α), (MonadCont.callCC fun x => dummy) = dummy

def ContT (r : Type u) (m : Type u → Type v) (α : Type w) : Type (max v w)

Equations

• ContT r m α = ((α → m r) → m r)

@[reducible]

def Cont (r : Type u) (α : Type w) : Type (max u w)

Equations

• Cont r α = ContT r id α

def ContT.run {r : Type u} {m : Type u → Type v} {α : Type w} : ContT r m α → (α → m r) → m r

Equations

• ContT.run = id

def ContT.map {r : Type u} {m : Type u → Type v} {α : Type w} (f : m r → m r) (x : ContT r m α) : ContT r m α

Equations

• ContT.map f x = f ∘ x

theorem ContT.run_contT_map_contT {r : Type u} {m : Type u → Type v} {α : Type w} (f : m r → m r) (x : ContT r m α) : ContT.run (ContT.map f x) = f ∘ ContT.run x

def ContT.withContT {r : Type u} {m : Type u → Type v} {α : Type w} {β : Type w} (f : (β → m r) → α → m r) (x : ContT r m α) : ContT r m β

Equations

• ContT.withContT f x g = x (f g)

theorem ContT.run_withContT {r : Type u} {m : Type u → Type v} {α : Type w} {β : Type w} (f : (β → m r) → α → m r) (x : ContT r m α) : ContT.run (ContT.withContT f x) = ContT.run x ∘ f

theorem ContT.ext {r : Type u} {m : Type u → Type v} {α : Type w} {x : ContT r m α} {y : ContT r m α} (h : ∀ (f : α → m r), ContT.run x f = ContT.run y f) : x = y

instance ContT.instMonadContT {r : Type u} {m : Type u → Type v} : Monad (ContT r m)

Equations

• ContT.instMonadContT = Monad.mk

instance ContT.instLawfulMonadContTInstMonadContT {r : Type u} {m : Type u → Type v} : LawfulMonad (ContT r m)

Equations

• @ContT.instLawfulMonadContTInstMonadContT = @ContT.instLawfulMonadContTInstMonadContT.proof_1

def ContT.monadLift {r : Type u} {m : Type u → Type v} [Monad m] {α : Type u} : m α → ContT r m α

Equations

• ContT.monadLift x f = x >>= f

instance ContT.instMonadLiftContT {r : Type u} {m : Type u → Type v} [Monad m] : MonadLift m (ContT r m)

Equations

• ContT.instMonadLiftContT = { monadLift := fun {α} => ContT.monadLift }

theorem ContT.monadLift_bind {r : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u} {β : Type u} (x : m α) (f : α → m β) : ContT.monadLift (x >>= f) = ContT.monadLift x >>= ContT.monadLift ∘ f

instance ContT.instMonadContContT {r : Type u} {m : Type u → Type v} : MonadCont (ContT r m)

Equations

• ContT.instMonadContContT = { callCC := fun {α β} f g => f { apply := fun x x_1 => g x } g }

instance ContT.instLawfulMonadContContTInstMonadContTInstMonadContContT {r : Type u} {m : Type u → Type v} : LawfulMonadCont (ContT r m)

Equations

• @ContT.instLawfulMonadContContTInstMonadContTInstMonadContContT = @ContT.instLawfulMonadContContTInstMonadContTInstMonadContContT.proof_1

instance ContT.instMonadExceptContT {r : Type u} {m : Type u → Type v} (ε : Type u_1) [MonadExcept ε m] : MonadExcept ε (ContT r m)

Equations

• ContT.instMonadExceptContT ε = { throw := fun {α} e x => throw e, tryCatch := fun {α} act h f => tryCatch (act f) fun e => h e f }

def ExceptT.mkLabel {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} {ε : Type u} : ContT.Label (Except ε α) m β → ContT.Label α (ExceptT ε m) β

Equations

• ExceptT.mkLabel x = match x with | { apply := f } => { apply := fun a => monadLift (f (Except.ok a)) }

theorem ExceptT.goto_mkLabel {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} {ε : Type u} (x : ContT.Label (Except ε α) m β) (i : α) : ContT.goto (ExceptT.mkLabel x) i = ExceptT.mk (Except.ok <$> ContT.goto x (Except.ok i))

def ExceptT.callCC {m : Type u → Type v} [Monad m] {ε : Type u} [MonadCont m] {α : Type u} {β : Type u} (f : ContT.Label α (ExceptT ε m) β → ExceptT ε m α) : ExceptT ε m α

Equations

• ExceptT.callCC f = ExceptT.mk (MonadCont.callCC fun x => ExceptT.run (f (ExceptT.mkLabel x)))

instance instMonadContExceptT {m : Type u → Type v} [Monad m] {ε : Type u} [MonadCont m] : MonadCont (ExceptT ε m)

Equations

• instMonadContExceptT = { callCC := fun {α β} => ExceptT.callCC }

instance instLawfulMonadContExceptTInstMonadExceptTInstMonadContExceptT {m : Type u → Type v} [Monad m] {ε : Type u} [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (ExceptT ε m)

Equations

• @instLawfulMonadContExceptTInstMonadExceptTInstMonadContExceptT = @instLawfulMonadContExceptTInstMonadExceptTInstMonadContExceptT.proof_1

def OptionT.mkLabel {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} : ContT.Label (Option α) m β → ContT.Label α (OptionT m) β

Equations

• OptionT.mkLabel x = match x with | { apply := f } => { apply := fun a => monadLift (f (some a)) }

theorem OptionT.goto_mkLabel {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (x : ContT.Label (Option α) m β) (i : α) : ContT.goto (OptionT.mkLabel x) i = OptionT.mk do let a ← ContT.goto x (some i) pure (some a)

def OptionT.callCC {m : Type u → Type v} [Monad m] [MonadCont m] {α : Type u} {β : Type u} (f : ContT.Label α (OptionT m) β → OptionT m α) : OptionT m α

Equations

• OptionT.callCC f = OptionT.mk (MonadCont.callCC fun x => OptionT.run (f (OptionT.mkLabel x)))

instance instMonadContOptionT {m : Type u → Type v} [Monad m] [MonadCont m] : MonadCont (OptionT m)

Equations

• instMonadContOptionT = { callCC := fun {α β} => OptionT.callCC }

instance instLawfulMonadContOptionTInstMonadOptionTInstMonadContOptionT {m : Type u → Type v} [Monad m] [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (OptionT m)

Equations

• @instLawfulMonadContOptionTInstMonadOptionTInstMonadContOptionT = @instLawfulMonadContOptionTInstMonadOptionTInstMonadContOptionT.proof_1

def WriterT.mkLabel {m : Type u → Type v} [Monad m] {α : Type u_1} {β : Type u} {ω : Type u} [EmptyCollection ω] : ContT.Label (α × ω) m β → ContT.Label α (WriterT ω m) β

Equations

• WriterT.mkLabel x = match x with | { apply := f } => { apply := fun a => monadLift (f (a, ∅)) }

def WriterT.mkLabel' {m : Type u → Type v} [Monad m] {α : Type u_1} {β : Type u} {ω : Type u} [Monoid ω] : ContT.Label (α × ω) m β → ContT.Label α (WriterT ω m) β

Equations

• WriterT.mkLabel' x = match x with | { apply := f } => { apply := fun a => monadLift (f (a, 1)) }

theorem WriterT.goto_mkLabel {m : Type u → Type v} [Monad m] {α : Type u_1} {β : Type u} {ω : Type u} [EmptyCollection ω] (x : ContT.Label (α × ω) m β) (i : α) : ContT.goto (WriterT.mkLabel x) i = monadLift (ContT.goto x (i, ∅))

theorem WriterT.goto_mkLabel' {m : Type u → Type v} [Monad m] {α : Type u_1} {β : Type u} {ω : Type u} [Monoid ω] (x : ContT.Label (α × ω) m β) (i : α) : ContT.goto (WriterT.mkLabel' x) i = monadLift (ContT.goto x (i, 1))

def WriterT.callCC {m : Type u → Type v} [Monad m] [MonadCont m] {α : Type u} {β : Type u} {ω : Type u} [EmptyCollection ω] (f : ContT.Label α (WriterT ω m) β → WriterT ω m α) : WriterT ω m α

Equations

• WriterT.callCC f = WriterT.mk (MonadCont.callCC (WriterT.run ∘ f ∘ WriterT.mkLabel))

def WriterT.callCC' {m : Type u → Type v} [Monad m] [MonadCont m] {α : Type u} {β : Type u} {ω : Type u} [Monoid ω] (f : ContT.Label α (WriterT ω m) β → WriterT ω m α) : WriterT ω m α

Equations

• WriterT.callCC' f = WriterT.mk (MonadCont.callCC (WriterT.run ∘ f ∘ WriterT.mkLabel'))

instance instMonadContWriterT {m : Type u → Type v} (ω : Type u) [Monad m] [EmptyCollection ω] [MonadCont m] : MonadCont (WriterT ω m)

Equations

• instMonadContWriterT ω = { callCC := fun {α β} => WriterT.callCC }

instance instMonadContWriterT_1 {m : Type u → Type v} (ω : Type u) [Monad m] [Monoid ω] [MonadCont m] : MonadCont (WriterT ω m)

Equations

• instMonadContWriterT_1 ω = { callCC := fun {α β} => WriterT.callCC' }

def StateT.mkLabel {m : Type u → Type v} {α : Type u} {β : Type u} {σ : Type u} : ContT.Label (α × σ) m (β × σ) → ContT.Label α (StateT σ m) β

Equations

• StateT.mkLabel x = match x with | { apply := f } => { apply := fun a => StateT.mk fun s => f (a, s) }

theorem StateT.goto_mkLabel {m : Type u → Type v} {α : Type u} {β : Type u} {σ : Type u} (x : ContT.Label (α × σ) m (β × σ)) (i : α) : ContT.goto (StateT.mkLabel x) i = StateT.mk fun s => ContT.goto x (i, s)

def StateT.callCC {m : Type u → Type v} {σ : Type u} [MonadCont m] {α : Type u} {β : Type u} (f : ContT.Label α (StateT σ m) β → StateT σ m α) : StateT σ m α

Equations

• StateT.callCC f = StateT.mk fun r => MonadCont.callCC fun f' => StateT.run (f (StateT.mkLabel f')) r

instance instMonadContStateT {m : Type u → Type v} {σ : Type u} [MonadCont m] : MonadCont (StateT σ m)

Equations

• instMonadContStateT = { callCC := fun {α β} => StateT.callCC }

instance instLawfulMonadContStateTInstMonadStateTInstMonadContStateT {m : Type u → Type v} [Monad m] {σ : Type u} [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (StateT σ m)

Equations

• @instLawfulMonadContStateTInstMonadStateTInstMonadContStateT = @instLawfulMonadContStateTInstMonadStateTInstMonadContStateT.proof_1

def ReaderT.mkLabel {m : Type u → Type v} {α : Type u_1} {β : Type u} (ρ : Type u) : ContT.Label α m β → ContT.Label α (ReaderT ρ m) β

Equations

• ReaderT.mkLabel ρ x = match x with | { apply := f } => { apply := monadLift ∘ f }

theorem ReaderT.goto_mkLabel {m : Type u → Type v} {α : Type u_1} {ρ : Type u} {β : Type u} (x : ContT.Label α m β) (i : α) : ContT.goto (ReaderT.mkLabel ρ x) i = monadLift (ContT.goto x i)

def ReaderT.callCC {m : Type u → Type v} {ε : Type u} [MonadCont m] {α : Type u} {β : Type u} (f : ContT.Label α (ReaderT ε m) β → ReaderT ε m α) : ReaderT ε m α

Equations

• ReaderT.callCC f = ReaderT.mk fun r => MonadCont.callCC fun f' => ReaderT.run (f (ReaderT.mkLabel ε f')) r

instance instMonadContReaderT {m : Type u → Type v} {ρ : Type u} [MonadCont m] : MonadCont (ReaderT ρ m)

Equations

• instMonadContReaderT = { callCC := fun {α β} => ReaderT.callCC }

instance instLawfulMonadContReaderTInstMonadReaderTInstMonadContReaderT {m : Type u → Type v} [Monad m] {ρ : Type u} [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (ReaderT ρ m)

Equations

• @instLawfulMonadContReaderTInstMonadReaderTInstMonadContReaderT = @instLawfulMonadContReaderTInstMonadReaderTInstMonadContReaderT.proof_1

def ContT.equiv {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} {α₁ : Type u₀} {r₁ : Type u₀} {α₂ : Type u₁} {r₂ : Type u₁} (F : m₁ r₁ ≃ m₂ r₂) (G : α₁ ≃ α₂) : ContT r₁ m₁ α₁ ≃ ContT r₂ m₂ α₂

reduce the equivalence between two continuation passing monads to the equivalence between their underlying monad

Equations

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