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σ.
instance
Lake.instInhabitedEResult
{α : Type u_1}
{σ : Type u_2}
{ε : Type u_3}
[Inhabited α]
[Inhabited σ]
:
Inhabited (Lake.EResult ε σ α)
Equations
- Lake.instInhabitedEResult = { default := Lake.EResult.ok default default }
instance
Lake.instInhabitedEResult_1
{ε : Type u_1}
{σ : Type u_2}
{α : Type u_3}
[Inhabited ε]
[Inhabited σ]
:
Inhabited (Lake.EResult ε σ α)
Equations
- Lake.instInhabitedEResult_1 = { default := Lake.EResult.error default default }
@[inline]
Extract the state σ from a EResult ε σ α.
Equations
- (Lake.EResult.ok a s).state = s
- (Lake.EResult.error a s).state = s
@[inline]
def
Lake.EResult.modifyState
{σ : Type u_1}
{σ' : Type u_2}
{ε : Type u_3}
{α : Type u_4}
(f : σ → σ')
:
Lake.EResult ε σ α → Lake.EResult ε σ' α
Equations
- Lake.EResult.modifyState f (Lake.EResult.ok a s) = Lake.EResult.ok a (f s)
- Lake.EResult.modifyState f (Lake.EResult.error e s) = Lake.EResult.error e (f s)
@[inline]
def
Lake.EResult.setState
{σ' : Type u_1}
{ε : Type u_2}
{σ : Type u_3}
{α : Type u_4}
(s : σ')
(r : Lake.EResult ε σ α)
:
Lake.EResult ε σ' α
Equations
- Lake.EResult.setState s r = Lake.EResult.modifyState (fun (x : σ) => s) r
@[inline]
def
Lake.EResult.toProd
{ε : Type u_1}
{σ : Type u_2}
{α : Type u_3}
:
Lake.EResult ε σ α → Except ε α × σ
Convert a EResult ε σ α into Except ε α × σ.
Equations
- (Lake.EResult.ok a s).toProd = (Except.ok a, s)
- (Lake.EResult.error a s).toProd = (Except.error a, s)
@[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
- (Lake.EResult.ok a s).toProd? = (some a, s)
- (Lake.EResult.error a s).toProd? = (none, s)
@[inline]
def
Lake.EResult.result?
{ε : Type u_1}
{σ : Type u_2}
{α : Type u_3}
:
Lake.EResult ε σ α → Option α
Extract the result α from a EResult ε σ α.
Equations
- (Lake.EResult.ok a a_1).result? = some a
- x.result? = none
@[inline]
Extract the error ε from a EResult ε σ α.
Equations
- (Lake.EResult.error e a).error? = some e
- x.error? = none
@[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
- (Lake.EResult.ok a s).toExcept = Except.ok a
- (Lake.EResult.error a s).toExcept = Except.error a
@[inline]
def
Lake.EResult.map
{α : Type u_1}
{β : Type u_2}
{ε : Type u_3}
{σ : Type u_4}
(f : α → β)
:
Lake.EResult ε σ α → Lake.EResult ε σ β
Equations
- Lake.EResult.map f (Lake.EResult.ok a s) = Lake.EResult.ok (f a) s
- Lake.EResult.map f (Lake.EResult.error e s) = Lake.EResult.error e s
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
- Lake.EStateT ε σ m α = (σ → m (Lake.EResult ε σ α))
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
- Lake.EStateT.instInhabitedOfPure = { default := fun (s : σ) => pure (Lake.EResult.error default s) }
@[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
- Lake.EStateT.run init self = self init
@[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
- Lake.EStateT.run' init x = Lake.EResult.toExcept <$> x init
@[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 α)
:
Execute an EStateT on initial state init
to get an Option result, discarding the exception contents.
Equations
- Lake.EStateT.run? init x = Lake.EResult.toProd? <$> x init
@[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
- Lake.EStateT.run?' init x = Lake.EResult.result? <$> x init
@[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
- x.catchExceptions h s = do let __do_lift ← x s match __do_lift with | Lake.EResult.ok a s => pure (a, s) | Lake.EResult.error e s => h e s
@[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
- Lake.EStateT.lift x s = do let a ← x pure (Lake.EResult.ok a s)
@[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
- Lake.EStateT.pure a s = pure (Lake.EResult.ok a s)
@[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.
instance
Lake.EStateT.instFunctor
{ε : Type u}
{σ : Type v}
{m : Type (max (max u v) u_1) → Type u_2}
[Functor m]
:
Functor (Lake.EStateT ε σ 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
- x.bind f s = do let __do_lift ← x s match __do_lift with | Lake.EResult.ok a s => f a s | Lake.EResult.error e s => pure (Lake.EResult.error e s)
@[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 : Unit → Lake.EStateT ε σ m β)
:
Lake.EStateT ε σ m β
The seqRight operation of the EStateT monad transformer.
Equations
- x.seqRight y s = do let __do_lift ← x s match __do_lift with | Lake.EResult.ok a s => y () s | Lake.EResult.error e s => pure (Lake.EResult.error e s)
@[always_inline]
instance
Lake.EStateT.instMonad
{ε : Type u}
{σ : Type v}
{m : Type (max (max u v) u_1) → Type u_2}
[Monad m]
:
Monad (Lake.EStateT ε σ 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 : σ)
:
Lake.EStateT ε σ m PUnit
The set operation of the EStateT monad.
Equations
- Lake.EStateT.set s x = pure (Lake.EResult.ok PUnit.unit s)
@[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
- Lake.EStateT.get s = pure (Lake.EResult.ok s s)
@[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
- Lake.EStateT.modifyGet f s = match f s with | (a, s) => pure (Lake.EResult.ok a s)
instance
Lake.EStateT.instMonadStateOfOfPure
{ε : Type u}
{σ : Type v}
{m : Type (max u v) → Type u_1}
[Pure m]
:
MonadStateOf σ (Lake.EStateT ε σ m)
@[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
- Lake.EStateT.throw e s = pure (Lake.EResult.error e s)
@[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_lift ← x s match __do_lift with | Lake.EResult.error e s => handle e s | ok => pure ok
instance
Lake.EStateT.instMonadExceptOfOfMonad
{ε : Type u}
{σ : Type v}
{m : Type (max (max u v) u_1) → Type u_2}
[Monad m]
:
MonadExceptOf ε (Lake.EStateT ε σ m)
@[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₂ : Unit → Lake.EStateT ε σ m α)
:
Lake.EStateT ε σ m α
Equations
- x₁.orElse x₂ s = do let __do_lift ← x₁ s match __do_lift with | Lake.EResult.error a s => x₂ () s | ok => pure ok
@[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.
@[always_inline]
instance
Lake.EStateT.instMonadFinallyOfMonad
{ε : Type u}
{σ : Type v}
{m : Type (max (max u v) u_1) → Type u_2}
[Monad m]
:
MonadFinally (Lake.EStateT ε σ m)
Equations
- One or more equations did not get rendered due to their size.