Documentation

Init.Control.Basic

@[reducible]
def Functor.mapRev {f : Type u → Type v} [Functor f] {α : Type u} {β : Type u} :
f α(αβ)f β
Equations
Instances For
    @[inline]
    def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) :
    Equations
    Instances For
      class Alternative (f : Type u → Type v) extends Applicative :
      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 (αβ)(Unitf α)f β
      • seqLeft : {α β : Type u} → f α(Unitf β)f α
      • seqRight : {α β : Type u} → f α(Unitf β)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 α(Unitf α)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
        instance instOrElseOfAlternative (f : Type u → Type v) (α : Type u) [Alternative f] :
        OrElse (f α)
        Equations
        @[inline]
        def guard {f : TypeType v} [Alternative f] (p : Prop) [Decidable p] :

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

        Equations
        Instances For
          @[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
          Instances For
            class ToBool (α : Type u) :
            • toBool : αBool
            Instances
              Equations
              @[macro_inline]
              def bool {β : Type u} {α : Type v} [ToBool β] (f : α) (t : α) (b : β) :
              α
              Equations
              Instances For
                @[macro_inline]
                def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x : m β) (y : m β) :
                m β
                Equations
                Instances For
                  @[macro_inline]
                  def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x : m β) (y : m β) :
                  m β
                  Equations
                  Instances For
                    @[macro_inline]
                    def notM {m : TypeType v} [Applicative m] (x : m Bool) :
                    Equations
                    Instances For

                      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:

                      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.

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

                      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 u → Type v) (n : Type u → Type w) :
                        Type (max (max (u + 1) v) w)

                        Transitive closure of MonadControl.

                        • stM : Type u → Type u
                        • liftWith : {α : Type u} → (({β : Type u} → n βm (stM m n β))m α)n α
                        • restoreM : {α : Type u} → stM m n αn α
                        Instances
                          @[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] :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          instance instMonadControlTOfPure (m : Type u → Type v) [Pure m] :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          @[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 α
                          Equations
                          Instances For
                            @[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 α
                            Equations
                            Instances For
                              class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂)) :
                              Type (max (max (max (u + 1) v) w₁) w₂)

                              Typeclass for the polymorphic forM operation described in the "do unchained" paper. Remark:

                              • γ is a "container" type of elements of type α.
                              • α is treated as an output parameter by the typeclass resolution procedure. That is, it tries to find an instance using only m and γ.
                              Instances
                                @[always_inline]
                                def Bind.kleisliRight {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} {γ : Type u_1} [Bind m] (f₁ : αm β) (f₂ : βm γ) (a : α) :
                                m γ

                                Left-to-right composition of Kleisli arrows.

                                Equations
                                • (f₁ >=> f₂) a = f₁ a >>= f₂
                                Instances For
                                  @[always_inline]
                                  def Bind.kleisliLeft {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} {γ : Type u_1} [Bind m] (f₂ : βm γ) (f₁ : αm β) (a : α) :
                                  m γ

                                  Right-to-left composition of Kleisli arrows.

                                  Equations
                                  • (f₂ <=< f₁) a = f₁ a >>= f₂
                                  Instances For
                                    @[always_inline]
                                    def Bind.bindLeft {α : Type u} {m : Type u → Type u_1} {β : Type u} [Bind m] (f : αm β) (ma : m α) :
                                    m β

                                    Same as Bind.bind but with arguments swapped.

                                    Equations
                                    Instances For

                                      Left-to-right composition of Kleisli arrows.

                                      Equations
                                      Instances For

                                        Right-to-left composition of Kleisli arrows.

                                        Equations
                                        Instances For

                                          Same as Bind.bind but with arguments swapped.

                                          Equations
                                          Instances For