Documentation

Lake.Util.EStateT

inductive Lake.EResult (ε : Type u) (σ : Type v) (α : Type w) :
Type (max u v w)

EResult ε σ α is equivalent to Except ε α × σ, but using a single combined inductive yields a more efficient data representation.

  • ok: {ε : Type u} → {σ : Type v} → {α : Type w} → ασLake.EResult ε σ α

    A success value of type α, and a new state σ.

  • error: {ε : Type u} → {σ : Type v} → {α : Type w} → εσLake.EResult ε σ α

    A failure value of type ε, and a new state σ.

Instances For
    instance Lake.instInhabitedEResult {α : Type u_1} {σ : Type u_2} {ε : Type u_3} [Inhabited α] [Inhabited σ] :
    Equations
    instance Lake.instInhabitedEResult_1 {ε : Type u_1} {σ : Type u_2} {α : Type u_3} [Inhabited ε] [Inhabited σ] :
    Equations
    @[inline]
    def Lake.EResult.state {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
    Lake.EResult ε σ ασ

    Extract the state σ from a EResult ε σ α.

    Equations
    Instances For
      @[inline]
      def Lake.EResult.modifyState {σ : Type u_1} {σ' : Type u_2} {ε : Type u_3} {α : Type u_4} (f : σσ') :
      Lake.EResult ε σ αLake.EResult ε σ' α
      Equations
      Instances For
        @[inline]
        def Lake.EResult.setState {σ' : Type u_1} {ε : Type u_2} {σ : Type u_3} {α : Type u_4} (s : σ') (r : Lake.EResult ε σ α) :
        Lake.EResult ε σ' α
        Equations
        Instances For
          @[inline]
          def Lake.EResult.toProd {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
          Lake.EResult ε σ αExcept ε α × σ

          Convert a EResult ε σ α into Except ε α × σ.

          Equations
          Instances For
            @[inline]
            def Lake.EResult.toProd? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
            Lake.EResult ε σ αOption α × σ

            Convert an EResult ε σ α into Option α × σ, discarding the exception contents.

            Equations
            Instances For
              @[inline]
              def Lake.EResult.result? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
              Lake.EResult ε σ αOption α

              Extract the result α from a EResult ε σ α.

              Equations
              Instances For
                @[inline]
                def Lake.EResult.error? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
                Lake.EResult ε σ αOption ε

                Extract the error ε from a EResult ε σ α.

                Equations
                Instances For
                  @[inline]
                  def Lake.EResult.toExcept {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
                  Lake.EResult ε σ αExcept ε α

                  Convert an EResult ε σ α into Except ε α, discarding its state.

                  Equations
                  Instances For
                    @[inline]
                    def Lake.EResult.map {α : Type u_1} {β : Type u_2} {ε : Type u_3} {σ : Type u_4} (f : αβ) :
                    Lake.EResult ε σ αLake.EResult ε σ β
                    Equations
                    Instances For
                      instance Lake.instFunctorEResult {ε : Type u_1} {σ : Type u_2} :
                      Equations
                      • Lake.instFunctorEResult = { map := fun {α β : Type ?u.24} => Lake.EResult.map, mapConst := fun {α β : Type ?u.24} => Lake.EResult.map Function.const β }
                      def Lake.EStateT (ε : Type u) (σ : Type v) (m : Type (max u v w) → Type x) (α : Type w) :
                      Type (max v x)

                      EStateT ε σ m is a combined error and state monad transformer, equivalent to ExceptT ε (StateT σ m) but more efficient.

                      Equations
                      Instances For
                        instance Lake.EStateT.instInhabitedOfPure {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Inhabited ε] [Pure m] :
                        Inhabited (Lake.EStateT ε σ m α)
                        Equations
                        @[inline]
                        def Lake.EStateT.run {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max u v w) → Type u_1} (init : σ) (self : Lake.EStateT ε σ m α) :
                        m (Lake.EResult ε σ α)

                        Execute an EStateT on initial state init to get an EResult result.

                        Equations
                        Instances For
                          @[inline]
                          def Lake.EStateT.run' {ε : Type u} {α : Type w} {m : Type (max u w) → Type u_1} {σ : Type (max u w)} [Functor m] (init : σ) (x : Lake.EStateT ε σ m α) :
                          m (Except ε α)

                          Execute an EStateT on initial state init to get an Except result, discarding the final state.

                          Equations
                          Instances For
                            @[inline]
                            def Lake.EStateT.toStateT {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [Functor m] (x : Lake.EStateT ε σ m α) :
                            StateT σ m (Except ε α)

                            Convert an EStateT to a StateT, returning an Except result.

                            Equations
                            • x.toStateT s = Lake.EResult.toProd <$> x s
                            Instances For
                              @[inline]
                              def Lake.EStateT.toStateT? {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [Functor m] (x : Lake.EStateT ε σ m α) :
                              StateT σ m (Option α)

                              Convert an EStateT to a StateT, returning an Option result.

                              Equations
                              • x.toStateT? s = Lake.EResult.toProd? <$> x s
                              Instances For
                                @[inline]
                                def Lake.EStateT.run? {σ : Type v} {α : Type w} {m : Type (max v w) → Type u_1} {ε : Type (max v w)} [Functor m] (init : σ) (x : Lake.EStateT ε σ m α) :
                                m (Option α × σ)

                                Execute an EStateT on initial state init to get an Option result, discarding the exception contents.

                                Equations
                                Instances For
                                  @[inline]
                                  def Lake.EStateT.run?' {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [Functor m] (init : σ) (x : Lake.EStateT ε σ m α) :
                                  m (Option α)

                                  Execute an EStateT on initial state init to get an Option result, discarding the final state.

                                  Equations
                                  Instances For
                                    @[inline]
                                    def Lake.EStateT.catchExceptions {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [Monad m] (x : Lake.EStateT ε σ m α) (h : εStateT σ m α) :
                                    StateT σ m α
                                    Equations
                                    Instances For
                                      @[inline]
                                      def Lake.EStateT.lift {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [Monad m] (x : m α) :
                                      Lake.EStateT ε σ m α

                                      Lift the m monad into the EStateT ε σ m monad transformer.

                                      Equations
                                      Instances For
                                        instance Lake.EStateT.instMonadLiftOfMonad {m : Type u → Type u_1} {ε : Type u} {σ : Type u} [Monad m] :
                                        Equations
                                        • Lake.EStateT.instMonadLiftOfMonad = { monadLift := fun {α : Type ?u.32} => Lake.EStateT.lift }
                                        @[inline]
                                        def Lake.EStateT.pure {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (a : α) :
                                        Lake.EStateT ε σ m α

                                        The pure operation of the EStateT monad transformer.

                                        Equations
                                        Instances For
                                          instance Lake.EStateT.instPure {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Pure m] :
                                          Pure (Lake.EStateT ε σ m)
                                          Equations
                                          • Lake.EStateT.instPure = { pure := fun {α : Type ?u.32} => Lake.EStateT.pure }
                                          @[inline]
                                          def Lake.EStateT.map {ε : Type u} {σ : Type v} {α : Type w} {β : Type w} {m : Type (max (max u v) w) → Type u_1} [Functor m] (f : αβ) (x : Lake.EStateT ε σ m α) :
                                          Lake.EStateT ε σ m β

                                          The map operation of the EStateT monad transformer.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            instance Lake.EStateT.instFunctor {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Functor m] :
                                            Equations
                                            • Lake.EStateT.instFunctor = { map := fun {α β : Type ?u.37} => Lake.EStateT.map, mapConst := fun {α β : Type ?u.37} => Lake.EStateT.map Function.const β }
                                            @[inline]
                                            def Lake.EStateT.bind {ε : Type u} {σ : Type v} {α : Type w} {β : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : Lake.EStateT ε σ m α) (f : αLake.EStateT ε σ m β) :
                                            Lake.EStateT ε σ m β

                                            The bind operation of the EStateT monad transformer.

                                            Equations
                                            Instances For
                                              @[inline]
                                              def Lake.EStateT.seqRight {ε : Type u} {σ : Type v} {α : Type w} {β : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : Lake.EStateT ε σ m α) (y : UnitLake.EStateT ε σ m β) :
                                              Lake.EStateT ε σ m β

                                              The seqRight operation of the EStateT monad transformer.

                                              Equations
                                              Instances For
                                                @[always_inline]
                                                instance Lake.EStateT.instMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Monad m] :
                                                Equations
                                                • Lake.EStateT.instMonad = Monad.mk
                                                @[inline]
                                                def Lake.EStateT.set {ε : Type u} {σ : Type v} {m : Type (max (max u v) w) → Type u_1} [Pure m] (s : σ) :

                                                The set operation of the EStateT monad.

                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def Lake.EStateT.get {ε : Type u} {σ : Type v} {m : Type (max u v) → Type u_1} [Pure m] :
                                                  Lake.EStateT ε σ m σ

                                                  The get operation of the EStateT monad.

                                                  Equations
                                                  Instances For
                                                    @[inline]
                                                    def Lake.EStateT.modifyGet {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (f : σα × σ) :
                                                    Lake.EStateT ε σ m α

                                                    The modifyGet operation of the EStateT monad transformer.

                                                    Equations
                                                    Instances For
                                                      instance Lake.EStateT.instMonadStateOfOfPure {ε : Type u} {σ : Type v} {m : Type (max u v) → Type u_1} [Pure m] :
                                                      Equations
                                                      • Lake.EStateT.instMonadStateOfOfPure = { get := Lake.EStateT.get, set := Lake.EStateT.set, modifyGet := fun {α : Type ?u.32} => Lake.EStateT.modifyGet }
                                                      @[inline]
                                                      def Lake.EStateT.throw {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (e : ε) :
                                                      Lake.EStateT ε σ m α

                                                      The throw operation of the EStateT monad transformer.

                                                      Equations
                                                      Instances For
                                                        @[inline]
                                                        def Lake.EStateT.tryCatch {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : Lake.EStateT ε σ m α) (handle : εLake.EStateT ε σ m α) :
                                                        Lake.EStateT ε σ m α
                                                        Equations
                                                        • x.tryCatch handle s = do let __do_liftx s match __do_lift with | Lake.EResult.error e s => handle e s | ok => pure ok
                                                        Instances For
                                                          instance Lake.EStateT.instMonadExceptOfOfMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Monad m] :
                                                          Equations
                                                          • Lake.EStateT.instMonadExceptOfOfMonad = { throw := fun {α : Type ?u.33} => Lake.EStateT.throw, tryCatch := fun {α : Type ?u.33} => Lake.EStateT.tryCatch }
                                                          @[inline]
                                                          def Lake.EStateT.orElse {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x₁ : Lake.EStateT ε σ m α) (x₂ : UnitLake.EStateT ε σ m α) :
                                                          Lake.EStateT ε σ m α
                                                          Equations
                                                          Instances For
                                                            instance Lake.EStateT.instOrElseOfMonad {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] :
                                                            OrElse (Lake.EStateT ε σ m α)
                                                            Equations
                                                            • Lake.EStateT.instOrElseOfMonad = { orElse := Lake.EStateT.orElse }
                                                            @[inline]
                                                            def Lake.EStateT.adaptExcept {ε : Type u} {ε' : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Functor m] (f : εε') (x : Lake.EStateT ε σ m α) :
                                                            Lake.EStateT ε' σ m α

                                                            Map the exception type of a EStateT ε σ m α by a function f : ε → ε'.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[always_inline]
                                                              instance Lake.EStateT.instMonadFinallyOfMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Monad m] :
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.