Equations
- «term_<&>_» = Lean.ParserDescr.trailingNode `«term_<&>_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <&> ") (Lean.ParserDescr.cat `term 100))
Equations
- failure : {α : Type u} → f α
- orElse : {α : Type u} → f α → (Unit → f α) → f α
Equations
- instOrElse f α = { orElse := Alternative.orElse }
Equations
- optional x = HOrElse.hOrElse (some <$> x) fun x => pure none
- toBool : α → Bool
Instances
Equations
- «term_<||>_» = Lean.ParserDescr.trailingNode `«term_<||>_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <||> ") (Lean.ParserDescr.cat `term 30))
Equations
- «term_<&&>_» = Lean.ParserDescr.trailingNode `«term_<&&>_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <&&> ") (Lean.ParserDescr.cat `term 35))
How MonadControl
works #
There is a tutorial by Alexis King that this docstring is based on.
Suppose we have foo:∀α,IOα→IOα
and bar:StateTσIOβ
(ie, bar:σ→IO(σ×β)
).
We might want to 'map' bar
by foo
. Concretely we would write this as:
opaque foo : ∀ {α}, IO α → IO α
opaque bar : StateT σ IO β
def mapped_foo : StateT σ IO β := do
let s ← get
let (b, s') ← liftM <| foo <| StateT.run bar s
set s'
return b
This is fine but it's not going to generalise, what if we replace StateTNatIO
with a large tower of monad transformers?
We would have to rewrite the above to handle each of the run
functions for each transformer in the stack.
Is there a way to generalise run
as a kind of inverse of lift
?
We have lift:mα→StateTσmα
for all m
, but we also need to 'unlift' the state.
But unlift:StateTσIOα→IOα
can't be implemented. So we need something else.
If we look at the definition of mapped_foo
, we see that lift<|foo<|StateT.runbars
has the type IO(σ×β)
. The key idea is that σ×β
contains all of the information needed to reconstruct the state and the new value.
Now lets define some values to generalise mapped_foo
:
- Write
IO(σ×β)
asIO(stMβ)
- Write
StateT.run.s
asmapInBase:StateTσIOα→IO(stMβ)
- Define
restoreM:IO(stMα)→StateTσIOα
as below
def stM (α : Type) := α × σ
def restoreM (x : IO (stM α)) : StateT σ IO α := do
let (a,s) ← liftM x
set s
return a
To get:
def mapped_foo' : StateT σ IO β := do
let s ← get
let mapInBase := fun z => StateT.run z s
restoreM <| foo <| mapInBase bar
and finally define
def control {α : Type}
(f : ({β : Type} → StateT σ IO β → IO (stM β)) → IO (stM α))
: StateT σ IO α := do
let s ← get
let mapInBase := fun {β} (z : StateT σ IO β) => StateT.run z s
let r : IO (stM α) := f mapInBase
restoreM r
Now we can write mapped_foo
as:
def mapped_foo'' : StateT σ IO β :=
control (fun mapInBase => foo (mapInBase bar))
The core idea of mapInBase
is that given any β
, it runs an instance of
StateTσIOβ
and 'packages' the result and state as IO(stMβ)
so that it can be piped through foo
.
Once it's been through foo
we can then unpack the state again with restoreM
.
Hence we can apply foo
to bar
without losing track of the state.
Here stMβ=σ×β
is the 'packaged result state', but we can generalise:
if we have a tower StateTσ₁<|StateTσ₂<|IO
, then the
composite packaged state is going to be stM₁₂β:=σ₁×σ₂×β
or stM₁₂:=stM₁∘stM₂
.
MonadControlmn
means that when programming in the monad n
,
we can switch to a base monad m
using control
, just like with liftM
.
In contrast to liftM
, however, we also get a function runInBase
that
allows us to "lower" actions in n
into m
.
This is really useful when we have large towers of monad transformers, as we do in the metaprogramming library.
For example there is a function withNewMCtxDepthImp:MetaMα→MetaMα
that runs the input monad instance
in a new nested metavariable context. We can lift this to withNewMctxDepth:nα→nα
using MonadControlTMetaMn
(MonadControlT
is the transitive closure of MonadControl
).
Which means that we can also run withNewMctxDepth
in the Tactic
monad without needing to
faff around with lifts and all the other boilerplate needed in mapped_foo
.
Relationship to MonadFunctor
#
A stricter form of MonadControl
is MonadFunctor
, which defines
monadMap{α}:(∀{β},mβ→mβ)→nα→nα
. Using monadMap
it is also possible to define mapped_foo
above.
However there are some mappings which can't be derived using MonadFunctor
. For example:
@[inline] def map1MetaM [MonadControlT MetaM n] [Monad n] (f : forall {α}, (β → MetaM α) → MetaM α) {α} (k : β → n α) : n α :=
control fun runInBase => f fun b => runInBase <| k b
@[inline] def map2MetaM [MonadControlT MetaM n] [Monad n] (f : forall {α}, (β → γ → MetaM α) → MetaM α) {α} (k : β → γ → n α) : n α :=
control fun runInBase => f fun b c => runInBase <| k b c
In monadMap
, we can only 'run in base' a single computation in n
into the base monad m
.
Using control
means that runInBase
can be used multiple times.
- stM : Type u → Type u
- liftWith : {α : Type u} → (({β : Type u} → n β → m (stM β)) → m α) → n α
- restoreM : {α : Type u} → m (stM α) → n α
MonadControl is a way of stating that the monad m
can be 'run inside' the monad n
.
This is the same as MonadBaseControl
in Haskell.
To learn about MonadControl
, see the comment above this docstring.
- stM : Type u → Type u
- liftWith : {α : Type u} → (({β : Type u} → n β → m (stM β)) → m α) → n α
- restoreM : {α : Type u} → stM α → n α
Transitive closure of MonadControl.
Instances
Equations
- instMonadControlT m n o = { stM := fun α => stM m n (MonadControl.stM n o α), liftWith := fun {α} f => MonadControl.liftWith fun x₂ => liftWith fun x₁ => f fun {β} => x₁ (MonadControl.stM n o β) ∘ x₂ β, restoreM := fun {α} => MonadControl.restoreM ∘ restoreM }
Equations
- instMonadControlT_1 m = { stM := fun α => α, liftWith := fun {α} f => f fun {β} x => x, restoreM := fun {α} x => pure x }