class Control.Monad.IO.MonadUnliftIO (m : Type → Type) [Monad m] [MonadLiftT IO m] : Type 1

Typeclass for monads that can "unlift" back to IO.

$$\text{withRunInIO} : ((\forall \alpha.\; m\;\alpha \to \text{IO}\;\alpha) \to \text{IO}\;\beta) \to m\;\beta$$

This enables running callbacks that require plain IO from within a monadic context m. The CPS form avoids universe issues with returning the polymorphic run function directly.

• withRunInIO {β : Type} : (((α : Type) → m α → IO α) → IO β) → m β

  Provide a function to run m actions in IO.

@[inline]

def Control.Monad.IO.MonadUnliftIO.toIO {m : Type → Type} {α : Type} [Monad m] [MonadLiftT IO m] [MonadUnliftIO m] (act : m α) : m (IO α)

Convenience: run a single m action in IO. $$\text{toIO}(act) : m\;(\text{IO}\;\alpha)$$

Equations

• Control.Monad.IO.MonadUnliftIO.toIO act = Control.Monad.IO.MonadUnliftIO.withRunInIO fun (run : (α : Type) → m α → IO α) => pure (run α act)

@[inline]

def Control.Monad.IO.MonadUnliftIO.liftIOOp {m : Type → Type} {α β : Type} [Monad m] [MonadLiftT IO m] [MonadUnliftIO m] (f : (IO α → IO α) → IO β) (act : m α) : m β

Lift an IO-expecting callback into m by providing the unlift. $$\text{liftIOOp} : ((\text{IO}\;\alpha \to \text{IO}\;\alpha) \to \text{IO}\;\beta) \to m\;\alpha \to m\;\beta$$

Equations

• Control.Monad.IO.MonadUnliftIO.liftIOOp f act = Control.Monad.IO.MonadUnliftIO.withRunInIO fun (run : (α : Type) → m α → IO α) => f fun (x : IO α) => run α act

@[implicit_reducible]

instance Control.Monad.IO.instMonadUnliftIOIO : MonadUnliftIO IO

IO trivially unlifts to itself: the run function is id.

Equations

• Control.Monad.IO.instMonadUnliftIOIO = { withRunInIO := fun {β : Type} (f : ((α : Type) → IO α → IO α) → IO β) => f fun (x : Type) (x_1 : IO x) => x_1 }

@[implicit_reducible]

instance Control.Monad.IO.instMonadUnliftIOReaderTIO {r : Type} : MonadUnliftIO (ReaderT r IO)

ReaderT r IO can unlift by capturing the environment.

Equations

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