@[instance 500]

instance instForInOfForIn' {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_4} {d : Membership α ρ} [ForIn' m ρ α d] :

ForIn m ρ α

A ForIn' instance, which handles for h : x in c do, can also handle for x in x do by ignoring h, and so provides a ForIn instance.

Note that this instance will cause a potentially non-defeq duplication if both ForIn and ForIn' instances are provided for the same type.

Equations

instForInOfForIn' = { forIn := fun {β : Type ?u.10} [Monad m] (x : ρ) (b : β) (f : α → β → m (ForInStep β)) => forIn' x b fun (a : α) (x : a ∈ x) => f a }

source

@[simp]

theorem forIn'_eq_forIn {α : Type u_1} {ρ : Type u_2} {m : Type u_3 → Type u_4} [d : Membership α ρ] [ForIn' m ρ α d] {β : Type u_3} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : α → β → m (ForInStep β)) (h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b) :

forIn' x b f = forIn x b g

source

theorem forIn_eq_forin' {α : Type u_1} {ρ : Type u_2} {m : Type u_3 → Type u_4} [d : Membership α ρ] [ForIn' m ρ α d] {β : Type u_3} [Monad m] (x : ρ) (b : β) (f : α → β → m (ForInStep β)) :

forIn x b f = forIn' x b fun (x_1 : α) (h : x_1 ∈ x) => binderNameHint x_1 f (binderNameHint h () (f x_1))

source

def ForInStep.value {α : Type u_1} (x : ForInStep α) :

Extracts the value from a ForInStep, ignoring whether it is ForInStep.done or ForInStep.yield.

Equations

(ForInStep.done b).value = b
(ForInStep.yield b).value = b

source

@[simp]

theorem ForInStep.value_done {β : Type u_1} (b : β) :

(done b).value = b

source

@[simp]

theorem ForInStep.value_yield {β : Type u_1} (b : β) :

(yield b).value = b

source

@[reducible]

def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} :

f α → (α → β) → f β

Maps a function over a functor, with parameters swapped so that the function comes last.

This function is Functor.map with the parameters reversed, typically used via the <&> operator.

Conventions for notations in identifiers:

The recommended spelling of <&> in identifiers is mapRev.

Equations

a <&> f = f <$> a

source

def «term_<&>_» :

Lean.TrailingParserDescr

Maps a function over a functor, with parameters swapped so that the function comes last.

This function is Functor.map with the parameters reversed, typically used via the <&> operator.

Conventions for notations in identifiers:

The recommended spelling of <&> in identifiers is mapRev.

Equations

«term_<&>_» = Lean.ParserDescr.trailingNode `«term_<&>_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <&> ") (Lean.ParserDescr.cat `term 100))

source

@[inline]

def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) :

f PUnit

Discards the value in a functor, retaining the functor's structure.

Discarding values is especially useful when using Applicative functors or Monads to implement effects, and some operation should be carried out only for its effects. In do-notation, statements whose values are discarded must return Unit, and discard can be used to explicitly discard their values.

Equations

discard x = Functor.mapConst PUnit.unit x

source

class Alternative (f : Type u → Type v) extends Applicative f :

Type (max (u + 1) v)

An Alternative functor is an Applicative functor that can "fail" or be "empty" and a binary operation <|> that “collects values” or finds the “left-most success”.

Important instances include

Option, where failure := none and <|> returns the left-most some.
Parser combinators typically provide an Applicative instance for error-handling and backtracking.

Error recovery and state can interact subtly. For example, the implementation of Alternative for OptionT (StateT σ Id) keeps modifications made to the state while recovering from failure, while StateT σ (OptionT Id) discards them.

map {α β : Type u} : (α → β) → f α → f β
mapConst {α β : Type u} : α → f β → f α
pure {α : Type u} : α → f α
seq {α β : Type u} : f (α → β) → (Unit → f α) → f β
seqLeft {α β : Type u} : f α → (Unit → f β) → f α
seqRight {α β : Type u} : f α → (Unit → f β) → f β
failure {α : Type u} : f α
Produces an empty collection or recoverable failure. The <|> operator collects values or recovers from failures. See Alternative for more details.
orElse {α : Type u} : f α → (Unit → f α) → f α
Depending on the Alternative instance, collects values or recovers from failures by returning the leftmost success. Can be written using the <|> operator syntax.

Instances

source

instance instOrElseOfAlternative (f : Type u → Type v) (α : Type u) [Alternative f] :

OrElse (f α)

Equations

instOrElseOfAlternative f α = { orElse := Alternative.orElse }

source

@[inline]

def guard {f : Type → Type v} [Alternative f] (p : Prop) [Decidable p] :

f Unit

If the proposition p is true, does nothing, else fails (using failure).

Equations

guard p = if p then pure () else failure

source

@[inline]

def optional {f : Type u → Type v} [Alternative f] {α : Type u} (x : f α) :

f (Option α)

Returns some x if f succeeds with value x, else returns none.

Equations

optional x = (some <$> x <|> pure none)

source

class ToBool (α : Type u) :

Type u

toBool : α → Bool

Instances

source

instance instToBoolBool :

