------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of IO
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --guardedness #-}

module IO.Effectful where

open import Level using (Level; _⊔_)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad)

open import IO.Base

private
  variable
    f : Level

------------------------------------------------------------------------
-- Structure

functor : RawFunctor {f} IO
functor = record { _<$>_ = _<$>_ }

applicative : RawApplicative {f} IO
applicative = record
  { rawFunctor = functor
  ; pure = pure
  ; _<*>_ = _<*>_
  }

monad : RawMonad {f} IO
monad = record
  { rawApplicative = applicative
  ; _>>=_ = _>>=_
  }