    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Basic definition and functions on the state monad transformer
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Effect.Monad.State.Transformer.Base where

    open import Data.Product.Base using (_×_; proj₁; proj₂)
    open import Data.Unit.Polymorphic.Base using (⊤)
    open import Effect.Functor using (RawFunctor)
    open import Function.Base using (_∘′_; const; id)
    open import Level using (Level; suc; _⊔_)

    private
      variable
        f s : Level
        A : Set s
        S : Set s
        M : Set s → Set f

    ------------------------------------------------------------------------
    -- State monad operations

    record RawMonadState
           (S : Set s)
           (M : Set s → Set f)
           : Set (suc s ⊔ f) where
      field
        gets   : (S → A) → M A
        modify : (S → S) → M ⊤

      put = modify ∘′ const
      get = gets id

    ------------------------------------------------------------------------
    -- State monad transformer

    record StateT
           (S : Set s)
           (M : Set s → Set f)
           (A : Set s)
           : Set (s ⊔ f) where
      constructor mkStateT
      field runStateT : S → M (S × A)
    open StateT public

    evalStateT : RawFunctor M → StateT S M A → S → M A
    evalStateT M ma s = let open RawFunctor M in proj₂ <$> runStateT ma s

    execStateT : RawFunctor M → StateT S M A → S → M S
    execStateT M ma s = let open RawFunctor M in proj₁ <$> runStateT ma s