    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The state monad transformer
    ------------------------------------------------------------------------

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

    module Effect.Monad.State.Transformer where

    open import Algebra using (RawMonoid)
    open import Data.Product.Base using (_×_; _,_; map₂; proj₁; proj₂)
    open import Data.Unit.Polymorphic.Base using (tt)
    open import Effect.Choice using (RawChoice)
    open import Effect.Empty using (RawEmpty)
    open import Effect.Functor using (RawFunctor)
    open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
    open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus; RawMonadT; RawMonadTd)
    open import Function.Base using (_∘′_; _$_; const)
    open import Level using (Level; _⊔_)

    private
      variable
        f s : Level
        A B : Set s
        S S₁ S₂ : Set s
        M : Set s → Set f

    ------------------------------------------------------------------------
    -- Re-export the basic type and definitions

    open import Effect.Monad.State.Transformer.Base public
      using ( RawMonadState
            ; StateT
            ; mkStateT
            ; runStateT
            ; evalStateT
            ; execStateT
            )

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

    functor : RawFunctor M → RawFunctor (StateT S M)
    functor M = record
      { _<$>_ = λ f ma → mkStateT (λ s → map₂ f <$> StateT.runStateT ma s)
      } where open RawFunctor M

    applicative : RawMonad M → RawApplicative (StateT S M)
    applicative M = record
      { rawFunctor = functor rawFunctor
      ; pure = λ a → mkStateT (pure ∘′ (_, a))
      ; _<*>_ = λ mf mx → mkStateT $ λ s →
                  do (s , f) ← StateT.runStateT mf s
                     (s , x) ← StateT.runStateT mx s
                     pure (s , f x)
      } where open RawMonad M

    empty : RawEmpty M → RawEmpty (StateT S M)
    empty M = record
      { empty = mkStateT (const (RawEmpty.empty M))
      }

    choice : RawChoice M → RawChoice (StateT S M)
    choice M = record
      { _<|>_ = λ ma₁ ma₂ → mkStateT $ λ s →
                StateT.runStateT ma₁ s
                <|> StateT.runStateT ma₂ s
      } where open RawChoice M

    applicativeZero : RawMonadZero M → RawApplicativeZero (StateT S M)
    applicativeZero M = record
      { rawApplicative = applicative (RawMonadZero.rawMonad M)
      ; rawEmpty = empty (RawMonadZero.rawEmpty M)
      }

    alternative : RawMonadPlus M → RawAlternative (StateT S M)
    alternative M = record
      { rawApplicativeZero = applicativeZero rawMonadZero
      ; rawChoice = choice rawChoice
      } where open RawMonadPlus M

    monad : RawMonad M → RawMonad (StateT S M)
    monad M = record
      { rawApplicative = applicative M
      ; _>>=_ = λ ma f → mkStateT $ λ s →
                  do (s , a) ← StateT.runStateT ma s
                     StateT.runStateT (f a) s
      } where open RawMonad M

    monadZero : RawMonadZero M → RawMonadZero (StateT S M)
    monadZero M = record
      { rawMonad = monad (RawMonadZero.rawMonad M)
      ; rawEmpty = empty (RawMonadZero.rawEmpty M)
      }

    monadPlus : RawMonadPlus M → RawMonadPlus (StateT S M)
    monadPlus M = record
      { rawMonadZero = monadZero rawMonadZero
      ; rawChoice = choice rawChoice
      } where open RawMonadPlus M

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

    monadT : RawMonadT {f = s} {g₁ = f} {g₂ = s ⊔ f} (StateT S)
    monadT M = record
      { lift = λ ma → mkStateT (λ s → (s ,_) <$> ma)
      ; rawMonad = monad M
      } where open RawMonad M

    monadState : RawMonad M → RawMonadState S (StateT S M)
    monadState M = record
      { gets   = λ f → mkStateT (λ s → pure (s , f s))
      ; modify = λ f → mkStateT (λ s → pure (f s , _))
      } where open RawMonad M

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

    liftStateT : RawMonad M →
                 RawMonadState S₁ M →
                 RawMonadState S₁ (StateT S₂ M)
    liftStateT M Mon = record
      { gets   = λ f₁ → lift (gets f₁)
      ; modify = λ f₁ → lift (modify f₁)
      } where open RawMonadTd (monadT M) using (lift); open RawMonadState Mon

    open import Effect.Monad.Reader.Transformer.Base

    liftReaderT : RawMonadState S₁ M →
                  RawMonadState S₁ (ReaderT S₂ M)
    liftReaderT Mon = record
      { gets   = λ f → mkReaderT (const (gets f))
      ; modify = λ f → mkReaderT (const (modify f))
      } where open RawMonadState Mon

    open import Effect.Monad.Writer.Transformer.Base

    liftWriterT : (MS : RawMonoid s f) →
                  RawFunctor M →
                  RawMonadState S M →
                  RawMonadState S (WriterT MS M)
    liftWriterT MS M Mon = record
      { gets   = λ f → mkWriterT λ w → (gets ((w ,_) ∘′ f))
      ; modify = λ f → mkWriterT λ w → (const (w , tt) <$> modify f)
      } where open RawMonadState Mon
              open RawFunctor M