ToBool Bool

Equations

instToBoolBool = { toBool := fun (b : Bool) => b }

source

@[macro_inline]

def bool {β : Type u} {α : Type v} [ToBool β] (f t : α) (b : β) :

Equations

bool f t b = match toBool b with | true => t | false => f

source

@[macro_inline]

def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) :

m β

Converts the result of the monadic action x to a Bool. If it is true, returns it and ignores y; otherwise, runs y and returns its result.

This a monadic counterpart to the short-circuiting || operator, usually accessed via the <||> operator.

Conventions for notations in identifiers:

The recommended spelling of <||> in identifiers is orM.

Equations

(x <||> y) = do let b ← x match toBool b with | true => pure b | false => y

source

def «term_<||>_» :

Lean.TrailingParserDescr

Equations

«term_<||>_» = Lean.ParserDescr.trailingNode `«term_<||>_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <||> ") (Lean.ParserDescr.cat `term 30))

source

@[macro_inline]

def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) :

m β

Converts the result of the monadic action x to a Bool. If it is true, returns y; otherwise, returns the original result of x.

This a monadic counterpart to the short-circuiting && operator, usually accessed via the <&&> operator.

Conventions for notations in identifiers:

The recommended spelling of <&&> in identifiers is andM.

Equations

(x <&&> y) = do let b ← x match toBool b with | true => y | false => pure b

source

def «term_<&&>_» :

Lean.TrailingParserDescr

Equations

«term_<&&>_» = Lean.ParserDescr.trailingNode `«term_<&&>_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <&&> ") (Lean.ParserDescr.cat `term 35))

source

@[macro_inline]

def notM {m : Type → Type v} [Applicative m] (x : m Bool) :

m Bool

Runs a monadic action and returns the negation of its result.

Equations

notM x = not <$> x

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 StateT Nat IO 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.run bar s 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 (σ × β) as IO (stM β)
Write StateT.run . s as mapInBase : 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₂.

MonadControl m n 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 MonadControlT MetaM n (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.

source

class MonadControl (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) :

Type (max (max (u + 1) v) w)

A way to lift a computation from one monad to another while providing the lifted computation with a means of interpreting computations from the outer monad. This provides a means of lifting higher-order operations automatically.

Clients should typically use control or controlAt, which request an instance of MonadControlT: the reflexive, transitive closure of MonadControl. New instances should be defined for MonadControl itself.

stM : Type u → Type u
A type that can be used to reconstruct both a returned value and any state used by the outer monad.
liftWith {α : Type u} : (({β : Type u} → n β → m (stM m n β)) → m α) → n α
Lifts an action from the inner monad m to the outer monad n. The inner monad has access to a reverse lifting operator that can run an n action, returning a value and state together.
restoreM {α : Type u} : m (stM m n α) → n α
Lifts a monadic action that returns a state and a value in the inner monad to an action in the outer monad. The extra state information is used to restore the results of effects from the reverse lift passed to liftWith's parameter.

Instances

source

class MonadControlT (m : Type u → Type v) (n : Type u → Type w) :

Type (max (max (u + 1) v) w)

stM : Type u → Type u
A type that can be used to reconstruct both a returned value and any state used by the outer monad.
liftWith {α : Type u} : (({β : Type u} → n β → m (stM m n β)) → m α) → n α
Lifts an action from the inner monad m to the outer monad n. The inner monad has access to a reverse lifting operator that can run an n action, returning a value and state together.
restoreM {α : Type u} : stM m n α → n α
Lifts a monadic action that returns a state and a value in the inner monad to an action in the outer monad. The extra state information is used to restore the results of effects from the reverse lift passed to liftWith's parameter.

Instances

source

@[always_inline]

instance instMonadControlTOfMonadControl (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) (o : Type u_1 → Type u_4) [MonadControl n o] [MonadControlT m n] :

MonadControlT m o

Equations

One or more equations did not get rendered due to their size.

source

instance instMonadControlTOfPure (m : Type u → Type v) [Pure m] :

MonadControlT m m

Equations

One or more equations did not get rendered due to their size.

source

@[inline]

def controlAt (m : Type u → Type v) {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u} (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) :

n α

Lifts an operation from an inner monad to an outer monad, providing it with a reverse lifting operator that allows outer monad computations to be run in the inner monad. The lifted operation is required to return extra information that is required in order to reconstruct the reverse lift's effects in the outer monad; this extra information is determined by stM.

This function takes the inner monad as an explicit parameter. Use control to infer the monad.

Equations

controlAt m f = liftWith f >>= restoreM

source

@[inline]

def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u} (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) :

n α

This function takes the inner monad as an implicit parameter. Use controlAt to specify it explicitly.

Equations

control f = controlAt m f

source

class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂)) :

Type (max (max (max (u + 1) v) w₁) w₂)

Overloaded monadic iteration over some container type.

An instance of ForM m γ α describes how to iterate a monadic operator over a container of type γ with elements of type α in the monad m. The element type should be uniquely determined by the monad and the container.

Use ForM.forIn to construct a ForIn instance from a ForM instance, thus enabling the use of the for operator in do-notation.