Documentation

Init.Control.Basic

def Functor.mapRev {f : Type uType v} [inst : Functor f] {α : Type u} {β : Type u} :
f α(αβ) → f β
Equations
@[inline]
def Functor.discard {f : Type uType v} {α : Type u} [inst : Functor f] (x : f α) :
Equations
class Alternative (f : Type uType v) extends Applicative :
Type (max (u + 1) v)
  • failure : {α : Type u} → f α
  • orElse : {α : Type u} → f α(Unitf α) → f α
Instances
instance instOrElse (f : Type uType v) (α : Type u) [inst : Alternative f] :
OrElse (f α)
Equations
@[inline]
def guard {f : TypeType v} [inst : Alternative f] (p : Prop) [inst : Decidable p] :
Equations
@[inline]
def optional {f : Type uType v} [inst : Alternative f] {α : Type u} (x : f α) :
f (Option α)
Equations
class ToBool (α : Type u) :
Type u
  • toBool : αBool
Instances
Equations
@[macroInline]
def bool {β : Type u} {α : Type v} [inst : ToBool β] (f : α) (t : α) (b : β) :
α
Equations
@[macroInline]
def orM {m : Type uType v} {β : Type u} [inst : Monad m] [inst : ToBool β] (x : m β) (y : m β) :
m β
Equations
@[macroInline]
def andM {m : Type uType v} {β : Type u} [inst : Monad m] [inst : ToBool β] (x : m β) (y : m β) :
m β
Equations
@[macroInline]
def notM {m : TypeType v} [inst : Applicative m] (x : m Bool) :
Equations

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:

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.

class MonadControl (m : Type uType v) (n : Type uType w) :
Type (max (max (u + 1) v) w)
  • stM : Type uType 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.

Instances
class MonadControlT (m : Type uType v) (n : Type uType w) :
Type (max (max (u + 1) v) w)
  • stM : Type uType u
  • liftWith : {α : Type u} → (({β : Type u} → n βm (stM β)) → m α) → n α
  • restoreM : {α : Type u} → stM αn α

Transitive closure of MonadControl.

Instances
instance instMonadControlT (m : Type u_1Type u_2) (n : Type u_1Type u_3) (o : Type u_1Type u_4) [inst : MonadControl n o] [inst : MonadControlT m n] :
Equations
instance instMonadControlT_1 (m : Type uType v) [inst : Pure m] :
Equations
  • instMonadControlT_1 m = { stM := fun α => α, liftWith := fun {α} f => f fun {β} x => x, restoreM := fun {α} x => pure x }
@[inline]
def controlAt (m : Type uType v) {n : Type uType w} [inst : MonadControlT m n] [inst : Bind n] {α : Type u} (f : ({β : Type u} → n βm (stM m n β)) → m (stM m n α)) :
n α
Equations
@[inline]
def control {m : Type uType v} {n : Type uType w} [inst : MonadControlT m n] [inst : Bind n] {α : Type u} (f : ({β : Type u} → n βm (stM m n β)) → m (stM m n α)) :
n α
Equations
class ForM (m : Type uType v) (γ : Type w₁) (α : outParam (Type w₂)) :
Type (max (max (max (u + 1) v) w₁) w₂)
Instances