7.2. Lifting Monads

When one monad is at least as capable as another, then actions from the latter monad can be used in a context that expects actions from the former. This is called lifting the action from one monad to another. Lean automatically inserts lifts when they are available; lifts are defined in the MonadLift type class. Automatic monad lifting is attempted before the general coercion mechanism.

🔗type class
MonadLift.{u, v, w}
    (m : semiOutParam (Type u → Type v))
    (n : Type u → Type w)
    : Type (max (max (u + 1) v) w)

A function for lifting a computation from an inner Monad to an outer Monad. Like Haskell's MonadTrans, but n does not have to be a monad transformer. Alternatively, an implementation of MonadLayer without layerInvmap (so far).

Instance Constructor

MonadLift.mk.{u, v, w}

Methods

monadLift : {α : Type u} → m α → n α

Lifts a value from monad m into monad n.

Lifting between monads is reflexive and transitive:

  • Any monad can run its own actions.

  • Lifts from m to m' and from m' to n can be composed to yield a lift from m to n. The utility type class MonadLiftT constructs lifts via the reflexive and transitive closure of MonadLift instances. Users should not define new instances of MonadLiftT, but it is useful as an instance implicit parameter to a polymorphic function that needs to run actions from multiple monads in some user-provided monad.

🔗type class
MonadLiftT.{u, v, w} (m : Type u → Type v)
    (n : Type u → Type w)
    : Type (max (max (u + 1) v) w)

The reflexive-transitive closure of MonadLift. monadLift is used to transitively lift monadic computations such as StateT.get or StateT.put s. Corresponds to Haskell's MonadLift.

Instance Constructor

MonadLiftT.mk.{u, v, w}

Methods

monadLift : {α : Type u} → m α → n α

Lifts a value from monad m into monad n.

Monad Lifts in Function Signatures

The function IO.withStdin has the following signature:

IO.withStdin.{u} {m : Type → Type u} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : IO.FS.Stream) (x : m α) : m α

Because it doesn't require its parameter to precisely be in IO, it can be used in many monads, and the body does not need to restrict itself to IO. The instance implicit parameter MonadLiftT BaseIO m allows the reflexive transitive closure of MonadLift to be used to assemble the lift.

