Documentation

Mathlib.Control.Monad.Cont

Continuation Monad #

Monad encapsulating continuation passing programming style, similar to Haskell's Cont, ContT and MonadCont:

structure MonadCont.Label (α : Type w) (m : Type u → Type v) (β : Type u) :
Type (max v w)
  • apply : αm β
Instances For
    def MonadCont.goto {α : Type u_1} {β : Type u} {m : Type u → Type v} (f : ContT.Label α m β) (x : α) :
    m β
    Equations
    Instances For
      class MonadCont (m : Type u → Type v) :
      Type (max (u + 1) v)
      Instances
        class LawfulMonadCont (m : Type u → Type v) [Monad m] [MonadCont m] extends LawfulMonad :
        Instances
          theorem LawfulMonadCont.callCC_bind_right {m : Type u → Type v} [Monad m] [MonadCont m] [self : LawfulMonadCont m] {α : Type u} {ω : Type u} {γ : Type u} (cmd : m α) (next : ContT.Label ω m γαm ω) :
          (MonadCont.callCC fun (f : ContT.Label ω m γ) => cmd >>= next f) = do let xcmd MonadCont.callCC fun (f : ContT.Label ω m γ) => next f x
          theorem LawfulMonadCont.callCC_bind_left {m : Type u → Type v} [Monad m] [MonadCont m] [self : LawfulMonadCont m] {α : Type u} (β : Type u) (x : α) (dead : ContT.Label α m ββm α) :
          (MonadCont.callCC fun (f : ContT.Label α m β) => ContT.goto f x >>= dead f) = pure x
          theorem LawfulMonadCont.callCC_dummy {m : Type u → Type v} [Monad m] [MonadCont m] [self : LawfulMonadCont m] {α : Type u} {β : Type u} (dummy : m α) :
          (MonadCont.callCC fun (x : ContT.Label α m β) => 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)
          Instances For
            @[reducible, inline]
            abbrev Cont (r : Type u) (α : Type w) :
            Type (max u w)
            Equations
            Instances For
              def ContT.run {r : Type u} {m : Type u → Type v} {α : Type w} :
              ContT r m α(αm r)m r
              Equations
              • ContT.run = id
              Instances For
                def ContT.map {r : Type u} {m : Type u → Type v} {α : Type w} (f : m rm r) (x : ContT r m α) :
                ContT r m α
                Equations
                Instances For
                  theorem ContT.run_contT_map_contT {r : Type u} {m : Type u → Type v} {α : Type w} (f : m rm r) (x : ContT r m α) :
                  (ContT.map f x).run = f x.run
                  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
                  Instances For
                    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.withContT f x).run = x.run 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), x.run f = y.run f) :
                    x = y
                    instance ContT.instMonad {r : Type u} {m : Type u → Type v} :
                    Monad (ContT r m)
                    Equations
                    • ContT.instMonad = Monad.mk
                    instance ContT.instLawfulMonad {r : Type u} {m : Type u → Type v} :
                    Equations
                    • =
                    def ContT.monadLift {r : Type u} {m : Type u → Type v} [Monad m] {α : Type u} :
                    m αContT r m α
                    Equations
                    Instances For
                      instance ContT.instMonadLiftOfMonad {r : Type u} {m : Type u → Type v} [Monad m] :
                      Equations
                      • ContT.instMonadLiftOfMonad = { monadLift := fun {α : Type u} => 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.instMonadCont {r : Type u} {m : Type u → Type v} :
                      Equations
                      • ContT.instMonadCont = { callCC := fun {α β : Type u_1} (f : ContT.Label α (ContT r m) βContT r m α) (g : αm r) => f { apply := fun (x : α) (x_1 : βm r) => g x } g }
                      instance ContT.instLawfulMonadCont {r : Type u} {m : Type u → Type v} :
                      Equations
                      • =
                      instance ContT.instMonadExcept {r : Type u} {m : Type u → Type v} (ε : Type u_1) [MonadExcept ε m] :
                      Equations
                      • One or more equations did not get rendered due to their size.
                      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
                      Instances For
                        theorem ExceptT.goto_mkLabel {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} {ε : Type u} (x : ContT.Label (Except ε α) m β) (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
                        Instances For
                          instance instMonadContExceptT {m : Type u → Type v} [Monad m] {ε : Type u} [MonadCont m] :
                          Equations
                          • instMonadContExceptT = { callCC := fun {α β : Type u} => ExceptT.callCC }
                          instance instLawfulMonadContExceptT {m : Type u → Type v} [Monad m] {ε : Type u} [MonadCont m] [LawfulMonadCont m] :
                          Equations
                          • =
                          def OptionT.mkLabel {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} :
                          ContT.Label (Option α) m βContT.Label α (OptionT m) β
                          Equations
                          Instances For
                            theorem OptionT.goto_mkLabel {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (x : ContT.Label (Option α) m β) (i : α) :
                            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
                            Instances For
                              instance instMonadContOptionT {m : Type u → Type v} [Monad m] [MonadCont m] :
                              Equations
                              • instMonadContOptionT = { callCC := fun {α β : Type u} => OptionT.callCC }
                              Equations
                              • =
                              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
                              Instances For
                                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
                                Instances For
                                  theorem WriterT.goto_mkLabel {m : Type u → Type v} [Monad m] {α : Type u_1} {β : Type u} {ω : Type u} [EmptyCollection ω] (x : ContT.Label (α × ω) m β) (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 : α) :
                                  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
                                  Instances For
                                    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
                                    Instances For
                                      Equations
                                      instance instMonadContWriterTOfMonadOfMonoid {m : Type u → Type v} (ω : Type u) [Monad m] [Monoid ω] [MonadCont m] :
                                      Equations
                                      def StateT.mkLabel {m : Type u → Type v} {α : Type u} {β : Type u} {σ : Type u} :
                                      ContT.Label (α × σ) m (β × σ)ContT.Label α (StateT σ m) β
                                      Equations
                                      Instances For
                                        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
                                        Instances For
                                          instance instMonadContStateT {m : Type u → Type v} {σ : Type u} [MonadCont m] :
                                          Equations
                                          • instMonadContStateT = { callCC := fun {α β : Type u} => StateT.callCC }
                                          instance instLawfulMonadContStateT {m : Type u → Type v} [Monad m] {σ : Type u} [MonadCont m] [LawfulMonadCont m] :
                                          Equations
                                          • =
                                          def ReaderT.mkLabel {m : Type u → Type v} {α : Type u_1} {β : Type u} (ρ : Type u) :
                                          ContT.Label α m βContT.Label α (ReaderT ρ m) β
                                          Equations
                                          Instances For
                                            theorem ReaderT.goto_mkLabel {m : Type u → Type v} {α : Type u_1} {ρ : Type u} {β : Type u} (x : ContT.Label α m β) (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
                                            Instances For
                                              instance instMonadContReaderT {m : Type u → Type v} {ρ : Type u} [MonadCont m] :
                                              Equations
                                              • instMonadContReaderT = { callCC := fun {α β : Type u} => ReaderT.callCC }
                                              instance instLawfulMonadContReaderT {m : Type u → Type v} [Monad m] {ρ : Type u} [MonadCont m] [LawfulMonadCont m] :
                                              Equations
                                              • =
                                              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.
                                              Instances For