The IO monad has many, many effects, and is used for writing programs that need to interact with the world.
It is described in its own section.
Programs that use IO are essentially black boxes: they are typically not particularly amenable to verification.
Many algorithms are easiest to express with a much smaller set of effects. These effects can often be simulated; for example, mutable state can be simulated by passing around a tuple that contains both the program's value and the state. These simulated effects are easier to reason formally about, because they are defined using ordinary code rather than new language primitives.
The standard library provides abstractions for working with commonly-used effects. Many frequently-used effects fall into a small number of categories:
Computations that have access to some data that may be modified by other parts of the computation use mutable state.
State can be implemented in a variety of ways, described in the section on state monads and captured in the MonadState type class.
Computations that can read the value of some parameter provided by a context exist in most programming languages, but many languages that feature state and exceptions as first-class features do not have built-in facilities for defining new parameterized computations.
Typically, these computations are provided with a parameter value when invoked, and sometimes they can locally override it.
Parameter values have dynamic extent: the value provided most recently in the call stack is the one that is used.
They can be simulated by passing a value unchanged through a sequence of function calls; however, this technique can make code harder to read and introduces a risk that the values may be passed incorrectly to further calls by mistake.
They can also be simulated using mutable state with a careful discipline surrounding the modification of the state.
Monads that maintain a parameter, potentially allowing it to be overridden in a section of the call stack, are called reader monads.
Reader monads are captured in the MonadReader type class.
Additionally, reader monads that allow the parameter value to be locally overridden are captured in the MonadWithReader type class.
Computations that may terminate early with an exceptional value use exceptions.
They are typically modeled with a sum type that has a constructor for ordinary termination and a constructor for early termination with errors.
Exception monads are described in the section on exception monads, and captured in the MonadExcept type class.
Using type classes like MonadState and MonadExcept allow client code to be polymorphic with respect to monads.
Together with automatic lifting, this allows programs to be re-usable in many different monads and makes them more robust to refactoring.
It's important to be aware that effects in a monad may not interact in only one way. For example, a monad with state and exceptions may or may not roll back state changes when an exception is thrown. If this matters for the correctness of a function, then it should use a more specific signature.
The function sumNonFives adds the contents of a list using a state monad, terminating early if it encounters a 5.
def sumNonFives {m}
[Monad m] [MonadState Nat m] [MonadExcept String m]
(xs : List Nat) :
m Unit := do
for x in xs do
if x == 5 then
throw "Five was encountered"
else
modify (· + x)
Running it in one monad returns the state at the time that 5 was encountered:
#eval
sumNonFives (m := ExceptT String (StateM Nat))
[1, 2, 3, 4, 5, 6] |>.run |>.run 0
(Except.error "Five was encountered", 10)
In another, the state is discarded:
#eval
sumNonFives (m := StateT Nat (Except String))
[1, 2, 3, 4, 5, 6] |>.run 0
Except.error "Five was encountered"
In the second case, an exception handler would roll back the state to its value at the start of the Lean.Parser.Term.termTry : termtry.
The following function is thus incorrect:
/-- Computes the sum of the non-5 prefix of a list. -/
def sumUntilFive {m}
[Monad m] [MonadState Nat m] [MonadExcept String m]
(xs : List Nat) :
m Nat := do
MonadState.set 0
try
sumNonFives xs
catch _ =>
pure ()
get
In one monad, the answer is correct:
#eval
sumUntilFive (m := ExceptT String (StateM Nat))
[1, 2, 3, 4, 5, 6] |>.run |>.run' 0
Except.ok 10
In the other, it is not:
#eval
sumUntilFive (m := StateT Nat (Except String))
[1, 2, 3, 4, 5, 6] |>.run' 0
Except.ok 0
A single monad may support multiple version of the same effect.
For example, there might be a mutable Nat and a mutable String or two separate reader parameters.
As long as they have different types, it should be convenient to access both.
In typical use, some monadic operations that are overloaded in type classes have type information available for instance synthesis, while others do not.
For example, the argument passed to set determines the type of the state to be used, while get takes no such argument.
The type information present in applications of set can be used to pick the correct instance when multiple states are available, which suggests that the type of the mutable state should be an input parameter or semi-output parameter so that it can be used to select instances.
The lack of type information present in uses of get, on the other hand, suggests that the type of the mutable state should be an output parameter in MonadState, so type class synthesis determines the state's type from the monad itself.
This dichotomy is solved by having two versions of many of the effect type classes.
The version with a semi-output parameter has the suffix -Of, and its operations take types explicitly as needed.
Examples include MonadStateOf, MonadReaderOf, and MonadExceptOf.
The operations with explicit type parameters have names ending in -The, such as getThe, readThe, and tryCatchThe.
The name of the version with an output parameter is undecorated.
The standard library exports a mix of operations from the -Of and undecorated versions of each type class, based on what has good inference behavior in typical use cases.
Operation | From Class | Notes |
|---|---|---|
| Output parameter improves type inference | |
Semi-output parameter uses type information from | ||
Output parameter is needed to allow functions without annotations | ||
| Output parameter is needed to allow functions without annotations | |
Output parameter is needed due to lack of type information from arguments | ||
Semi-output parameter uses the provided type to guide synthesis | ||
Output parameter avoids the need for type annotations on the function | ||
Semi-output parameter uses provided type to guide synthesis | ||
Output parameter enables the use of constructor dot notation for the exception | ||
Semi-output parameter uses provided type to guide synthesis | ||
Output parameter enables the use of constructor dot notation for the exception | ||
Semi-output parameter uses provided type to guide synthesis |
The state monad M has two separate states: a Nat and a String.
abbrev M := StateT Nat (StateM String)
Because get is an alias for MonadState.get, the state type is an output parameter.
This means that Lean selects a state type automatically, in this case the one from the outermost monad transformer:
#check (get : M _)
get : M Nat
Only the outermost may be used, because the type of the state is an output parameter.
#check (get : M String)
failed to synthesize MonadState String M Additional diagnostic information may be available using the `set_option diagnostics true` command.
Providing the state type explicitly using getThe from MonadStateOf allows both states to be read.
#check ((getThe String, getThe Nat) : M String × M Nat)
(getThe String, getThe Nat) : M String × M Nat
Setting a state works for either type, because the state type is a semi-output parameter on MonadStateOf.
#check (set 4 : M Unit)
set 4 : M PUnit
#check (set "Four" : M Unit)
set "Four" : M PUnit
A monad transformer is a function that, when provided with a monad, gives back a new monad. Typically, this new monad has all the effects of the original monad along with some additional ones.
A monad transformer consists of the following:
A function T that constructs the new monad's type from an existing monad
A run function that adapts a T m α into some variant of m, often requiring additional parameters and returning a more specific type under m
An instance of [Monad m] → Monad (T m) that allows the transformed monad to be used as a monad
An instance of MonadLift that allows the original monad's code to be used in the transformed monad
If possible, an instance of MonadControl m (T m) that allows actions from the transformed monad to be used in the original monad
Typically, a monad transformer also provides instances of one or more type classes that describe the effects that it introduces.
The transformer's Monad and MonadLift instances make it practical to write code in the transformed monad, while the type class instances allow the transformed monad to be used with polymorphic functions.
The identity monad transformer neither adds nor removes capabilities to the transformed monad. Its definition is the identity function, suitably specialized:
def IdT (m : Type u → Type v) : Type u → Type v := m
Similarly, the run function requires no additional arguments and just returns an m α:
def IdT.run (act : IdT m α) : m α := act
The monad instance relies on the monad instance for the transformed monad, selecting it via type ascriptions:
instance [Monad m] : Monad (IdT m) where
pure x := (pure x : m _)
bind x f := (x >>= f : m _)
Because IdT m is definitionally equal to m, the MonadLift m (IdT m) instance doesn't need to modify the action being lifted:
instance : MonadLift m (IdT m) where
monadLift x := x
The MonadControl instance is similarly simple.
instance [Monad m] : MonadControl m (IdT m) where
stM α := α
liftWith f := f (fun x => Id.run <| pure x)
restoreM v := v
The Lean standard library provides transformer versions of many different monads, including ReaderT, ExceptT, and StateT, along with variants using other representations such as StateCpsT, StateRefT, and ExceptCpsT.
Additionally, the EStateM monad is equivalent to combining ExceptT and StateT, but it can use a more specialized representation to improve performance.
The identity monad Id has no effects whatsoever.
Both Id and the corresponding implementation of pure are the identity function, and bind is reversed function application.
The identity monad has two primary use cases:
It can be the type of a Lean.Parser.Term.do : termdo block that implements a pure function with local effects.
It can be placed at the bottom of a stack of monad transformers.
Id.{u} (type : Type u) : Type u
Id.run.{u_1} {α : Type u_1} (x : Id α) : α
State monads provide access to a mutable value.
The underlying implementation may a tuple to simulate mutability, or it may use something like ST.Ref to ensure mutation.
Even those implementations that use a tuple may in fact use mutation at run-time due to Lean's use of mutation when there are unique references to values, but this requires a programming style that prefers modify and modifyGet over get and set.
MonadState.{u, v} (σ : outParam (Type u))
(m : Type u → Type v) : Type (max (u + 1) v)
Similar to MonadStateOf, but σ is an outParam for convenience.
MonadState.mk.{u, v} |
get | : | m σ |
| ||
set | : | σ → m PUnit |
| ||
modifyGet | : | {α : Type u} → (σ → α × σ) → m α |
It is equivalent to | ||
MonadState.get.{u, v} {σ : outParam (Type u)} {m : Type u → Type v} [self : MonadState σ m] : m σ
(← get) : σ gets the state out of a monad m.
modify.{u, v} {σ : Type u} {m : Type u → Type v}
[MonadState σ m] (f : σ → σ) : m PUnit
modify (f : σ → σ) applies the function f to the state.
It is equivalent to do set (f (← get)), but modify f may be preferable
because the former does not use the state linearly (without sufficient inlining).
MonadState.modifyGet.{u, v} {σ : outParam (Type u)} {m : Type u → Type v} [self : MonadState σ m] {α : Type u} : (σ → α × σ) → m α
modifyGet (f : σ → α × σ) applies f to the current state, replaces
the state with the return value, and returns a computed value.
It is equivalent to do let (a, s) := f (← get); put s; pure a, but
modifyGet f may be preferable because the former does not use the state
linearly (without sufficient inlining).
getModify.{u, v} {σ : Type u}
{m : Type u → Type v} [MonadState σ m]
(f : σ → σ) : m σ
getModify f gets the state, applies function f, and returns the old value
of the state. It is equivalent to get <* modify f but may be more efficient.
MonadStateOf.{u, v} (σ : semiOutParam (Type u))
(m : Type u → Type v) : Type (max (u + 1) v)
An implementation of MonadState. In contrast to the Haskell implementation,
we use overlapping instances to derive instances automatically from monadLift.
MonadStateOf.mk.{u, v} |
get | : | m σ |
| ||
set | : | σ → m PUnit |
| ||
modifyGet | : | {α : Type u} → (σ → α × σ) → m α |
It is equivalent to | ||
getThe.{u, v} (σ : Type u) {m : Type u → Type v}
[MonadStateOf σ m] : m σ
Like get, but with σ explicit. This is useful if a monad supports
MonadStateOf for multiple different types σ.
modifyThe.{u, v} (σ : Type u)
{m : Type u → Type v} [MonadStateOf σ m]
(f : σ → σ) : m PUnit
Like modify, but with σ explicit. This is useful if a monad supports
MonadStateOf for multiple different types σ.
modifyGetThe.{u, v} {α : Type u} (σ : Type u)
{m : Type u → Type v} [MonadStateOf σ m]
(f : σ → α × σ) : m α
Like modifyGet, but with σ explicit. This is useful if a monad supports
MonadStateOf for multiple different types σ.
The tuple-based state monads represent a computation with states that have type σ yielding values of type α as functions that take a starting state and yield a value paired with a final state, e.g. σ → α × σ.
The Monad operations thread the state correctly through the computation.
StateM.{u} (σ α : Type u) : Type u
StateT.{u, v} (σ : Type u) (m : Type u → Type v)
(α : Type u) : Type (max u v)
StateT.run.{u, v} {σ : Type u}
{m : Type u → Type v} {α : Type u}
(x : StateT σ m α) (s : σ) : m (α × σ)
StateT.orElse.{u, v} {σ : Type u}
{m : Type u → Type v} [Alternative m]
{α : Type u} (x₁ : StateT σ m α)
(x₂ : Unit → StateT σ m α) : StateT σ m α
StateT.failure.{u, v} {σ : Type u}
{m : Type u → Type v} [Alternative m]
{α : Type u} : StateT σ m α
StateT.run'.{u, v} {σ : Type u}
{m : Type u → Type v} [Functor m]
{α : Type u} (x : StateT σ m α) (s : σ)
: m α
StateT.bind.{u, v} {σ : Type u}
{m : Type u → Type v} [Monad m]
{α β : Type u} (x : StateT σ m α)
(f : α → StateT σ m β) : StateT σ m β
StateT.modifyGet.{u, v} {σ : Type u}
{m : Type u → Type v} [Monad m] {α : Type u}
(f : σ → α × σ) : StateT σ m α
StateT.lift.{u, v} {σ : Type u}
{m : Type u → Type v} [Monad m] {α : Type u}
(t : m α) : StateT σ m α
Continuation-passing-style state monads represent stateful computations as functions that, for any type whatsoever, take an initial state and a continuation (modeled as a function) that accepts a value and an updated state.
An example of such a type is (δ : Type u) → σ → (α → σ → δ) → δ, though StateCpsT is a transformer that can be applied to any monad.
State monads in continuation passing style have different performance characteristics than tuple-based state monads; for some applications, it may be worth benchmarking them.
StateCpsT.{u, v} (σ : Type u)
(m : Type u → Type v) (α : Type u)
: Type (max (u + 1) v)
StateCpsT.runK.{u, v} {α σ : Type u}
{m : Type u → Type v} {β : Type u}
(x : StateCpsT σ m α) (s : σ)
(k : α → σ → m β) : m β
The monad StateRefT σ m is a specialized state monad transformer that can be used when m is a monad to which ST computations can be lifted.
It implements the operations of MonadState using an ST.Ref, rather than pure functions.
This ensures that mutation is actually used at run time.
ST and EST require a phantom type parameter that's used together with runST's polymorphic function argument to encapsulate mutability.
Rather than require this as a parameter to the transformer, an auxiliary type class STWorld is used to propagate it directly from m.
The transformer itself is defined as a syntax extension and an elaborator, rather than an ordinary function.
This is because STWorld has no methods: it exists only to propagate information from the inner monad to the transformed monad.
Nonetheless, its instances are terms; keeping them around could lead to unnecessarily large types.
STWorld (σ : outParam Type) (m : Type → Type) : Type
The syntax for StateRefT σ m accepts two arguments:
term ::= ... | StateRefT term (macroDollarArg | term)
Its elaborator synthesizes an instance of STWorld ω m to ensure that m supports mutable references.
Having discovered the value of ω, it then produces the term StateRefT' ω σ m, discarding the synthesized instance.
StateRefT' (ω σ : Type) (m : Type → Type)
(α : Type) : Type
StateRefT'.get {ω σ : Type} {m : Type → Type}
[MonadLiftT (ST ω) m] : StateRefT' ω σ m σ
StateRefT'.set {ω σ : Type} {m : Type → Type}
[MonadLiftT (ST ω) m] (s : σ)
: StateRefT' ω σ m PUnit
StateRefT'.modifyGet {ω σ : Type}
{m : Type → Type} {α : Type}
[MonadLiftT (ST ω) m] (f : σ → α × σ)
: StateRefT' ω σ m α
StateRefT'.run {ω σ : Type} {m : Type → Type}
[Monad m] [MonadLiftT (ST ω) m] {α : Type}
(x : StateRefT' ω σ m α) (s : σ) : m (α × σ)
StateRefT'.run' {ω σ : Type} {m : Type → Type}
[Monad m] [MonadLiftT (ST ω) m] {α : Type}
(x : StateRefT' ω σ m α) (s : σ) : m α
StateRefT'.lift {ω σ : Type} {m : Type → Type}
{α : Type} (x : m α) : StateRefT' ω σ m α
MonadReader.{u, v} (ρ : outParam (Type u))
(m : Type u → Type v) : Type v
Similar to MonadReaderOf, but ρ is an outParam for convenience.
MonadReader.mk.{u, v} |
read | : | m ρ |
| ||
MonadReaderOf.{u, v} (ρ : semiOutParam (Type u))
(m : Type u → Type v) : Type v
An implementation of Haskell's MonadReader (sans functional dependency; see also MonadReader
in this module). It does not contain local because this
function cannot be lifted using monadLift. local is instead provided by
the MonadWithReader class as withReader.
Note: This class can be seen as a simplification of the more "principled" definition
class MonadReaderOf (ρ : Type u) (n : Type u → Type u) where
lift {α : Type u} : ({m : Type u → Type u} → [Monad m] → ReaderT ρ m α) → n α
MonadReaderOf.mk.{u, v} |
read | : | m ρ |
| ||
readThe.{u, v} (ρ : Type u)
{m : Type u → Type v} [MonadReaderOf ρ m]
: m ρ
Like read, but with ρ explicit. This is useful if a monad supports
MonadReaderOf for multiple different types ρ.
MonadWithReader.{u, v} (ρ : outParam (Type u))
(m : Type u → Type v) : Type (max (u + 1) v)
Similar to MonadWithReaderOf, but ρ is an outParam for convenience.
MonadWithReader.mk.{u, v} |
withReader | : | {α : Type u} → (ρ → ρ) → m α → m α |
| ||
MonadWithReaderOf.{u, v}
(ρ : semiOutParam (Type u))
(m : Type u → Type v) : Type (max (u + 1) v)
MonadWithReaderOf ρ adds the operation withReader : (ρ → ρ) → m α → m α.
This runs the inner x : m α inside a modified context after applying the
function f : ρ → ρ. In addition to ReaderT itself, this operation lifts
over most monad transformers, so it allows us to apply withReader to monads
deeper in the stack.
MonadWithReaderOf.mk.{u, v} |
withReader | : | {α : Type u} → (ρ → ρ) → m α → m α |
| ||
withTheReader.{u, v} (ρ : Type u)
{m : Type u → Type v}
[MonadWithReaderOf ρ m] {α : Type u}
(f : ρ → ρ) (x : m α) : m α
Like withReader, but with ρ explicit. This is useful if a monad supports
MonadWithReaderOf for multiple different types ρ.
ReaderT.{u, v} (ρ : Type u)
(m : Type u → Type v) (α : Type u)
: Type (max u v)
An implementation of Haskell's ReaderT. This is a monad transformer which
equips a monad with additional read-only state, of type ρ.
ReaderM.{u} (ρ α : Type u) : Type u
ReaderT.adapt.{u, v} {ρ : Type u}
{m : Type u → Type v} {ρ' α : Type u}
(f : ρ' → ρ)
: ReaderT ρ m α → ReaderT ρ' m α
adapt (f : ρ' → ρ) precomposes function f on the reader state of a
ReaderT ρ, yielding a ReaderT ρ'.
ReaderT.read.{u, v} {ρ : Type u}
{m : Type u → Type v} [Monad m]
: ReaderT ρ m ρ
(← read) : ρ gets the read-only state of a ReaderT ρ.
ReaderT.run.{u, v} {ρ : Type u}
{m : Type u → Type v} {α : Type u}
(x : ReaderT ρ m α) (r : ρ) : m α
If x : ReaderT ρ m α and r : ρ, then x.run r : ρ runs the monad with the
given reader state.
ReaderT.orElse.{u_1, u_2}
{m : Type u_1 → Type u_2} {ρ α : Type u_1}
[Alternative m] (x₁ : ReaderT ρ m α)
(x₂ : Unit → ReaderT ρ m α) : ReaderT ρ m α
ReaderT.bind.{u, v} {ρ : Type u}
{m : Type u → Type v} [Monad m]
{α β : Type u} (x : ReaderT ρ m α)
(f : α → ReaderT ρ m β) : ReaderT ρ m β
The bind operation of the ReaderT monad.
ReaderT.failure.{u_1, u_2}
{m : Type u_1 → Type u_2} {ρ α : Type u_1}
[Alternative m] : ReaderT ρ m α
Ordinarily, Option is thought of as data, similarly to a nullable type.
It can also be considered as a monad, and thus a way of performing computations.
The Option monad and its transformer OptionT can be understood as describing computations that may terminate early, discarding the results.
Callers can check for early termination and invoke a fallback if desired using OrElse.orElse or by treating it as a MonadExcept Unit.
OptionT.{u, v} (m : Type u → Type v)
(α : Type u) : Type v
OptionT.bind.{u, v} {m : Type u → Type v}
[Monad m] {α β : Type u} (x : OptionT m α)
(f : α → OptionT m β) : OptionT m β
Exception monads describe computations that terminate early (fail).
Failing computations provide their caller with an exception value that describes why they failed.
In other words, computations either return a value or an exception.
The inductive type Except captures this pattern, and is itself a monad.
Except.{u, v} (ε : Type u) (α : Type v)
: Type (max u v)
Except ε α is a type which represents either an error of type ε, or an "ok"
value of type α. The error type is listed first because
Except ε : Type → Type is a Monad: the pure operation is ok and the bind
operation returns the first encountered error.
Except.pure.{u, u_1} {ε : Type u} {α : Type u_1}
(a : α) : Except ε α
Except.bind.{u, u_1, u_2} {ε : Type u}
{α : Type u_1} {β : Type u_2}
(ma : Except ε α) (f : α → Except ε β)
: Except ε β
Except.map.{u, u_1, u_2} {ε : Type u}
{α : Type u_1} {β : Type u_2} (f : α → β)
: Except ε α → Except ε β
Except.mapError.{u, u_1, u_2} {ε : Type u}
{ε' : Type u_1} {α : Type u_2} (f : ε → ε')
: Except ε α → Except ε' α
Except.tryCatch.{u, u_1} {ε : Type u}
{α : Type u_1} (ma : Except ε α)
(handle : ε → Except ε α) : Except ε α
MonadExcept.{u, v, w} (ε : outParam (Type u))
(m : Type v → Type w)
: Type (max (max u (v + 1)) w)
Similar to MonadExceptOf, but ε is an outParam for convenience.
MonadExcept.mk.{u, v, w} |
throw | : | {α : Type v} → ε → m α |
| ||
tryCatch | : | {α : Type v} → m α → (ε → m α) → m α |
| ||
MonadExcept.ofExcept.{u_1, u_2, u_3}
{m : Type u_1 → Type u_2} {ε : Type u_3}
{α : Type u_1} [Monad m] [MonadExcept ε m]
: Except ε α → m α
"Unwraps" an Except ε α to get the α, or throws the exception otherwise.
MonadExcept.orElse.{u, v, w} {ε : Type u}
{m : Type v → Type w} [MonadExcept ε m]
{α : Type v} (t₁ : m α) (t₂ : Unit → m α)
: m α
A MonadExcept can implement t₁ <|> t₂ as try t₁ catch _ => t₂.
MonadExcept.orelse'.{u, v, w} {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx : Bool := true) : m α
Alternative orelse operator that allows to select which exception should be used.
The default is to use the first exception since the standard orelse uses the second.
MonadExceptOf.{u, v, w}
(ε : semiOutParam (Type u))
(m : Type v → Type w)
: Type (max (max u (v + 1)) w)
An implementation of Haskell's MonadError class. A MonadError ε m is a
monad m with two operations:
throw : ε → m α "throws an error" of type ε to the nearest enclosing
catch block
tryCatch (body : m α) (handler : ε → m α) : m α will catch any errors in
body and pass the resulting error to handler.
Errors in handler will not be caught.
The try ... catch e => ... syntax inside do blocks is sugar for the
tryCatch operation.
MonadExceptOf.mk.{u, v, w} |
throw | : | {α : Type v} → ε → m α |
| ||
tryCatch | : | {α : Type v} → m α → (ε → m α) → m α |
| ||
throwThe.{u, v, w} (ε : Type u)
{m : Type v → Type w} [MonadExceptOf ε m]
{α : Type v} (e : ε) : m α
This is the same as throw, but allows specifying the particular error type
in case the monad supports throwing more than one type of error.
tryCatchThe.{u, v, w} (ε : Type u)
{m : Type v → Type w} [MonadExceptOf ε m]
{α : Type v} (x : m α) (handle : ε → m α)
: m α
This is the same as tryCatch, but allows specifying the particular error type
in case the monad supports throwing more than one type of error.
MonadFinally.{u, v} (m : Type u → Type v)
: Type (max (u + 1) v)MonadFinally.mk.{u, v} |
tryFinally' | : | {α β : Type u} → m α → (Option α → m β) → m (α × β) |
| ||
ExceptT.{u, v} (ε : Type u)
(m : Type u → Type v) (α : Type u) : Type v
ExceptT.lift.{u, v} {ε : Type u}
{m : Type u → Type v} [Monad m] {α : Type u}
(t : m α) : ExceptT ε m α
ExceptT.run.{u, v} {ε : Type u}
{m : Type u → Type v} {α : Type u}
(x : ExceptT ε m α) : m (Except ε α)
ExceptT.pure.{u, v} {ε : Type u}
{m : Type u → Type v} [Monad m] {α : Type u}
(a : α) : ExceptT ε m α
ExceptT.bind.{u, v} {ε : Type u}
{m : Type u → Type v} [Monad m]
{α β : Type u} (ma : ExceptT ε m α)
(f : α → ExceptT ε m β) : ExceptT ε m β
ExceptT.bindCont.{u, v} {ε : Type u}
{m : Type u → Type v} [Monad m]
{α β : Type u} (f : α → ExceptT ε m β)
: Except ε α → m (Except ε β)
ExceptT.tryCatch.{u, v} {ε : Type u}
{m : Type u → Type v} [Monad m] {α : Type u}
(ma : ExceptT ε m α)
(handle : ε → ExceptT ε m α) : ExceptT ε m α
ExceptT.mk.{u, v} {ε : Type u}
{m : Type u → Type v} {α : Type u}
(x : m (Except ε α)) : ExceptT ε m α
Continuation-passing-style exception monads represent potentially-failing computations as functions that take success and failure continuations, both of which return the same type, returning that type.
They must work for any return type.
An example of such a type is (β : Type u) → (α → β) → (ε → β) → β.
ExceptCpsT is a transformer that can be applied to any monad, so ExceptCpsT ε m α is actually defined as (β : Type u) → (α → m β) → (ε → m β) → m β.
Exception monads in continuation passing style have different performance characteristics than Except-based state monads; for some applications, it may be worth benchmarking them.
ExceptCpsT.{u, v} (ε : Type u)
(m : Type u → Type v) (α : Type u)
: Type (max (u + 1) v)
ExceptCpsT.runCatch.{u_1, u_2}
{m : Type u_1 → Type u_2} {α : Type u_1}
[Monad m] (x : ExceptCpsT α m α) : m α
ExceptCpsT.runK.{u, u_1} {m : Type u → Type u_1}
{β ε α : Type u} (x : ExceptCpsT ε m α)
(s : ε) (ok : α → m β) (error : ε → m β)
: m β
ExceptCpsT.run.{u, u_1} {m : Type u → Type u_1}
{ε α : Type u} [Monad m]
(x : ExceptCpsT ε m α) : m (Except ε α)
ExceptCpsT.lift.{u_1, u_2}
{m : Type u_1 → Type u_2} {α ε : Type u_1}
[Monad m] (x : m α) : ExceptCpsT ε m α
The EStateM monad has both exceptions and mutable state.
EStateM ε σ α is logically equivalent to ExceptT ε (StateM σ) α.
While ExceptT ε (StateM σ) evaluates to the type σ → Except ε α × σ, the type EStateM ε σ α evaluates to σ → EStateM.Result ε σ α.
EStateM.Result is an inductive type that's very similar to Except, except both constructors have an additional field for the state.
In compiled code, this representation removes one level of indirection from each monadic bind.
EStateM.{u} (ε σ α : Type u) : Type u
EStateM ε σ is a combined error and state monad, equivalent to
ExceptT ε (StateM σ) but more efficient.
EStateM.Result.{u} (ε σ α : Type u) : Type u
Result ε σ α is equivalent to Except ε α × σ, but using a single
combined inductive yields a more efficient data representation.
ok.{u} {ε σ α : Type u}
: α → σ → EStateM.Result ε σ α
A success value of type α, and a new state σ.
error.{u} {ε σ α : Type u}
: ε → σ → EStateM.Result ε σ α
A failure value of type ε, and a new state σ.
EStateM.run.{u} {ε σ α : Type u}
(x : EStateM ε σ α) (s : σ)
: EStateM.Result ε σ α
Execute an EStateM on initial state s to get a Result.
EStateM.run'.{u} {ε σ α : Type u}
(x : EStateM ε σ α) (s : σ) : Option α
Execute an EStateM on initial state s for the returned value α.
If the monadic action throws an exception, returns none instead.
EStateM.adaptExcept.{u} {ε σ α ε' : Type u}
(f : ε → ε') (x : EStateM ε σ α)
: EStateM ε' σ α
Map the exception type of a EStateM ε σ α by a function f : ε → ε'.
Composing StateT and ExceptT in different orders causes exceptions to interact differently with state.
In one ordering, state changes are rolled back when exceptions are caught; in the other, they persist.
The latter option matches the semantics of most imperative programming languages, but the former is very useful for search-based problems.
Often, some but not all state should be rolled back; this can be achieved by “sandwiching” ExceptT between two separate uses of StateT.
To avoid yet another layer of indirection via the use of StateT σ (EStateM ε σ') α, EStateM offers the EStateM.Backtrackable type class.
This class specifies some part of the state that can be saved and restored.
EStateM then arranges for the saving and restoring to take place around error handling.
EStateM.Backtrackable.{u}
(δ : outParam (Type u)) (σ : Type u)
: Type u
Auxiliary instance for saving/restoring the "backtrackable" part of the state.
Here σ is the state, and δ is some subpart of it, and we have a
getter and setter for it (a "lens" in the Haskell terminology).
EStateM.Backtrackable.mk.{u} |
save | : | σ → δ |
| ||
restore | : | σ → δ → σ |
| ||
There is a universally-applicable instance of Backtrackable that neither saves nor restores anything.
Because instance synthesis chooses the most recent instance first, the universal instance is used only if no other instance has been defined.
EStateM.nonBacktrackable.{u} {σ : Type u}
: EStateM.Backtrackable PUnit σ
Dummy default instance. This makes every σ trivially "backtrackable"
by doing nothing on backtrack. Because this is the first declared instance
of Backtrackable _ σ, it will be picked only if there are no other
Backtrackable _ σ instances registered.
These functions are typically not called directly, but rather are accessed through their corresponding type classes.
EStateM.map.{u} {ε σ α β : Type u} (f : α → β)
(x : EStateM ε σ α) : EStateM ε σ β
The map operation of the EStateM monad.
EStateM.pure.{u} {ε σ α : Type u} (a : α)
: EStateM ε σ α
The pure operation of the EStateM monad.
EStateM.bind.{u} {ε σ α β : Type u}
(x : EStateM ε σ α) (f : α → EStateM ε σ β)
: EStateM ε σ β
The bind operation of the EStateM monad.
EStateM.orElse.{u} {ε σ α δ : Type u}
[EStateM.Backtrackable δ σ]
(x₁ : EStateM ε σ α)
(x₂ : Unit → EStateM ε σ α) : EStateM ε σ α
Implementation of orElse for EStateM where the state is Backtrackable.
EStateM.orElse'.{u} {ε σ α δ : Type u} [EStateM.Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx : Bool := true) : EStateM ε σ α
Alternative orElse operator that allows to select which exception should be used.
The default is to use the first exception since the standard orElse uses the second.
EStateM.seqRight.{u} {ε σ α β : Type u}
(x : EStateM ε σ α)
(y : Unit → EStateM ε σ β) : EStateM ε σ β
The seqRight operation of the EStateM monad.
EStateM.tryCatch.{u} {ε σ δ : Type u}
[EStateM.Backtrackable δ σ] {α : Type u}
(x : EStateM ε σ α)
(handle : ε → EStateM ε σ α) : EStateM ε σ α
Implementation of tryCatch for EStateM where the state is Backtrackable.
EStateM.throw.{u} {ε σ α : Type u} (e : ε)
: EStateM ε σ α
The throw operation of the EStateM monad.