When a term of type n β is expected, but the provided term has type m α, and the two types are not definitionally equal, Lean attempts to insert lifts and coercions before reporting an error. There are the following possibilities:

  1. If m and n can be unified to the same monad, then α and β are not the same. In this case, no monad lifts are necessary, but the value in the monad must be coerced. If the appropriate coercion is found, then a call to Lean.Internal.coeM is inserted, which has the following signature:

    Lean.Internal.coeM.{u, v} {m : Type u → Type v} {α β : Type u} [(a : α) → CoeT α a β] [Monad m] (x : m α) : m β

  2. If α and β can be unified, then the monads differ. In this case, a monad lift is necessary to transform an expression with type m α to n α. If m can be lifted to n (that is, there is an instance of MonadLiftT m n) then a call to liftM, which is an alias for MonadLiftT.monadLift, is inserted.

    liftM.{u, v, w} {m : Type u → Type v} {n : Type u → Type w} [self : MonadLiftT m n] {α : Type u} : m α → n α

  3. If neither m and n nor α and β can be unified, but m can be lifted into n and α can be coerced to β, then a lift and a coercion can be combined. This is done by inserting a call to Lean.Internal.liftCoeM:

    Lean.Internal.liftCoeM.{u, v, w} {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [(a : α) → CoeT α a β] [Monad n] (x : m α) : n β

As their names suggest, Lean.Internal.coeM and Lean.Internal.liftCoeM are implementation details, not part of the public API. In the resulting terms, occurrences of Lean.Internal.coeM, Lean.Internal.liftCoeM, and coercions are unfolded.

Lifting IO Monads

There is an instance of MonadLift BaseIO IO, so any BaseIO action can be run in IO as well:

def fromBaseIO (act : BaseIO α) : IO α := act

Behind the scenes, liftM is inserted:

fun {α} act => liftM act : {α : Type} → BaseIO α → EIO IO.Error α#check fun {α} (act : BaseIO α) => (act : IO α) 
fun {α} act => liftM act : {α : Type} → BaseIO α → EIO IO.Error α
Lifting Transformed Monads

There are also instances of MonadLift for most of the standard library's monad transformers, so base monad actions can be used in transformed monads without additional work. For example, state monad actions can be lifted across reader and exception transformers, allowing compatible monads to be intermixed freely:

def declaration uses 'sorry'incrBy (n : Nat) : StateM Nat Unit := modify (def incrOrFail : ReaderT Nat (ExceptT String (StateM Nat)) Unit := do if (← read) > 5 then throw "Too much!" incrBy (← read)

Disabling lifting causes the code to fail to work:

set_option autoLift false def declaration uses 'sorry'incrBy (n : Nat) : StateM Nat Unit := modify (def incrOrFail : ReaderT Nat (ExceptT String (StateM Nat)) Unit := do if (← read) > 5 then throw "Too much!" type mismatch incrBy __do_lift✝ has type StateM Nat Unit : Type but is expected to have type ReaderT Nat (ExceptT String (StateM Nat)) Unit : TypeincrBy (← read)

Automatic lifting can be disabled by setting autoLift to false.

🔗option
autoLift

Default value: true

insert monadic lifts (i.e., liftM and coercions) when needed

7.2.1. Reversing Lifts

Monad lifting is not always sufficient to combine monads. Many operations provided by monads are higher order, taking an action in the same monad as a parameter. Even if these operations are lifted to some more powerful monad, their arguments are still restricted to the original monad.

There are two type classes that support this kind of “reverse lifting”: MonadFunctor and MonadControl. An instance of MonadFunctor m n explains how to interpret a fully-polymorphic function in m into n. This polymorphic function must work for all types α: it has type {α : Type u} → m α → m α. Such a function can be thought of as one that may have effects, but can't do so based on specific values that are provided. An instance of MonadControl m n explains how to interpret an arbitrary action from m into n, while at the same time providing a “reverse interpreter” that allows the m action to run n actions.

7.2.1.1. Monad Functors

🔗type class
MonadFunctor.{u, v, w}
    (m : semiOutParam (Type u → Type v))
    (n : Type u → Type w)
    : Type (max (max (u + 1) v) w)

A functor in the category of monads. Can be used to lift monad-transforming functions. Based on MFunctor from the pipes Haskell package, but not restricted to monad transformers. Alternatively, an implementation of MonadTransFunctor.

Instance Constructor

MonadFunctor.mk.{u, v, w}

Methods

monadMap : {α : Type u} → ({β : Type u} → m β → m β) → n α → n α

Lifts a monad morphism f : {β : Type u} → m β → m β to monadMap f : {α : Type u} → n α → n α.

🔗type class
MonadFunctorT.{u, v, w} (m : Type u → Type v)
    (n : Type u → Type w)
    : Type (max (max (u + 1) v) w)

The reflexive-transitive closure of MonadFunctor. monadMap is used to transitively lift Monad morphisms.

Instance Constructor

MonadFunctorT.mk.{u, v, w}

Methods

monadMap : {α : Type u} → ({β : Type u} → m β → m β) → n α → n α

Lifts a monad morphism f : {β : Type u} → m β → m β to monadMap f : {α : Type u} → n α → n α.

7.2.1.2. Reversible Lifting with MonadControl

🔗type class
MonadControl.{u, v, w}
    (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.

Instance Constructor

MonadControl.mk.{u, v, w}

Methods

stM : Type u → Type u
liftWith : {α : Type u} → (({β : Type u} → n β → m (MonadControl.stM m n β)) → m α) → n α
restoreM : {α : Type u} → m (MonadControl.stM m n α) → n α
🔗type class
MonadControlT.{u, v, w} (m : Type u → Type v)
    (n : Type u → Type w)
    : Type (max (max (u + 1) v) w)

Transitive closure of MonadControl.

Instance Constructor

MonadControlT.mk.{u, v, w}

Methods

stM : Type u → Type u
liftWith : {α : Type u} → (({β : Type u} → n β → m (stM m n β)) → m α) → n α
restoreM : {α : Type u} → stM m n α → n α
🔗def
control.{u, v, w} {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 α
🔗def
controlAt.{u, v, w} (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 α
Exceptions and Lifting

One example is Except.tryCatch:

Except.tryCatch.{u, v} {ε : Type u} {α : Type v} (ma : Except ε α) (handle : ε → Except ε α) : Except ε α

Both of its parameters are in Except ε. MonadLift can lift the entire application of the handler. The function getBytes, which extracts the single bytes from an array of Nats using state and exceptions, is written without Lean.Parser.Term.do : termdo-notation or automatic lifting in order to make its structure explicit.

set_option autoLift false def getByte (n : Nat) : Except String UInt8 := if n < 256 then pure n.toUInt8 else throw s!"Out of range: {n}" def getBytes (input : Array Nat) : StateT (Array UInt8) (Except String) Unit := do input.forM fun i => liftM (Except.tryCatch (some <$> getByte i) fun _ => pure none) >>= fun | some b => modify (·.push b) | none => pure () Except.ok #[1, 58, 255, 2]#eval getBytes #[1, 58, 255, 300, 2, 1000000] |>.run #[] |>.map (·.2) 
Except.ok #[1, 58, 255, 2]

getBytes uses an Option returned from the lifted action to signal the desired state updates. This quickly becomes unwieldy if there are more possible ways to react to the inner action, such as saving handled exceptions. Ideally, state updates would be performed within the tryCatch call directly.

Attempting to save bytes and handled exceptions does not work, however, because the arguments to Except.tryCatch have type Except String Unit:

def getBytes' (input : Array Nat) : StateT (Array String) (StateT (Array UInt8) (Except String)) Unit := do input.forM fun i => liftM (Except.tryCatch (getByte i >>= fun b => failed to synthesize MonadStateOf (Array UInt8) (Except String) Additional diagnostic information may be available using the `set_option diagnostics true` command.modifyThe (Array UInt8) (·.push b)) fun e => failed to synthesize MonadStateOf (Array String) (Except String) Additional diagnostic information may be available using the `set_option diagnostics true` command.modifyThe (Array String) (·.push e)) 
failed to synthesize
  MonadStateOf (Array String) (Except String)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

Because StateT has a MonadControl instance, control can be used instead of liftM. It provides the inner action with an interpreter for the outer monad. In the case of StateT, this interpreter expects that the inner monad returns a tuple that includes the updated state, and takes care of providing the initial state and extracting the updated state from the tuple.

def getBytes' (input : Array Nat) : StateT (Array String) (StateT (Array UInt8) (Except String)) Unit := do input.forM fun i => control fun run => (Except.tryCatch (getByte i >>= fun b => run (modifyThe (Array UInt8) (·.push b)))) fun e => run (modifyThe (Array String) (·.push e)) Except.ok (#["Out of range: 300", "Out of range: 1000000"], #[1, 58, 255, 2])#eval getBytes' #[1, 58, 255, 300, 2, 1000000] |>.run #[] |>.run #[] |>.map (fun (((), bytes), errs) => (bytes, errs)) 
Except.ok (#["Out of range: 300", "Out of range: 1000000"], #[1, 58, 255, 2])