Documentation

Init.Control.ExceptCps

The Exception monad transformer using CPS style.

def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) :
Type (max (u + 1) v)

Adds exceptions of type ε to a monad m.

Instead of using Except ε to model exceptions, this implementation uses continuation passing style. This has different performance characteristics from ExceptT ε.

Equations
    Instances For
      @[inline]
      def ExceptCpsT.run {m : Type u → Type u_1} {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) :
      m (Except ε α)

      Use a monadic action that may throw an exception as an action that may return an exception's value.

      Equations
        Instances For
          @[inline]
          def ExceptCpsT.runK {m : Type u → Type u_1} {β ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : αm β) (error : εm β) :
          m β

          Use a monadic action that may throw an exception by providing explicit success and failure continuations.

          Equations
            Instances For
              @[inline]
              def ExceptCpsT.runCatch {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : ExceptCpsT α m α) :
              m α

              Returns the value of a computation, forgetting whether it was an exception or a success.

              This corresponds to early return.

              Equations
                Instances For
                  @[always_inline]
                  instance ExceptCpsT.instMonad {ε : Type u_1} {m : Type u_1 → Type u_2} :
                  Equations
                    instance ExceptCpsT.instLawfulMonad {σ : Type u_1} {m : Type u_1 → Type u_2} :
                    instance ExceptCpsT.instMonadExceptOf {ε : Type u_1} {m : Type u_1 → Type u_2} :
                    Equations
                      @[inline]
                      def ExceptCpsT.lift {m : Type u_1 → Type u_2} {α ε : Type u_1} [Monad m] (x : m α) :
                      ExceptCpsT ε m α

                      Run an action from the transformed monad in the exception monad.

                      Equations
                        Instances For
                          instance ExceptCpsT.instMonadLiftOfMonad {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] :
                          Equations
                            instance ExceptCpsT.instInhabited {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [Inhabited ε] :
                            Equations
                              @[simp]
                              theorem ExceptCpsT.run_pure {m : Type u_1 → Type u_2} {ε α : Type u_1} {x : α} [Monad m] :
                              @[simp]
                              theorem ExceptCpsT.run_lift {m : Type u → Type u_1} {α ε : Type u} [Monad m] (x : m α) :
                              (lift x).run = do let ax pure (Except.ok a)
                              @[simp]
                              theorem ExceptCpsT.run_throw {m : Type u_1 → Type u_2} {ε β : Type u_1} {e : ε} [Monad m] :
                              @[simp]
                              theorem ExceptCpsT.run_bind_lift {m : Type u_1 → Type u_2} {α ε β : Type u_1} [Monad m] (x : m α) (f : αExceptCpsT ε m β) :
                              (lift x >>= f).run = do let ax (f a).run
                              @[simp]
                              theorem ExceptCpsT.run_bind_throw {m : Type u_1 → Type u_2} {ε α β : Type u_1} [Monad m] (e : ε) (f : αExceptCpsT ε m β) :
                              (throw e >>= f).run = (throw e).run
                              @[simp]
                              theorem ExceptCpsT.runCatch_pure {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} [Monad m] :
                              @[simp]
                              theorem ExceptCpsT.runCatch_lift {m : Type u → Type u_1} {α : Type u} [Monad m] [LawfulMonad m] (x : m α) :
                              @[simp]
                              theorem ExceptCpsT.runCatch_throw {m : Type u_1 → Type u_2} {α : Type u_1} {a : α} [Monad m] :
                              @[simp]
                              theorem ExceptCpsT.runCatch_bind_lift {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] (x : m α) (f : αExceptCpsT β m β) :
                              (lift x >>= f).runCatch = do let ax (f a).runCatch
                              @[simp]
                              theorem ExceptCpsT.runCatch_bind_throw {m : Type u_1 → Type u_2} {β α : Type u_1} [Monad m] (e : β) (f : αExceptCpsT β m β) :