module FP.Prelude.Monads where

import FP.Prelude.Core
import FP.Prelude.Effects
import FP.Prelude.Constraints
import FP.Prelude.Morphism
import FP.Prelude.Lattice

-- E and I effects can be implemented by combining unit, discard and commute
-- All effects are implemented this way except for continuation effects
class FunctorUnit (t ∷ (★ → ★) → (★ → ★)) where funit ∷ (Functor m) ⇒ m ↝ t m
class FunctorDiscard (t ∷ (★ → ★) → (★ → ★)) where fdiscard ∷ (Functor m) ⇒ t (t m) ↝ t m

-- For commuting effects
class FunctorFunctor (t ∷ (★ → ★) → (★ → ★)) where fmap ∷ m ↝ n → t m ↝ t n
class FunctorIsoFunctor (t ∷ (★ → ★) → (★ → ★)) where fisomap ∷ (m ↝ n,n ↝ m) → (t m ↝ t n)

-- # ID

newtype ID a = ID { runID ∷ a }
  deriving
  ( Eq,Ord
  , POrd,Bot,Join,Meet,Top,JoinLattice,Monoid,Difference
  )

isoID ∷ ID a ⇄ a
isoID = Iso runID ID

instance Functor ID where 
  map ∷ (a → b) → ID a → ID b
  map f = ID ∘ f ∘ runID
instance FunctorM ID where 
  mapM ∷ (Monad m) ⇒ (a → m b) → ID a → m (ID b)
  mapM f = map ID ∘ f ∘ runID
instance Monad ID where 
  return ∷ a → ID a
  return = ID
  (≫=) ∷ ID a → (a → ID b) → ID b
  aM ≫= k = k $ runID aM

instance Functorial POrd ID where functorial = W
instance OrdFunctorial POrd ID where ordFunctorial = W
instance Functorial Bot ID where functorial = W
instance Functorial Join ID where functorial = W
instance Functorial Meet ID where functorial = W
instance Functorial Top ID where functorial = W
instance Functorial JoinLattice ID where functorial = W
instance Functorial Monoid ID where functorial = W

-- # Failure

-- Base Effect

type Failure = FailureT ID

failure ∷ Maybe a → Failure a
failure = abortMaybe

runFailure ∷ Failure a → Maybe a
runFailure = runID ∘ runFailureT

-- Commuting with self

commuteFailure ∷ (Functor m) ⇒ FailureT (FailureT m) ↝ FailureT (FailureT m)
commuteFailure aMM = FailureT $ FailureT $ ff ^$ runFailureT $ runFailureT aMM
  where
    ff ∷ Maybe (Maybe a) → Maybe (Maybe a)
    ff Nothing = Just Nothing
    ff (Just Nothing) = Nothing
    ff (Just (Just a)) = Just (Just a)
  
-- Functor and Monad

instance (Functor m) ⇒ Functor (FailureT m) where
  map ∷ (a → b) → FailureT m a → FailureT m b
  map f = FailureT ∘ map (map f) ∘ runFailureT
instance (Monad m) ⇒ Monad (FailureT m) where
  return ∷ a → FailureT m a
  return = FailureT ∘ return ∘ Just
  (≫=) ∷ FailureT m a → (a → FailureT m b) → FailureT m b
  aM ≫= k = FailureT $ do
    aM' ← runFailureT aM
    case aM' of
      Nothing → return Nothing
      Just a → runFailureT $ k a

-- Higher Functor

instance FunctorUnit FailureT where 
  funit ∷ (Functor m) ⇒ m ↝ FailureT m
  funit = FailureT ∘ map Just
instance FunctorDiscard FailureT where
  fdiscard ∷ (Functor m) ⇒ FailureT (FailureT m) ↝ FailureT m
  fdiscard = FailureT ∘ ff ^∘ runFailureT ∘ runFailureT
    where
      ff ∷ Maybe (Maybe a) → Maybe a
      ff Nothing = Nothing
      ff (Just aM) = aM
instance FunctorFunctor FailureT where
  fmap ∷ (m ↝ n) → FailureT m ↝ FailureT n
  fmap f = FailureT ∘ f ∘ runFailureT

-- MonadMonoid and MonadJoin

instance (MonadMonoid m) ⇒ MonadMonoid (FailureT m) where
  mnull ∷ FailureT m a
  mnull = FailureT mnull
  (<⧺>) ∷ FailureT m a → FailureT m a → FailureT m a
  aM₁ <⧺> aM₂ = FailureT $ runFailureT aM₁ <⧺> runFailureT aM₂
instance (MonadBot m) ⇒ MonadBot (FailureT m) where
  mbot ∷ FailureT m a
  mbot = FailureT mbot
instance (MonadJoin m) ⇒ MonadJoin (FailureT m) where
  (<⊔>) ∷ FailureT m a → FailureT m a → FailureT m a
  aM₁ <⊔> aM₂ = FailureT $ runFailureT aM₁ <⊔> runFailureT aM₂
instance (MonadJoinLattice m) ⇒ MonadJoinLattice (FailureT m)

-- Failure Effect

instance (Functor m) ⇒ MonadFailure (FailureT m) where
  failureE ∷ FailureT (FailureT m) ↝ FailureT m
  failureE = fdiscard ∘ commuteFailure
  failureI ∷ FailureT m ↝ FailureT (FailureT m)
  failureI = commuteFailure ∘ funit

-- Maybe Failure Effect

instance MonadFailure Maybe where
  failureE ∷ FailureT Maybe ↝ Maybe
  failureE = runFailure ∘ failureE ∘ fmap failure
  failureI ∷ Maybe ↝ FailureT Maybe
  failureI = fmap runFailure ∘ failureI ∘ failure

-- # Error

-- Base Effect

type Error e = ErrorT e ID

runError ∷ Error e a → e ⨄ a
runError = runID ∘ runErrorT

-- Commuting with self

errorCommute ∷ (Functor m) ⇒ ErrorT e (ErrorT e m) ↝ ErrorT e (ErrorT e m)
errorCommute = ErrorT ∘ ErrorT ∘ ff ^∘ runErrorT ∘ runErrorT
  where
    ff ∷ e ⨄ (e ⨄ a) → e ⨄ (e ⨄ a)
    ff (Left e) = Right (Left e)
    ff (Right (Left e)) = Left e
    ff (Right (Right a)) = Right $ Right a

-- Functor and Monad

instance (Functor m) ⇒ Functor (ErrorT e m) where
  map ∷ (a → b) → ErrorT e m a → ErrorT e m b
  map f aM = ErrorT $ mapRight f ^$ runErrorT aM
instance (Monad m) ⇒ Monad (ErrorT e m) where
  return ∷ a → ErrorT e m a
  return = ErrorT ∘ return ∘ Right
  (≫=) ∷ ErrorT e m a → (a → ErrorT e m b) → ErrorT e m b
  aM ≫= k = ErrorT $ do
    aeM ← runErrorT aM
    case aeM of
      Left e → return $ Left e
      Right a → runErrorT $ k a

-- Higher Functor

instance FunctorUnit (ErrorT e) where
  funit ∷ (Functor m) ⇒ m ↝ ErrorT e m
  funit aM = ErrorT $ Right ^$ aM
instance FunctorDiscard (ErrorT e) where
  fdiscard ∷ (Functor m) ⇒ ErrorT e (ErrorT e m) ↝ ErrorT e m
  fdiscard = ErrorT ∘ ff ^∘ runErrorT ∘ runErrorT
    where
      ff (Left e) = Left e
      ff (Right ea) = ea
instance FunctorFunctor (ErrorT e) where
  fmap ∷ m ↝ n → ErrorT e m ↝ ErrorT e n
  fmap f = ErrorT ∘ f ∘ runErrorT

-- MonadMonoid and MonadJoin

instance (MonadMonoid m) ⇒ MonadMonoid (ErrorT e m) where
  mnull ∷ ErrorT e m a
  mnull = ErrorT mnull
  (<⧺>) ∷ ErrorT e m a → ErrorT e m a → ErrorT e m a
  aM₁ <⧺> aM₂ = ErrorT $ runErrorT aM₁ <⧺> runErrorT aM₂
instance (MonadBot m) ⇒ MonadBot (ErrorT e m) where
  mbot ∷ ErrorT e m a
  mbot = ErrorT mbot
instance (MonadJoin m) ⇒ MonadJoin (ErrorT e m) where
  (<⊔>) ∷ ErrorT e m a → ErrorT e m a → ErrorT e m a
  aM₁ <⊔> aM₂ = ErrorT $ runErrorT aM₁ <⊔> runErrorT aM₂

-- Error Effect

instance (Functor m) ⇒ MonadError e (ErrorT e m) where
  errorE ∷ ErrorT e (ErrorT e m) ↝ ErrorT e m
  errorE = fdiscard ∘ errorCommute
  errorI ∷ ErrorT e m ↝ ErrorT e (ErrorT e m)
  errorI = errorCommute ∘ funit

-- Sum Error Effect

instance MonadError e ((⨄) e) where
  errorE ∷ ErrorT e ((⨄) e) ↝ (⨄) e
  errorE = runError ∘ errorE ∘ fmap throwSum
  errorI ∷ (⨄) e ↝ ErrorT e ((⨄) e)
  errorI = fmap runError ∘ errorI ∘ throwSum

-- # Reader

-- Base Effect

type Reader r = ReaderT r ID

reader ∷ (r → a) → Reader r a
reader f = ReaderT $ ID ∘ f

runReader ∷ Reader r a → r → a
runReader = runID ∘∘ runReaderT

runReaderWith ∷ r → Reader r a → a
runReaderWith = flip runReader

-- Commuting with self

readerCommute ∷ ReaderT r₁ (ReaderT r₂ m) ↝ ReaderT r₂ (ReaderT r₁ m)
readerCommute aMM = ReaderT $ \ r₂ → ReaderT $ \ r₁ → runReaderTWith r₂ $ runReaderTWith r₁ aMM

-- Functor and Monad

instance (Functor m) ⇒ Functor (ReaderT r m) where
  map ∷ (a → b) → ReaderT r m a → ReaderT r m b
  map f aM = ReaderT $ map f ∘ runReaderT aM
instance (Monad m) ⇒ Monad (ReaderT r m) where
  return ∷ a → ReaderT r m a
  return = ReaderT ∘ const ∘ return
  (≫=) ∷ ReaderT r m a → (a → ReaderT r m b) → ReaderT r m b
  aM ≫= k = ReaderT $ \ r → runReaderTWith r ∘ k *$ runReaderTWith r aM

-- Higher Functor

instance FunctorUnit (ReaderT r) where
  funit ∷ (Functor m) ⇒ m ↝ ReaderT r m
  funit = ReaderT ∘ const
instance FunctorDiscard (ReaderT r) where
  fdiscard ∷ (Functor m) ⇒ ReaderT r (ReaderT r m) ↝ ReaderT r m 
  fdiscard aMM = ReaderT $ \ r → runReaderTWith r $ runReaderTWith r aMM
instance FunctorFunctor (ReaderT r) where
  fmap ∷ (m ↝ n) → (ReaderT r m ↝ ReaderT r n)
  fmap f aM = ReaderT $ \ r → f $ runReaderTWith r aM

-- MonadMonoid and Join

instance (MonadMonoid m) ⇒ MonadMonoid (ReaderT r m) where
  mnull ∷ ReaderT r m a
  mnull = ReaderT $ const mnull
  (<⧺>) ∷ ReaderT r m a → ReaderT r m a → ReaderT r m a
  aM₁ <⧺> aM₂ = ReaderT $ \ r → runReaderT aM₁ r <⧺> runReaderT aM₂ r
instance (MonadBot m) ⇒ MonadBot (ReaderT r m) where
  mbot ∷ ReaderT r m a
  mbot = ReaderT $ const mbot
instance (MonadJoin m) ⇒ MonadJoin (ReaderT r m) where
  (<⊔>) ∷ ReaderT r m a → ReaderT r m a → ReaderT r m a
  aM₁ <⊔> aM₂ = ReaderT $ \ r → runReaderT aM₁ r <⊔> runReaderT aM₂ r
instance (MonadJoinLattice m) ⇒ MonadJoinLattice (ReaderT r m)

-- Reader Effect

instance (Functor m) ⇒ MonadReader r (ReaderT r m) where
  readerE ∷ ReaderT r (ReaderT r m) ↝ ReaderT r m
  readerE = fdiscard ∘ readerCommute
  readerI ∷ ReaderT r m ↝ ReaderT r (ReaderT r m)
  readerI = readerCommute ∘ funit

-- Base Reader Effect

instance MonadReader r ((→) r) where
  readerE ∷ ReaderT r ((→) r) ↝ (→) r
  readerE = runReader ∘ readerE ∘ fmap reader
  readerI ∷ (→) r ↝ ReaderT r ((→) r)
  readerI = fmap runReader ∘ readerI ∘ reader

-- # Writer

-- Base Effect

type Writer o = WriterT o ID

writer ∷ (a,o) → Writer o a
writer = WriterT ∘ ID

runWriter ∷ Writer o a → (a,o)
runWriter = runID ∘ runWriterT

execWriter ∷ Writer o a → o
execWriter = snd ∘ runWriter

-- Commuting with self

writerCommute ∷ ∀ m o₁ o₂. (Functor m) ⇒ WriterT o₁ (WriterT o₂ m) ↝ WriterT o₂ (WriterT o₁ m)
writerCommute aMM = WriterT $ WriterT $ ff ^$ runWriterT $ runWriterT aMM
  where
    ff ∷ ((a,o₁),o₂) → ((a,o₂),o₁)
    ff ((a,o₁),o₂) = ((a,o₂),o₁)

-- Functor and Monad

instance (Functor m) ⇒ Functor (WriterT o m) where 
  map ∷ (a → b) → WriterT o m a → WriterT o m b
  map f = WriterT ∘ mapFst f ^∘ runWriterT
instance (Monad m,Monoid o) ⇒ Monad (WriterT o m) where
  return ∷ a → WriterT o m a
  return = WriterT ∘ return ∘ (,null)
  (≫=) ∷ WriterT o m a → (a → WriterT o m b) → WriterT o m b
  aM ≫= k = WriterT $ do
    (a,o₁) ← runWriterT aM
    (b,o₂) ← runWriterT $ k a
    o' ← return ♯$ o₁ ⧺ o₂
    return (b,o')

-- Higher Functor

instance (Monoid o) ⇒ FunctorUnit (WriterT o) where
  funit ∷ (Functor m) ⇒ m ↝ WriterT o m
  funit = WriterT ∘ map (,null)
instance FunctorDiscard (WriterT o) where
  fdiscard ∷ (Functor m) ⇒ WriterT o (WriterT o m) ↝ WriterT o m
  fdiscard = fst ^∘ runWriterT
instance FunctorFunctor (WriterT o) where
  fmap ∷ (m ↝ n) → (WriterT o m ↝ WriterT o n)
  fmap f aM = WriterT $ f $ runWriterT aM

-- MonadMonoid and MonadJoin

instance (MonadMonoid m,Monoid o) ⇒ MonadMonoid (WriterT o m) where
  mnull ∷ WriterT o m a
  mnull = WriterT mnull
  (<⧺>) ∷ WriterT o m a → WriterT o m a → WriterT o m a
  aM₁ <⧺> aM₂ = WriterT $ runWriterT aM₁ <⧺> runWriterT aM₂
instance (MonadBot m,Monoid o) ⇒ MonadBot (WriterT o m) where
  mbot ∷ WriterT o m a
  mbot = WriterT mbot
instance (MonadJoin m,Monoid o) ⇒ MonadJoin (WriterT o m) where
  (<⊔>) ∷ WriterT o m a → WriterT o m a → WriterT o m a
  aM₁ <⊔> aM₂ = WriterT $ runWriterT aM₁ <⊔> runWriterT aM₂
instance (MonadJoinLattice m,Monoid o) ⇒ MonadJoinLattice (WriterT o m)

-- Monoid Functor

instance (Functorial Monoid m,Monoid o,Monoid a) ⇒ Monoid (WriterT o m a) where
  null ∷ WriterT o m a
  null =
    with (functorial ∷ W (Monoid (m (a,o)))) $
    WriterT null
  (⧺) ∷ WriterT o m a → WriterT o m a → WriterT o m a
  aM₁ ⧺ aM₂ =
    with (functorial ∷ W (Monoid (m (a,o)))) $
    WriterT $ runWriterT aM₁ ⧺ runWriterT aM₂
instance (Functorial Monoid m,Monoid o) ⇒ Functorial Monoid (WriterT o m) where functorial = W

-- Writer Effect

instance (Functor m,Monoid o) ⇒ MonadWriter o (WriterT o m) where
  writerE ∷ WriterT o (WriterT o m) ↝ WriterT o m
  writerE = fdiscard ∘ writerCommute
  writerI ∷ WriterT o m ↝ WriterT o (WriterT o m)
  writerI = writerCommute ∘ funit

-- Base Writer Effect

instance (Monoid o) ⇒ MonadWriter o ((,) o) where
  writerE ∷ WriterT o ((,) o) ↝ ((,) o)
  writerE = swap ∘ runWriter ∘ writerE ∘ fmap (writer ∘ swap)
  writerI ∷ ((,) o) ↝ WriterT o ((,) o)
  writerI = fmap (swap ∘ runWriter) ∘ writerI ∘ writer ∘ swap

-- # State

-- Base Effect

type State s = StateT s ID

runStateWith ∷ s → State s a → (a,s)
runStateWith = runID ∘∘ runStateTWith

evalStateWith ∷ s → State s a → a
evalStateWith = fst ∘∘ runStateWith

execStateWith ∷ s → State s a → s
execStateWith = snd ∘∘ runStateWith

-- Commuting with self

stateCommute ∷ ∀ m s₁ s₂. (Functor m) ⇒ StateT s₁ (StateT s₂ m) ↝ StateT s₂ (StateT s₁ m)
stateCommute aMM = StateT $ \ s₂ → StateT $ \ s₁ → ff ^$ runStateTWith s₂ $ runStateTWith s₁ aMM
  where
    ff ∷ ((a,s₁),s₂) → ((a,s₂),s₁)
    ff ((a,s₁),s₂) = ((a,s₂),s₁)

-- Functor and Monad

instance (Functor m) ⇒ Functor (StateT s m) where 
  map ∷ (a → b) → StateT s m a → StateT s m b
  map f aM = StateT $ \ s → mapFst f ^$ runStateT aM s
instance (Monad m) ⇒ Monad (StateT s m) where
  return ∷ a → StateT s m a
  return x = StateT $ \ s → return (x,s)
  (≫=) ∷ StateT s m a → (a → StateT s m b) → StateT s m b
  aM ≫= k = StateT $ \ s → do
    (a,s') ← runStateT aM s
    runStateT (k a) s'

-- Higher Functor

instance FunctorUnit (StateT s) where 
  funit ∷ (Functor m) ⇒ m ↝ StateT s m
  funit aM = StateT $ \ s → (,s) ^$ aM
instance FunctorDiscard (StateT s) where 
  fdiscard ∷ (Functor m) ⇒ StateT s (StateT s m) ↝ StateT s m
  fdiscard aMM = StateT $ \ s → runStateTWith s $ fst ^$ runStateTWith s aMM
instance FunctorFunctor (StateT s) where
  fmap ∷ (m ↝ n) → StateT s m ↝ StateT s n
  fmap f aM = StateT $ f ∘ runStateT aM

-- MonadMonoid and MonadJoin

instance (MonadMonoid m) ⇒ MonadMonoid (StateT s m) where
  mnull ∷ StateT s m a
  mnull = StateT $ const mnull
  (<⧺>) ∷ StateT s m a → StateT s m a → StateT s m a
  aM₁ <⧺> aM₂ = StateT $ \ s → runStateT aM₁ s <⧺> runStateT aM₂ s
instance (MonadBot m) ⇒ MonadBot (StateT s m) where
  mbot ∷ StateT s m a
  mbot = StateT $ const mbot
instance (MonadJoin m) ⇒ MonadJoin (StateT s m) where
  (<⊔>) ∷ StateT s m a → StateT s m a → StateT s m a
  aM₁ <⊔> aM₂ = StateT $ \ s → runStateT aM₁ s <⊔> runStateT aM₂ s
instance (MonadJoinLattice m) ⇒ MonadJoinLattice (StateT s m)
instance (MonadTop m) ⇒ MonadTop (StateT s m) where 
  mtop ∷ StateT s m a
  mtop = StateT $ const mtop

-- Monoid Functor

instance (Functorial Monoid m,Monoid s,Monoid a) ⇒ Monoid (StateT s m a) where
  null ∷ StateT s m a
  null =
    with (functorial ∷ W (Monoid (m (a,s)))) $
    StateT $ \ _ → null
  (⧺) ∷ StateT s m a → StateT s m a → StateT s m a
  aM₁ ⧺ aM₂ =
    with (functorial ∷ W (Monoid (m (a,s)))) $
    StateT $ \ s → runStateT aM₁ s ⧺ runStateT aM₂ s
instance (Functorial Monoid m,Monoid s) ⇒ Functorial Monoid (StateT s m) where functorial = W

-- JoinLattice Functor

instance (Functorial JoinLattice m,JoinLattice s,JoinLattice a) ⇒ Bot (StateT s m a) where
  bot ∷ StateT s m a
  bot = 
    with (functorial ∷ W (JoinLattice (m (a,s)))) $
    StateT $ \ _ → bot
instance (Functorial JoinLattice m,JoinLattice s,JoinLattice a) ⇒ Join (StateT s m a) where
  (⊔) ∷ StateT s m a → StateT s m a → StateT s m a
  aM₁ ⊔ aM₂ = 
    with (functorial ∷ W (JoinLattice (m (a,s)))) $
    StateT $ \ s → runStateT aM₁ s ⊔ runStateT aM₂ s
instance (Functorial JoinLattice m,JoinLattice s,JoinLattice a) ⇒ JoinLattice (StateT s m a)
instance (Functorial JoinLattice m,JoinLattice s) ⇒ Functorial JoinLattice (StateT s m) where functorial = W

-- State Effect

instance (Functor m) ⇒ MonadState s (StateT s m) where
  stateE ∷ StateT s (StateT s m) ↝ StateT s m
  stateE = fdiscard ∘ stateCommute
  stateI ∷ StateT s m ↝ StateT s (StateT s m) 
  stateI = stateCommute ∘ funit

-- # NondetAppendT [Append/Join]

-- Commuting with self

pluck ∷ [a] → [[a]] → Maybe ([a],[[a]])
pluck [] _ = Nothing
pluck (x:xs) [] = Just ([x],[xs])
pluck (x₁:xs₁) (xs₂:xss) = case pluck xs₂ xss of
  Nothing → Nothing
  Just (ys₂,xss') → Just (x₁:ys₂,xs₁:xss')

transpose ∷ [[a]] → [[a]]
transpose [] = [[]]
transpose (xs:xss) =
  case pluck xs xss of
    Nothing → []
    Just (ys,xss') → ys:transpose xss'

nondetAppendCommute ∷ (Functor m) ⇒ NondetAppendT (NondetAppendT m) ↝ NondetAppendT (NondetAppendT m)
nondetAppendCommute = NondetAppendT ∘ NondetAppendT ∘ map transpose ∘ runNondetAppendT ∘ runNondetAppendT

transposeSetLazy ∷ 𝒫ᵇ (𝒫ᵇ a) → 𝒫ᵇ (𝒫ᵇ a)
transposeSetLazy = lazySet ∘ map lazySet ∘ transpose ∘ list ∘ map list

nondetCommute ∷ (Functor m) ⇒ NondetJoinT (NondetJoinT m) ↝ NondetJoinT (NondetJoinT m)
nondetCommute = NondetJoinT ∘ NondetJoinT ∘ map transposeSetLazy ∘ runNondetJoinT ∘ runNondetJoinT

-- Monoid, Functor and Monad

instance (Functorial Monoid m) ⇒ Monoid (NondetAppendT m a) where
  null ∷ NondetAppendT m a
  null =
    with (functorial ∷ W (Monoid (m [a]))) $
    NondetAppendT null
  (⧺) ∷ NondetAppendT m a → NondetAppendT m a → NondetAppendT m a
  xs ⧺ ys =
    with (functorial ∷ W (Monoid (m [a]))) $
    NondetAppendT $ runNondetAppendT xs ⧺ runNondetAppendT ys
instance (Functorial Monoid m) ⇒ Functorial Monoid (NondetAppendT m) where functorial = W

instance (Functorial JoinLattice m) ⇒ Bot (NondetJoinT m a) where
  bot ∷ NondetJoinT m a
  bot =
    with (functorial ∷ W (JoinLattice (m (𝒫ᵇ a)))) $
    NondetJoinT bot
instance (Functorial JoinLattice m) ⇒ Join (NondetJoinT m a) where
  (⊔) ∷ NondetJoinT m a → NondetJoinT m a → NondetJoinT m a
  xs ⊔ ys =
    with (functorial ∷ W (JoinLattice (m (𝒫ᵇ a)))) $
    NondetJoinT $ runNondetJoinT xs ⊔ runNondetJoinT ys
instance (Functorial JoinLattice m) ⇒ JoinLattice (NondetJoinT m a)
instance (Functorial JoinLattice m) ⇒ Functorial JoinLattice (NondetJoinT m) where functorial = W

instance (Functor m) ⇒ Functor (NondetAppendT m) where
  map ∷ (a → b) → NondetAppendT m a → NondetAppendT m b
  map f = NondetAppendT ∘ map (map f) ∘ runNondetAppendT
instance (Monad m,Functorial Monoid m) ⇒ Monad (NondetAppendT m) where
  return ∷ a → NondetAppendT m a
  return = NondetAppendT ∘ return ∘ return
  (≫=) ∷ NondetAppendT m a → (a → NondetAppendT m b) → NondetAppendT m b
  aM ≫= k = NondetAppendT $ do
    xs ← runNondetAppendT aM
    runNondetAppendT $ concat $ k ^$ xs

instance (Functor m) ⇒ Functor (NondetJoinT m) where
  map ∷ (a → b) → NondetJoinT m a → NondetJoinT m b
  map f = NondetJoinT ∘ map (map f) ∘ runNondetJoinT
instance (Monad m,Functorial JoinLattice m) ⇒ Monad (NondetJoinT m) where
  return ∷ a → NondetJoinT m a
  return = NondetJoinT ∘ return ∘ return
  (≫=) ∷ NondetJoinT m a → (a → NondetJoinT m b) → NondetJoinT m b
  aM ≫= k = NondetJoinT $ do
    xs ← runNondetJoinT aM
    runNondetJoinT $ joins $ k ^$ xs

-- Higher Functor

instance FunctorUnit NondetAppendT where
  funit ∷ (Functor m) ⇒ m ↝ NondetAppendT m
  funit = NondetAppendT ∘ map return
instance FunctorDiscard NondetAppendT where
  fdiscard ∷ (Functor m) ⇒ NondetAppendT (NondetAppendT m) ↝ NondetAppendT m
  fdiscard = NondetAppendT ∘ concat ^∘ runNondetAppendT ∘ runNondetAppendT
instance FunctorFunctor NondetAppendT where
  fmap ∷ m ↝ n → NondetAppendT m ↝ NondetAppendT n
  fmap f = NondetAppendT ∘ f ∘ runNondetAppendT

instance FunctorUnit NondetJoinT where
  funit ∷ (Functor m) ⇒ m ↝ NondetJoinT m
  funit = NondetJoinT ∘ map return
instance FunctorDiscard NondetJoinT where
  fdiscard ∷ (Functor m) ⇒ NondetJoinT (NondetJoinT m) ↝ NondetJoinT m
  fdiscard = NondetJoinT ∘ joins ^∘ runNondetJoinT ∘ runNondetJoinT
instance FunctorFunctor NondetJoinT where
  fmap ∷ m ↝ n → NondetJoinT m ↝ NondetJoinT n
  fmap f = NondetJoinT ∘ f ∘ runNondetJoinT

-- Monad Monoid

instance (Functorial Monoid m) ⇒ MonadMonoid (NondetAppendT m) where {mnull = null;(<⧺>) = (⧺)}
instance MonadMonoid [] where {mnull = null;(<⧺>) = (⧺)}

instance (Functorial JoinLattice m) ⇒ MonadBot (NondetJoinT m) where mbot = bot
instance (Functorial JoinLattice m) ⇒ MonadJoin (NondetJoinT m) where (<⊔>) = (⊔)
instance (Functorial JoinLattice m) ⇒ MonadJoinLattice (NondetJoinT m)
instance MonadBot 𝒫ᵇ where mbot = bot
instance MonadJoin 𝒫ᵇ where (<⊔>) = (⊔)

-- Nondet Effect

instance (Functor m) ⇒ MonadNondetAppend (NondetAppendT m) where
  nondetAppendE ∷ NondetAppendT (NondetAppendT m) ↝ NondetAppendT m
  nondetAppendE = fdiscard ∘ nondetAppendCommute
  nondetAppendI ∷ NondetAppendT m ↝ NondetAppendT (NondetAppendT m)
  nondetAppendI = nondetAppendCommute ∘ funit

instance (Functor m) ⇒ MonadNondetJoin (NondetJoinT m) where
  nondetJoinE ∷ NondetJoinT (NondetJoinT m) ↝ NondetJoinT m
  nondetJoinE = fdiscard ∘ nondetCommute
  nondetJoinI ∷ NondetJoinT m ↝ NondetJoinT (NondetJoinT m)
  nondetJoinI = nondetCommute ∘ funit

-- # Flow [Append/Join]

-- Commuting with self

flowCommuteAppend ∷ ∀ s₁ s₂ m. (Functor m,Monoid s₁) ⇒ FlowAppendT s₁ (FlowAppendT s₂ m) ↝ FlowAppendT s₂ (FlowAppendT s₁ m)
flowCommuteAppend xMM = FlowAppendT $ \ s₂ → FlowAppendT $ \ s₁ → ff ^$ runFlowAppendT (runFlowAppendT xMM s₁) s₂
  where
    ff ∷ ∀ a. (a ⇰♭⧺ s₁) ⇰♭⧺ s₂ → (a ⇰♭⧺ s₂) ⇰♭⧺ s₁
    ff = lazyDictAppend ∘ map (mapFst lazyDictAppend) ∘ map merge ∘ map (mapFst list) ∘ list
      where
        merge ∷ ([(a,s₁)],s₂) → ([(a,s₂)],s₁)
        merge (xs₁s,s₂) = (map (\ (x,_) → (x,s₂)) xs₁s,concat $ map snd xs₁s)

flowCommuteJoin ∷ ∀ s₁ s₂ m. (Functor m,JoinLattice s₁) ⇒ FlowJoinT s₁ (FlowJoinT s₂ m) ↝ FlowJoinT s₂ (FlowJoinT s₁ m)
flowCommuteJoin xMM = FlowJoinT $ \ s₂ → FlowJoinT $ \ s₁ → ff ^$ runFlowJoinT (runFlowJoinT xMM s₁) s₂
  where
    ff ∷ ∀ a. (a ⇰♭⊔ s₁) ⇰♭⊔ s₂ → (a ⇰♭⊔ s₂) ⇰♭⊔ s₁
    ff = lazyDictJoin ∘ map (mapFst lazyDictJoin) ∘ map merge ∘ map (mapFst list) ∘ list
      where
        merge ∷ ([(a,s₁)],s₂) → ([(a,s₂)],s₁)
        merge (xs₁s,s₂) = (map (\ (x,_) → (x,s₂)) xs₁s,joins $ map snd xs₁s)

-- Monoid/Functor/Monad

instance (Functorial Monoid m,Monoid s) ⇒ Monoid (FlowAppendT s m a) where
  null ∷ FlowAppendT s m a
  null = 
    with (functorial ∷ W (Monoid (m (a ⇰♭⧺ s)))) $
    FlowAppendT $ \ _ → null
  (⧺) ∷ FlowAppendT s m a → FlowAppendT s m a → FlowAppendT s m a
  xss₁ ⧺ xss₂ = 
    with (functorial ∷ W (Monoid (m (a ⇰♭⧺ s)))) $  
    FlowAppendT $ \ s → runFlowAppendT xss₁ s ⧺ runFlowAppendT xss₂ s
instance (Functorial JoinLattice m,JoinLattice s) ⇒ Bot (FlowJoinT s m a) where
  bot ∷ FlowJoinT s m a
  bot = 
    with (functorial ∷ W (JoinLattice (m (a ⇰♭⊔ s)))) $
    FlowJoinT $ \ _ → bot
instance (Functorial JoinLattice m,JoinLattice s) ⇒ Join (FlowJoinT s m a) where
  (⊔) ∷ FlowJoinT s m a → FlowJoinT s m a → FlowJoinT s m a
  xss₁ ⊔ xss₂ = 
    with (functorial ∷ W (JoinLattice (m (a ⇰♭⊔ s)))) $  
    FlowJoinT $ \ s → runFlowJoinT xss₁ s ⊔ runFlowJoinT xss₂ s
instance (Functorial JoinLattice m,JoinLattice s) ⇒ JoinLattice (FlowJoinT s m a)

instance (Functor m) ⇒ Functor (FlowAppendT s m) where
  map ∷ (a → b) → FlowAppendT s m a → FlowAppendT s m b
  map f xM = FlowAppendT $ \ s → map (mapKeyLazyDictAppend f) $ runFlowAppendT xM s
instance (Monad m,Functorial Monoid m,Monoid s) ⇒ Monad (FlowAppendT s m) where
  return ∷ a → FlowAppendT s m a
  return x = FlowAppendT $ \ s → return $ lazyDictAppend [(x,s)]
  (≫=) ∷ ∀ a b. FlowAppendT s m a → (a → FlowAppendT s m b) → FlowAppendT s m b
  xM ≫= f = 
    with (functorial ∷ W (Monoid (m (b ⇰♭⧺ s)))) $
    FlowAppendT $ \ s → do
      xss ← runLazyDictAppend ^$ runFlowAppendT xM s
      concat $ mapOn xss $ \ (x,s') → runFlowAppendT (f x) s'

instance (Functor m) ⇒ Functor (FlowJoinT s m) where
  map ∷ (a → b) → FlowJoinT s m a → FlowJoinT s m b
  map f xM = FlowJoinT $ \ s → map (mapKeyLazyDictJoin f) $ runFlowJoinT xM s
instance (Monad m,Functorial JoinLattice m,JoinLattice s) ⇒ Monad (FlowJoinT s m) where
  return ∷ a → FlowJoinT s m a
  return x = FlowJoinT $ \ s → return $ lazyDictJoin [(x,s)]
  (≫=) ∷ ∀ a b. FlowJoinT s m a → (a → FlowJoinT s m b) → FlowJoinT s m b
  xM ≫= f = 
    with (functorial ∷ W (JoinLattice (m (b ⇰♭⊔ s)))) $
    FlowJoinT $ \ s → do
      xss ← runLazyDictJoin ^$ runFlowJoinT xM s
      joins $ mapOn xss $ \ (x,s') → runFlowJoinT (f x) s'

-- Higher Functor

instance FunctorUnit (FlowAppendT s) where
  funit ∷ (Functor m) ⇒ m ↝ FlowAppendT s m
  funit xM = FlowAppendT $ \ s → ff s ^$ xM
    where
      ff s x = lazyDictAppend [(x,s)]
instance (Monoid s) ⇒ FunctorDiscard (FlowAppendT s) where
  fdiscard ∷ ∀ m. (Functor m) ⇒ FlowAppendT s (FlowAppendT s m) ↝ FlowAppendT s m
  fdiscard xMM = FlowAppendT $ \ s → flip runFlowAppendT s $ ff $ runFlowAppendT xMM s
    where
      ff ∷ FlowAppendT s m (a ⇰♭⧺ s) → FlowAppendT s m a
      ff asM = FlowAppendT $ \ s → 
        lazyDictAppend ∘ concat ∘ map (\ (xs,s') → map (,s') (list xs)) ∘ runLazyDictAppend ^$ 
        runFlowAppendT (map (map fst ∘ runLazyDictAppend) asM) s
instance FunctorFunctor (FlowAppendT s) where
  fmap ∷ m ↝ n → FlowAppendT s m ↝ FlowAppendT s n
  fmap f xM = FlowAppendT $ \ s → f $ runFlowAppendT xM s

instance FunctorUnit (FlowJoinT s) where
  funit ∷ (Functor m) ⇒ m ↝ FlowJoinT s m
  funit xM = FlowJoinT $ \ s → ff s ^$ xM
    where
      ff s x = lazyDictJoin [(x,s)]
instance (JoinLattice s) ⇒ FunctorDiscard (FlowJoinT s) where
  fdiscard ∷ ∀ m. (Functor m) ⇒ FlowJoinT s (FlowJoinT s m) ↝ FlowJoinT s m
  fdiscard xMM = FlowJoinT $ \ s → flip runFlowJoinT s $ ff $ runFlowJoinT xMM s
    where
      ff ∷ FlowJoinT s m (a ⇰♭⊔ s) → FlowJoinT s m a
      ff asM = FlowJoinT $ \ s → 
        lazyDictJoin ∘ concat ∘ map (\ (xs,s') → map (,s') (list xs)) ∘ runLazyDictJoin ^$ 
        runFlowJoinT (map (map fst ∘ runLazyDictJoin) asM) s
instance FunctorFunctor (FlowJoinT s) where
  fmap ∷ m ↝ n → FlowJoinT s m ↝ FlowJoinT s n
  fmap f xM = FlowJoinT $ \ s → f $ runFlowJoinT xM s

-- Sum Effects

instance (Monoid s,Functorial Monoid m) ⇒ MonadMonoid (FlowAppendT s m) where {mnull = null;(<⧺>) = (⧺)}
instance (JoinLattice s,Functorial JoinLattice m) ⇒ MonadBot (FlowJoinT s m) where mbot = bot
instance (JoinLattice s,Functorial JoinLattice m) ⇒ MonadJoin (FlowJoinT s m) where (<⊔>) = (⊔)
instance (JoinLattice s,Functorial JoinLattice m) ⇒ MonadJoinLattice (FlowJoinT s m)

-- Flow Effect

instance (Functor m,Monoid s) ⇒ MonadFlowAppend s (FlowAppendT s m) where
  flowAppendE ∷ FlowAppendT s (FlowAppendT s m) ↝ FlowAppendT s m
  flowAppendE = fdiscard ∘ flowCommuteAppend
  flowAppendI ∷ FlowAppendT s m ↝ FlowAppendT s (FlowAppendT s m)
  flowAppendI = flowCommuteAppend ∘ funit

instance (Functor m,JoinLattice s) ⇒ MonadFlowJoin s (FlowJoinT s m) where
  flowJoinE ∷ FlowJoinT s (FlowJoinT s m) ↝ FlowJoinT s m
  flowJoinE = fdiscard ∘ flowCommuteJoin
  flowJoinI ∷ FlowJoinT s m ↝ FlowJoinT s (FlowJoinT s m)
  flowJoinI = flowCommuteJoin ∘ funit

-- Also supports state effects

flowJoinFromState ∷ (Functor m) ⇒ StateT s m ↝ FlowJoinT s m
flowJoinFromState xM = FlowJoinT $ \ s → ff ^$ runStateT xM s
  where
    ff ∷ (a,s) → a ⇰♭⊔ s
    ff = lazyDictJoin ∘ singleFold

flowJoinStateI ∷ (Functor m) ⇒ FlowJoinT s m ↝ StateT s (FlowJoinT s m)
flowJoinStateI xsM = StateT $ \ s → FlowJoinT $ \ s₀ → ff s₀ ^$ runFlowJoinT xsM s
  where
    ff ∷ s → a ⇰♭⊔ s → (a,s) ⇰♭⊔ s
    ff s₀ = lazyDictJoin ∘ map (,s₀) ∘ list 
instance (Functor m,JoinLattice s) ⇒ MonadState s (FlowJoinT s m) where
  stateE ∷ StateT s (FlowJoinT s m) ↝ FlowJoinT s m
  stateE = flowJoinE ∘ flowJoinFromState
  stateI ∷ FlowJoinT s m ↝ StateT s (FlowJoinT s m)
  stateI = flowJoinStateI

-- # ContT

-- Base Effect

type Cont r = ContT r ID

cont ∷ ((a → r) → r) → Cont r a
cont k = ContT $ \ k' → ID $ k $ \ a → runID $ k' a

runCont ∷ Cont r a → (a → r) → r
runCont aM f = runID $ runContT aM (ID ∘ f)

evalCont ∷ Cont r r → r
evalCont aM = runCont aM id

-- Functor and Monad

instance Functor (ContT r m) where map = mmap
instance Monad (ContT r m) where
  return ∷ a → ContT r m a
  return a = ContT $ \ k → k a
  (≫=) ∷ ContT r m a → (a → ContT r m b) → ContT r m b
  aM ≫= kM = ContT $ \ (k ∷ b → m r) → runContT aM $ \ a → runContT (kM a) k

-- Higher Functor

instance FunctorIsoFunctor (ContT r) where
  fisomap ∷ (m ↝ n,n ↝ m) → (ContT r m ↝ ContT r n)
  fisomap (to,from) aM = ContT $ \ (k ∷ a → n r) → to $ runContT aM $ \ a → from $ k a

-- Cont Effect

instance (Monad m) ⇒ MonadCont r (ContT r m) where
  contE ∷ ContT r (ContT r m) ↝ ContT r m
  contE aMM = ContT $ \ (k ∷ a → m r) → 
    evalContT $ runContT aMM $ \ a → ContT $ \ (k' ∷ r → m r) → k' *$ k a
  contI ∷ ContT r m ↝ ContT r (ContT r m)
  contI aM = ContT $ \ (k₁ ∷ a → ContT r m r) → ContT $ \ (k₂ ∷ r → m r) →
    k₂ *$ runContT aM $ \ a → evalContT (k₁ a)

-- # OpaqueContT

-- Base Effect

type OpaqueCont k r = OpaqueContT k r ID

opaqueCont ∷ (k r ID a → r) → OpaqueCont k r a
opaqueCont nk = OpaqueContT $ ID ∘ nk

runOpaqueCont ∷ OpaqueCont k r a → k r ID a → r
runOpaqueCont = runID ∘∘ runOpaqueContT

metaCont ∷ (Isomorphic3 (k r) (ContFun r)) ⇒ ((a → r) → r) → OpaqueCont k r a
metaCont nk = opaqueCont $ \ (k ∷ k r ID a) → nk $ (∘) runID ∘ runContFun $ isoTo3 isomorphic3 k

runMetaCont ∷ (Isomorphic3 (ContFun r) (k r)) ⇒ OpaqueCont k r a → (a → r) → r
runMetaCont aM k = runOpaqueCont aM $ isoTo3 isomorphic3 $ ContFun $ ID ∘ k

evalOpaqueCont ∷ (Isomorphic3 (ContFun r) (k r)) ⇒ OpaqueCont k r r → r
evalOpaqueCont aM = runMetaCont aM id

-- Functor and Monad

instance (Monad m,Isomorphic3 (ContFun r) (k r)) ⇒ Functor (OpaqueContT k r m) where map = mmap
instance (Monad m,Isomorphic3 (ContFun r) (k r)) ⇒ Monad (OpaqueContT k r m) where
  return ∷ a → OpaqueContT k r m a
  return a = OpaqueContT $ \ k → runContFun (isoFrom3 isomorphic3 k) a
  (≫=) ∷ OpaqueContT k r m a → (a → OpaqueContT k r m b) → OpaqueContT k r m b
  aM ≫= kM = OpaqueContT $ \ (k ∷ k r m a) → runMetaContT aM $ \ a → runOpaqueContT (kM a) k

-- Higher Functor

instance (Isomorphic3 (ContFun r) (k r)) ⇒ FunctorIsoFunctor (OpaqueContT k r) where
  fisomap ∷ (m ↝ n,n ↝ m) → OpaqueContT k r m ↝ OpaqueContT k r n
  fisomap tofrom = opaque ∘ fisomap tofrom ∘ meta

-- OpaqueCont Effect

class Balloon k r | k → r where
  inflate ∷ (Monad m) ⇒ k r m ↝ k r (OpaqueContT k r m)
  deflate ∷ (Monad m) ⇒ k r (OpaqueContT k r m) ↝ k r m

instance (Monad m,Isomorphic3 (ContFun r) (k r),Balloon k r) ⇒ MonadOpaqueCont k r (OpaqueContT k r m) where
  opaqueContE ∷ OpaqueContT k r (OpaqueContT k r m) a → OpaqueContT k r m a
  opaqueContE kk = OpaqueContT $ \ (k ∷ k r m a ) → runMetaContTWith return $ runOpaqueContT kk $ inflate k
  opaqueContI ∷ OpaqueContT k r m a → OpaqueContT k r (OpaqueContT k r m) a
  opaqueContI aM = OpaqueContT $ \ k₁ → metaContT $ \ (k₂ ∷ r → m r) → k₂ *$ runOpaqueContT aM $ deflate k₁

instance (Monad m,Isomorphic3 (ContFun r) (k r)) ⇒ MonadCont r (OpaqueContT k r m) where
  contE ∷ ContT r (OpaqueContT k r m) ↝ OpaqueContT k r m
  contE aMM = metaContT $ \ (k ∷ a → m r) →
    runMetaContTWith return $ runContT aMM $ \ a → metaContT $ \ (k' ∷ r → m r) → k' *$ k a
  contI ∷ OpaqueContT k r m ↝ ContT r (OpaqueContT k r m)
  contI aM = ContT $ \ (k₁ ∷ a → OpaqueContT k r m r) → metaContT $ \ (k₂ ∷ r → m r) →
    k₂ *$ runMetaContT aM $ \ a → runMetaContT (k₁ a) return

----------------------
-- Monads Commuting --
----------------------

-- # Failure // *

-- ## Failure // Error [ISO]

failureErrorCommute ∷ (Functor m) ⇒ FailureT (ErrorT e m) ↝ ErrorT e (FailureT m)
failureErrorCommute = ErrorT ∘ FailureT ∘ map ff ∘ runErrorT ∘ runFailureT
  where
    ff ∷ (e ⨄ Maybe a) → Maybe (e ⨄ a)
    ff (Left e) = Just (Left e)
    ff (Right Nothing) = Nothing
    ff (Right (Just x)) = Just (Right x)

errorFailureCommute ∷ (Functor m) ⇒ ErrorT e (FailureT m) ↝ FailureT (ErrorT e m)
errorFailureCommute = FailureT ∘ ErrorT ∘ map ff ∘ runFailureT ∘ runErrorT
  where
    ff ∷ Maybe (e ⨄ a) → (e ⨄ Maybe a)
    ff Nothing = Right Nothing
    ff (Just (Left e)) = Left e
    ff (Just (Right x)) = Right (Just x)

instance (Functor m,MonadFailure m) ⇒ MonadFailure (ErrorT e m) where
  failureE ∷ FailureT (ErrorT e m) ↝ ErrorT e m
  failureE = fmap failureE ∘ failureErrorCommute
  failureI ∷ ErrorT e m ↝ FailureT (ErrorT e m)
  failureI = errorFailureCommute ∘ fmap failureI

instance (Functor m,MonadError e m) ⇒ MonadError e (FailureT m) where
  errorE ∷ ErrorT e (FailureT m) ↝ FailureT m
  errorE = fmap errorE ∘ errorFailureCommute
  errorI ∷ FailureT m ↝ ErrorT e (FailureT m)
  errorI = failureErrorCommute ∘ fmap errorI

-- ## Failure // Reader [ISO]

failureReaderCommute ∷ (Functor m) ⇒ FailureT (ReaderT r m) ↝ ReaderT r (FailureT m)
failureReaderCommute aMRM = ReaderT $ \ r → FailureT $ runReaderTWith r $ runFailureT aMRM

readerFailureCommute ∷ (Functor m) ⇒ ReaderT r (FailureT m) ↝ FailureT (ReaderT r m)
readerFailureCommute aRMM = FailureT $ ReaderT $ \ r → runFailureT $ runReaderTWith r aRMM

instance (Functor m,MonadFailure m) ⇒ MonadFailure (ReaderT r m) where
  failureE ∷ FailureT (ReaderT r m) ↝ ReaderT r m
  failureE = fmap failureE ∘ failureReaderCommute
  failureI ∷ ReaderT r m ↝ FailureT (ReaderT r m)
  failureI = readerFailureCommute ∘ fmap failureI

instance (Functor m,MonadReader r m) ⇒ MonadReader r (FailureT m) where
  readerE ∷ ReaderT r (FailureT m) ↝ FailureT m
  readerE = fmap readerE ∘ readerFailureCommute
  readerI ∷ FailureT m ↝ ReaderT r (FailureT m)
  readerI = failureReaderCommute ∘ fmap readerI

-- ## Failure // Writer [ADJ]

failureWriterCommute ∷ (Functor m) ⇒ FailureT (WriterT o m) ↝ WriterT o (FailureT m)
failureWriterCommute aMRM = WriterT $ FailureT $ ff ^$ runWriterT $ runFailureT aMRM
  where
    ff ∷ (Maybe a,o) → Maybe (a,o)
    ff (Nothing,_) = Nothing
    ff (Just a,o) = Just (a,o)

writerFailureCommute ∷ (Monoid o,Functor m) ⇒ WriterT o (FailureT m) ↝ FailureT (WriterT o m)
writerFailureCommute aRMM = FailureT $ WriterT $ ff ^$ runFailureT $ runWriterT aRMM
  where
    ff ∷ (Monoid o) ⇒ Maybe (a,o) → (Maybe a,o)
    ff Nothing = (Nothing,null)
    ff (Just (a,o)) = (Just a,o)

instance (Functor m,MonadFailure m,Monoid o) ⇒ MonadFailure (WriterT o m) where
  failureE ∷ FailureT (WriterT o m) ↝ WriterT o m
  failureE = fmap failureE ∘ failureWriterCommute
  failureI ∷ WriterT o m ↝ FailureT (WriterT o m)
  failureI = writerFailureCommute ∘ fmap failureI

instance (Functor m,MonadWriter o m,Monoid o) ⇒ MonadWriter o (FailureT m) where
  writerE ∷ WriterT o (FailureT m) ↝ FailureT m
  writerE = fmap writerE ∘ writerFailureCommute
  writerI ∷ FailureT m ↝ WriterT o (FailureT m)
  writerI = failureWriterCommute ∘ fmap writerI

-- ## Failure // State [ADJ]

failureStateCommute ∷ ∀ s m. (Functor m) ⇒ FailureT (StateT s m) ↝ StateT s (FailureT m)
failureStateCommute aMSM = StateT $ \ s₁ → FailureT $ ff ^$ runStateTWith s₁ $ runFailureT aMSM
  where
    ff ∷ (Maybe a,s) → Maybe (a,s)
    ff (Nothing,_) = Nothing
    ff (Just a,s₂) = Just (a,s₂)

stateFailureCommute ∷ ∀ s m. (Functor m) ⇒ StateT s (FailureT m) ↝ FailureT (StateT s m)
stateFailureCommute aSMM = FailureT $ StateT $ \ s₁ → ff s₁ ^$ runFailureT $ runStateTWith s₁ aSMM
  where
    ff ∷ s → (Maybe (a,s)) → (Maybe a,s)
    ff s₁ Nothing = (Nothing,s₁)
    ff _ (Just (a,s₂)) = (Just a,s₂)

instance (Functor m,MonadFailure m) ⇒ MonadFailure (StateT s m) where
  failureE ∷ FailureT (StateT s m) ↝ StateT s m
  failureE = fmap failureE ∘ failureStateCommute
  failureI ∷ StateT s m ↝ FailureT (StateT s m)
  failureI = stateFailureCommute ∘ fmap failureI

instance (Functor m,MonadState s m) ⇒ MonadState s (FailureT m) where
  stateE ∷ StateT s (FailureT m) ↝ FailureT m
  stateE = fmap stateE ∘ stateFailureCommute
  stateI ∷ FailureT m ↝ StateT s (FailureT m)
  stateI = failureStateCommute ∘ fmap stateI

-- ## Failure // Nondet [ADJ]

failureNondetAppendCommute ∷ (Functor m) ⇒ FailureT (NondetAppendT m) ↝ NondetAppendT (FailureT m)
failureNondetAppendCommute = NondetAppendT ∘ FailureT ∘ map ff ∘ runNondetAppendT ∘ runFailureT
  where
    ff ∷ [Maybe a] → Maybe [a]
    ff [] = Just []
    ff (Nothing:_) = Nothing
    ff (Just x:xMs) = (x:) ^$ ff xMs

nondetAppendFailureCommute ∷ (Functor m) ⇒ NondetAppendT (FailureT m) ↝ FailureT (NondetAppendT m)
nondetAppendFailureCommute = FailureT ∘ NondetAppendT ∘ map ff ∘ runFailureT ∘ runNondetAppendT
  where
    ff ∷ Maybe [a] → [Maybe a]
    ff Nothing = [Nothing]
    ff (Just xs) = map Just xs

instance (Functor m,MonadFailure m) ⇒ MonadFailure (NondetAppendT m) where
  failureE ∷ FailureT (NondetAppendT m) ↝ NondetAppendT m
  failureE = fmap failureE ∘ failureNondetAppendCommute
  failureI ∷ NondetAppendT m ↝ FailureT (NondetAppendT m)
  failureI = nondetAppendFailureCommute ∘ fmap failureI

instance (Functor m,MonadNondetAppend m) ⇒ MonadNondetAppend (FailureT m) where
  nondetAppendE ∷ NondetAppendT (FailureT m) ↝ FailureT m
  nondetAppendE = fmap nondetAppendE ∘ nondetAppendFailureCommute
  nondetAppendI ∷ FailureT m ↝ NondetAppendT (FailureT m)
  nondetAppendI = failureNondetAppendCommute ∘ fmap nondetAppendI

failureNondetCommute ∷ (Functor m) ⇒ FailureT (NondetJoinT m) ↝ NondetJoinT (FailureT m)
failureNondetCommute = NondetJoinT ∘ FailureT ∘ map (map lazySet ∘ ff ∘ list) ∘ runNondetJoinT ∘ runFailureT
  where
    ff ∷ [Maybe a] → Maybe [a]
    ff [] = Just []
    ff (Nothing:_) = Nothing
    ff (Just x:xMs) = (x:) ^$ ff xMs

nondetFailureCommute ∷ (Functor m) ⇒ NondetJoinT (FailureT m) ↝ FailureT (NondetJoinT m)
nondetFailureCommute = FailureT ∘ NondetJoinT ∘ map (lazySet ∘ ff ∘ map list) ∘ runFailureT ∘ runNondetJoinT
  where
    ff ∷ Maybe [a] → [Maybe a]
    ff Nothing = [Nothing]
    ff (Just xs) = map Just xs

instance (Functor m,MonadFailure m) ⇒ MonadFailure (NondetJoinT m) where
  failureE ∷ FailureT (NondetJoinT m) ↝ NondetJoinT m
  failureE = fmap failureE ∘ failureNondetCommute
  failureI ∷ NondetJoinT m ↝ FailureT (NondetJoinT m)
  failureI = nondetFailureCommute ∘ fmap failureI

instance (Functor m,MonadNondetJoin m) ⇒ MonadNondetJoin (FailureT m) where
  nondetJoinE ∷ NondetJoinT (FailureT m) ↝ FailureT m
  nondetJoinE = fmap nondetJoinE ∘ nondetFailureCommute
  nondetJoinI ∷ FailureT m ↝ NondetJoinT (FailureT m)
  nondetJoinI = failureNondetCommute ∘ fmap nondetJoinI

-- TODO: FlowAppendT

-- ## Failure // Cont

-- TODO: 

-- ## Failure // OpaqueCont

-- TODO: 

-- # Error // *

-- ## Error // Reader [ISO]

errorReaderCommute ∷ ErrorT e (ReaderT r m) ↝ ReaderT r (ErrorT e m)
errorReaderCommute aMRM = ReaderT $ \ r → ErrorT $ runReaderTWith r $ runErrorT aMRM

readerErrorCommute ∷ ReaderT r (ErrorT e m) ↝ ErrorT e (ReaderT r m)
readerErrorCommute aRMM = ErrorT $ ReaderT $ \ r → runErrorT $ runReaderTWith r aRMM

instance (Functor m,MonadError e m) ⇒ MonadError e (ReaderT r m) where
  errorE ∷ ErrorT e (ReaderT r m) ↝ ReaderT r m
  errorE = fmap errorE ∘ errorReaderCommute
  errorI ∷ ReaderT r m ↝ ErrorT e (ReaderT r m)
  errorI = readerErrorCommute ∘ fmap errorI

instance (Functor m,MonadReader r m) ⇒ MonadReader r (ErrorT e m) where
  readerE ∷ ReaderT r (ErrorT e m) ↝ ErrorT e m
  readerE = fmap readerE ∘ readerErrorCommute
  readerI ∷ ErrorT e m ↝ ReaderT r (ErrorT e m)
  readerI = errorReaderCommute ∘ fmap readerI

-- ## Error // Writer [ADJ]

errorWriterCommute ∷ ∀ e o m. (Functor m) ⇒ ErrorT e (WriterT o m) ↝ WriterT o (ErrorT e m)
errorWriterCommute = WriterT ∘ ErrorT ∘ ff ^∘ runWriterT ∘ runErrorT
  where
    ff ∷ (e ⨄ a,o) → (e ⨄ (a,o))
    ff (Left e,_) = Left e
    ff (Right a,o) = Right (a,o)

writerErrorCommute ∷ (Functor m,Monoid o) ⇒ WriterT o (ErrorT e m) ↝ ErrorT e (WriterT o m)
writerErrorCommute = ErrorT ∘ WriterT ∘ ff ^∘ runErrorT ∘ runWriterT
  where
    ff ∷ (Monoid o) ⇒ (e ⨄ (a,o)) → (e ⨄ a,o)
    ff (Left e) = (Left e,null)
    ff (Right (a,o)) = (Right a,o)

instance (Functor m,MonadError e m,Monoid o) ⇒ MonadError e (WriterT o m) where
  errorE ∷ ErrorT e (WriterT o m) ↝ WriterT o m
  errorE = fmap errorE ∘ errorWriterCommute
  errorI ∷ WriterT o m ↝ ErrorT e (WriterT o m)
  errorI = writerErrorCommute ∘ fmap errorI

instance (Functor m,MonadWriter o m,Monoid o) ⇒ MonadWriter o (ErrorT e m) where
  writerE ∷ WriterT o (ErrorT e m) ↝ ErrorT e m
  writerE = fmap writerE ∘ writerErrorCommute
  writerI ∷ ErrorT e m ↝ WriterT o (ErrorT e m)
  writerI = errorWriterCommute ∘ fmap writerI

-- ## Error // State [ADJ]

errorStateCommute ∷ (Functor m) ⇒ ErrorT e (StateT s m) ↝ StateT s (ErrorT e m)
errorStateCommute aMRM = StateT $ \ s → ErrorT $ ff ^$ runStateTWith s $ runErrorT aMRM
  where
    ff ∷ (e ⨄ a,s) → e ⨄ (a,s)
    ff (Left e,_) = Left e
    ff (Right a,s) = Right (a,s)

stateErrorCommute ∷ (Functor m) ⇒ StateT s (ErrorT e m) ↝ ErrorT e (StateT s m)
stateErrorCommute aRMM = ErrorT $ StateT $ \ s → ff s ^$ runErrorT $ runStateTWith s aRMM
  where
    ff ∷ s → e ⨄ (a,s) → (e ⨄ a,s)
    ff s (Left e) = (Left e,s)
    ff _ (Right (a,s)) = (Right a,s)

instance (Functor m,MonadError e m) ⇒ MonadError e (StateT s m) where
  errorE ∷ ErrorT e (StateT s m) ↝ StateT s m
  errorE = fmap errorE ∘ errorStateCommute
  errorI ∷ StateT s m ↝ ErrorT e (StateT s m)
  errorI = stateErrorCommute ∘ fmap errorI

instance (Functor m,MonadState s m) ⇒ MonadState s (ErrorT e m) where
  stateE ∷ StateT s (ErrorT e m) ↝ ErrorT e m
  stateE = fmap stateE ∘ stateErrorCommute
  stateI ∷ ErrorT e m ↝ StateT s (ErrorT e m)
  stateI = errorStateCommute ∘ fmap stateI

-- ## Error // Nondet [ADJ]

errorNondetAppendCommute ∷ (Functor m) ⇒ ErrorT e (NondetAppendT m) ↝ NondetAppendT (ErrorT e m)
errorNondetAppendCommute = NondetAppendT ∘ ErrorT ∘ map ff ∘ runNondetAppendT ∘ runErrorT
  where
    ff ∷ [e ⨄ a] → e ⨄ [a]
    ff [] = Right []
    ff (Left e:_) = Left e
    ff (Right x:xsM) = (x:) ^$ ff xsM

nondetAppendErrorCommute ∷ (Functor m) ⇒ NondetAppendT (ErrorT e m) ↝ ErrorT e (NondetAppendT m)
nondetAppendErrorCommute = ErrorT ∘ NondetAppendT ∘ map ff ∘ runErrorT ∘ runNondetAppendT
  where
    ff ∷ e ⨄ [a] → [e ⨄ a]
    ff (Left e) = [Left e]
    ff (Right xs) = map Right xs

instance (Functor m,MonadError e m) ⇒ MonadError e (NondetAppendT m) where
  errorE ∷ ErrorT e (NondetAppendT m) ↝ NondetAppendT m
  errorE = fmap errorE ∘ errorNondetAppendCommute
  errorI ∷ NondetAppendT m ↝ ErrorT e (NondetAppendT m)
  errorI = nondetAppendErrorCommute ∘ fmap errorI

instance (Functor m,MonadNondetAppend m) ⇒ MonadNondetAppend (ErrorT e m) where
  nondetAppendE ∷ NondetAppendT (ErrorT e m) ↝ ErrorT e m
  nondetAppendE = fmap nondetAppendE ∘ nondetAppendErrorCommute
  nondetAppendI ∷ ErrorT e m ↝ NondetAppendT (ErrorT e m)
  nondetAppendI = errorNondetAppendCommute ∘ fmap nondetAppendI

errorNondetCommute ∷ (Functor m) ⇒ ErrorT e (NondetJoinT m) ↝ NondetJoinT (ErrorT e m)
errorNondetCommute = NondetJoinT ∘ ErrorT ∘ map (map lazySet ∘ ff ∘ list) ∘ runNondetJoinT ∘ runErrorT
  where
    ff ∷ [e ⨄ a] → e ⨄ [a]
    ff [] = Right []
    ff (Left e:_) = Left e
    ff (Right x:xsM) = (x:) ^$ ff xsM

nondetErrorCommute ∷ (Functor m) ⇒ NondetJoinT (ErrorT e m) ↝ ErrorT e (NondetJoinT m)
nondetErrorCommute = ErrorT ∘ NondetJoinT ∘ map (lazySet ∘ ff ∘ map list) ∘ runErrorT ∘ runNondetJoinT
  where
    ff ∷ e ⨄ [a] → [e ⨄ a]
    ff (Left e) = [Left e]
    ff (Right xs) = map Right xs

instance (Functor m,MonadError e m) ⇒ MonadError e (NondetJoinT m) where
  errorE ∷ ErrorT e (NondetJoinT m) ↝ NondetJoinT m
  errorE = fmap errorE ∘ errorNondetCommute
  errorI ∷ NondetJoinT m ↝ ErrorT e (NondetJoinT m)
  errorI = nondetErrorCommute ∘ fmap errorI

instance (Functor m,MonadNondetJoin m) ⇒ MonadNondetJoin (ErrorT e m) where
  nondetJoinE ∷ NondetJoinT (ErrorT e m) ↝ ErrorT e m
  nondetJoinE = fmap nondetJoinE ∘ nondetErrorCommute
  nondetJoinI ∷ ErrorT e m ↝ NondetJoinT (ErrorT e m)
  nondetJoinI = errorNondetCommute ∘ fmap nondetJoinI

-- TODO: FlowAppendT

-- ## Error // Cont

-- TODO: 

-- ## Error // OpaqueCont

-- TODO: 

-- # Reader // *

-- ## Reader // Writer [ISO]

readerWriterCommute ∷ ReaderT r (WriterT o m) ↝ WriterT o (ReaderT r m)
readerWriterCommute aRWM = WriterT $ ReaderT $ \ r → runWriterT $ runReaderTWith r aRWM

writerReaderCommute ∷ WriterT o (ReaderT r m) ↝ ReaderT r (WriterT o m)
writerReaderCommute aWRM = ReaderT $ \ r → WriterT $ runReaderTWith r $ runWriterT aWRM

instance (Functor m,MonadReader r m) ⇒ MonadReader r (WriterT o m) where
  readerE ∷ ReaderT r (WriterT o m) ↝ WriterT o m
  readerE = fmap readerE ∘ readerWriterCommute
  readerI ∷ WriterT o m ↝ ReaderT r (WriterT o m)
  readerI = writerReaderCommute ∘ fmap readerI

instance (Functor m,MonadWriter o m) ⇒ MonadWriter o (ReaderT r m) where
  writerE ∷ WriterT o (ReaderT r m) ↝ ReaderT r m
  writerE = fmap writerE ∘ writerReaderCommute
  writerI ∷ ReaderT r m ↝ WriterT o (ReaderT r m)
  writerI = readerWriterCommute ∘ fmap writerI

-- ## Reader // State [ISO]

readerStateCommute ∷ (Functor m) ⇒ ReaderT r (StateT s m) ↝ StateT s (ReaderT r m)
readerStateCommute aRSM = StateT $ \ s → ReaderT $ \ r → runStateTWith s $ runReaderTWith r aRSM

stateReaderCommute ∷ (Functor m) ⇒ StateT s (ReaderT r m) ↝ ReaderT r (StateT s m)
stateReaderCommute aSRM = ReaderT $ \ r → StateT $ \ s → runReaderTWith r $ runStateTWith s aSRM

instance (Functor m,MonadReader r m) ⇒ MonadReader r (StateT s m) where
  readerE ∷ ReaderT r (StateT s m) ↝ StateT s m
  readerE = fmap readerE ∘ readerStateCommute
  readerI ∷ StateT s m ↝ ReaderT r (StateT s m)
  readerI = stateReaderCommute ∘ fmap readerI

instance (Functor m,MonadState s m) ⇒ MonadState s (ReaderT r m) where
  stateE ∷ StateT s (ReaderT r m) ↝ ReaderT r m
  stateE = fmap stateE ∘ stateReaderCommute
  stateI ∷ ReaderT r m ↝ StateT s (ReaderT r m)
  stateI = readerStateCommute ∘ fmap stateI

-- ## Reader // Nondet [ISO]

readerNondetAppendCommute ∷ (Functor m) ⇒ ReaderT r (NondetAppendT m) ↝ NondetAppendT (ReaderT r m)
readerNondetAppendCommute aM = NondetAppendT $ ReaderT $ \ r → runNondetAppendT $ runReaderTWith r aM

nondetAppendReaderCommute ∷ (Functor m) ⇒ NondetAppendT (ReaderT r m) ↝ ReaderT r (NondetAppendT m)
nondetAppendReaderCommute aM = ReaderT $ \ r → NondetAppendT $ runReaderTWith r $ runNondetAppendT aM

instance (Functor m,MonadReader r m) ⇒ MonadReader r (NondetAppendT m) where
  readerE ∷ ReaderT r (NondetAppendT m) ↝ NondetAppendT m
  readerE = fmap readerE ∘ readerNondetAppendCommute
  readerI ∷ NondetAppendT m ↝ ReaderT r (NondetAppendT m)
  readerI = nondetAppendReaderCommute ∘ fmap readerI

instance (Functor m,MonadNondetAppend m) ⇒ MonadNondetAppend (ReaderT r m) where
  nondetAppendE ∷ NondetAppendT (ReaderT r m) ↝ ReaderT r m
  nondetAppendE = fmap nondetAppendE ∘ nondetAppendReaderCommute
  nondetAppendI ∷ ReaderT r m ↝ NondetAppendT (ReaderT r m)
  nondetAppendI = readerNondetAppendCommute ∘ fmap nondetAppendI

readerNondetCommute ∷ (Functor m) ⇒ ReaderT r (NondetJoinT m) ↝ NondetJoinT (ReaderT r m)
readerNondetCommute aM = NondetJoinT $ ReaderT $ \ r → runNondetJoinT $ runReaderTWith r aM

nondetReaderCommute ∷ (Functor m) ⇒ NondetJoinT (ReaderT r m) ↝ ReaderT r (NondetJoinT m)
nondetReaderCommute aM = ReaderT $ \ r → NondetJoinT $ runReaderTWith r $ runNondetJoinT aM

instance (Functor m,MonadReader r m) ⇒ MonadReader r (NondetJoinT m) where
  readerE ∷ ReaderT r (NondetJoinT m) ↝ NondetJoinT m
  readerE = fmap readerE ∘ readerNondetCommute
  readerI ∷ NondetJoinT m ↝ ReaderT r (NondetJoinT m)
  readerI = nondetReaderCommute ∘ fmap readerI

instance (Functor m,MonadNondetJoin m) ⇒ MonadNondetJoin (ReaderT r m) where
  nondetJoinE ∷ NondetJoinT (ReaderT r m) ↝ ReaderT r m
  nondetJoinE = fmap nondetJoinE ∘ nondetReaderCommute
  nondetJoinI ∷ ReaderT r m ↝ NondetJoinT (ReaderT r m)
  nondetJoinI = readerNondetCommute ∘ fmap nondetJoinI

-- ## Reader // Flow [???]

readerFlowAppendCommute ∷ ∀ r s m. (Functor m) ⇒ ReaderT r (FlowAppendT s m) ↝ FlowAppendT s (ReaderT r m)
readerFlowAppendCommute xMM = FlowAppendT $ \ s → ReaderT $ \ r → runFlowAppendT (runReaderT xMM r) s

flowAppendReaderCommute ∷ ∀ s r m. (Functor m) ⇒ FlowAppendT s (ReaderT r m) ↝ ReaderT r (FlowAppendT s m)
flowAppendReaderCommute xMM = ReaderT $ \ r → FlowAppendT $ \ s → runReaderT (runFlowAppendT xMM s) r

instance (Functor m,MonadReader r m) ⇒ MonadReader r (FlowAppendT s m) where
  readerE ∷ ReaderT r (FlowAppendT s m) ↝ FlowAppendT s m
  readerE = fmap readerE ∘ readerFlowAppendCommute
  readerI ∷ FlowAppendT s m ↝ ReaderT r (FlowAppendT s m)
  readerI = flowAppendReaderCommute ∘ fmap readerI

instance (Functor m,MonadFlowAppend s m) ⇒ MonadFlowAppend s (ReaderT r m) where
  flowAppendE ∷ FlowAppendT s (ReaderT r m) ↝ ReaderT r m
  flowAppendE = fmap flowAppendE ∘ flowAppendReaderCommute
  flowAppendI ∷ ReaderT r m ↝ FlowAppendT s (ReaderT r m)
  flowAppendI = readerFlowAppendCommute ∘ fmap flowAppendI

readerFlowJoinCommute ∷ ∀ r s m. (Functor m) ⇒ ReaderT r (FlowJoinT s m) ↝ FlowJoinT s (ReaderT r m)
readerFlowJoinCommute xMM = FlowJoinT $ \ s → ReaderT $ \ r → runFlowJoinT (runReaderT xMM r) s

flowJoinReaderCommute ∷ ∀ s r m. (Functor m) ⇒ FlowJoinT s (ReaderT r m) ↝ ReaderT r (FlowJoinT s m)
flowJoinReaderCommute xMM = ReaderT $ \ r → FlowJoinT $ \ s → runReaderT (runFlowJoinT xMM s) r

instance (Functor m,MonadReader r m) ⇒ MonadReader r (FlowJoinT s m) where
  readerE ∷ ReaderT r (FlowJoinT s m) ↝ FlowJoinT s m
  readerE = fmap readerE ∘ readerFlowJoinCommute
  readerI ∷ FlowJoinT s m ↝ ReaderT r (FlowJoinT s m)
  readerI = flowJoinReaderCommute ∘ fmap readerI

instance (Functor m,MonadFlowJoin s m) ⇒ MonadFlowJoin s (ReaderT r m) where
  flowJoinE ∷ FlowJoinT s (ReaderT r m) ↝ ReaderT r m
  flowJoinE = fmap flowJoinE ∘ flowJoinReaderCommute
  flowJoinI ∷ ReaderT r m ↝ FlowJoinT s (ReaderT r m)
  flowJoinI = readerFlowJoinCommute ∘ fmap flowJoinI

-- ## Reader // Cont

-- TODO

-- ## Reader // OpaqueCont

-- TODO

-- # Writer // *

-- ## Writer // State [ISO]

writerStateCommute ∷ ∀ o s m. (Functor m) ⇒ WriterT o (StateT s m) ↝ StateT s (WriterT o m)
writerStateCommute aRMM = StateT $ \ s₁ → WriterT $ ff ^$ runStateTWith s₁ $ runWriterT aRMM
  where
    ff ∷ ((a,o),s) → ((a,s),o)
    ff ((a,o),s) = ((a,s),o)

stateWriterCommute ∷ ∀ o s m. (Functor m) ⇒ StateT s (WriterT o m) ↝ WriterT o (StateT s m)
stateWriterCommute aMRM = WriterT $ StateT $ ff ^∘ runWriterT ∘ runStateT aMRM
  where
    ff ∷ ((a,s),o) → ((a,o),s)
    ff ((a,s),o) = ((a,o),s)

instance (Functor m,MonadWriter o m) ⇒ MonadWriter o (StateT s m) where
  writerE ∷ WriterT o (StateT s m) ↝ StateT s m
  writerE = fmap writerE ∘ writerStateCommute
  writerI ∷ StateT s m ↝ WriterT o (StateT s m)
  writerI = stateWriterCommute ∘ fmap writerI

instance (Functor m,MonadState s m) ⇒ MonadState s (WriterT o m) where
  stateE ∷ StateT s (WriterT o m) ↝ WriterT o m
  stateE = fmap stateE ∘ stateWriterCommute
  stateI ∷ WriterT o m ↝ StateT s (WriterT o m)
  stateI = writerStateCommute ∘ fmap stateI

-- ## Writer // Nondet [ADJ]

writerNondetAppendCommute ∷ ∀ o m. (Functor m,Monoid o) ⇒ WriterT o (NondetAppendT m) ↝ NondetAppendT (WriterT o m)
writerNondetAppendCommute = NondetAppendT ∘ WriterT ∘ ff ^∘ runNondetAppendT ∘ runWriterT
  where
    ff ∷ [(a,o)] → ([a],o)
    ff asL = (fst ^$ asL,concat $ snd ^$ asL)

nondetAppendWriterCommute ∷ ∀ o m. (Functor m) ⇒ NondetAppendT (WriterT o m) ↝ WriterT o (NondetAppendT m)
nondetAppendWriterCommute = WriterT ∘ NondetAppendT ∘ ff ^∘ runWriterT ∘ runNondetAppendT
  where
    ff ∷ ([a],o) → [(a,o)]
    ff (xs,o) = (,o) ^$ xs

instance (Functor m,MonadWriter o m,Monoid o) ⇒ MonadWriter o (NondetAppendT m) where
  writerE ∷ WriterT o (NondetAppendT m) ↝ NondetAppendT m
  writerE = fmap writerE ∘ writerNondetAppendCommute
  writerI ∷ NondetAppendT m ↝ WriterT o (NondetAppendT m)
  writerI = nondetAppendWriterCommute ∘ fmap writerI

instance (Functor m,MonadNondetAppend m,Monoid o) ⇒ MonadNondetAppend (WriterT o m) where
  nondetAppendE ∷ NondetAppendT (WriterT o m) ↝ WriterT o m
  nondetAppendE = fmap nondetAppendE ∘ nondetAppendWriterCommute
  nondetAppendI ∷ WriterT o m ↝ NondetAppendT (WriterT o m)
  nondetAppendI = writerNondetAppendCommute ∘ fmap nondetAppendI

writerNondetJoinCommute ∷ ∀ o m. (Functor m,Monoid o) ⇒ WriterT o (NondetJoinT m) ↝ NondetJoinT (WriterT o m)
writerNondetJoinCommute = NondetJoinT ∘ WriterT ∘ (mapFst lazySet ∘ ff ∘ list) ^∘ runNondetJoinT ∘ runWriterT
  where
    ff ∷ [(a,o)] → ([a],o)
    ff asL = (fst ^$ asL,concat $ snd ^$ asL)

nondetJoinWriterCommute ∷ ∀ o m. (Functor m) ⇒ NondetJoinT (WriterT o m) ↝ WriterT o (NondetJoinT m)
nondetJoinWriterCommute = WriterT ∘ NondetJoinT ∘ (lazySet ∘ ff ∘ mapFst list) ^∘ runWriterT ∘ runNondetJoinT
  where
    ff ∷ ([a],o) → [(a,o)]
    ff (xs,o) = (,o) ^$ xs

instance (Functor m,MonadWriter o m,Monoid o) ⇒ MonadWriter o (NondetJoinT m) where
  writerE ∷ WriterT o (NondetJoinT m) ↝ NondetJoinT m
  writerE = fmap writerE ∘ writerNondetJoinCommute
  writerI ∷ NondetJoinT m ↝ WriterT o (NondetJoinT m)
  writerI = nondetJoinWriterCommute ∘ fmap writerI

instance (Functor m,MonadNondetJoin m,Monoid o) ⇒ MonadNondetJoin (WriterT o m) where
  nondetJoinE ∷ NondetJoinT (WriterT o m) ↝ WriterT o m
  nondetJoinE = fmap nondetJoinE ∘ nondetJoinWriterCommute
  nondetJoinI ∷ WriterT o m ↝ NondetJoinT (WriterT o m)
  nondetJoinI = writerNondetJoinCommute ∘ fmap nondetJoinI

-- TODO: FlowAppendT

-- ## Writer // Cont

-- TODO

-- ## Writer // OpaqeuCont

-- TODO

-- # State // *

mergeState ∷ (Functor m) ⇒ StateT s₁ (StateT s₂ m) a → StateT (s₁,s₂) m a
mergeState aMM = StateT $ \ (s₁,s₂) → ff ^$ runStateT (runStateT aMM s₁) s₂
  where
    ff ∷ ((a,s₁),s₂) → (a,(s₁,s₂))
    ff ((a,s₁),s₂) = (a,(s₁,s₂))

splitState ∷ (Functor m) ⇒ StateT (s₁,s₂) m a → StateT s₁ (StateT s₂ m) a
splitState aM = StateT $ \ s₁ → StateT $ \ s₂ → ff ^$ runStateT aM (s₁,s₂)
  where
    ff ∷ (a,(s₁,s₂)) → ((a,s₁),s₂)
    ff (a,(s₁,s₂)) = ((a,s₁),s₂)

mapState ∷ ∀ m s₁ s₂ a. (Functor m) ⇒ (s₁ ⇄ s₂) → StateT s₁ m a → StateT s₂ m a
mapState iso aM = StateT $ \ s₂ → ff ^$ runStateT aM $ isoFrom iso s₂
  where 
    ff ∷ (a,s₁) → (a,s₂)
    ff (a,s₁) = (a,isoTo iso s₁)

-- combineStateE ∷ (Functor m,MonadState s₂ (t m)) ⇒ s₃ ⇄ (s₁,s₂) → StateT s₃ (StateT s₁ m) ↝ (StateT s₁ m)
-- combineStateE iso = stateE ∘ fmap stateE ∘ splitState ∘ mapState iso

-- combineStateI ∷ (Functor m,MonadState s₁ m,MonadState s₂ m) ⇒ s₃ ⇄ (s₁,s₂) → m ↝ StateT s₃ m
-- combineStateI iso = mapState (sym iso) ∘ mergeState ∘ fmap stateI ∘ stateI

-- stateECombineFlowJoin 
--   ∷ (Functor m,MonadState s₁ m,MonadFlowJoin s₂ m) 
--   ⇒ (s₃ → (s₁,s₂)) 
--   → ((s₁,s₂) → s₃) 
--   → StateT s₃ m ↝ m
-- stateECombineFlowJoin to from = 
--   stateE 
--   ∘ fmap (flowJoinE ∘ flowFromStateJ) 
--   ∘ splitState 
--   ∘ mapStateT to from

-- ## State // Nondet [ADJ]

stateNondetAppendCommute ∷ ∀ s m. (Functor m,Monoid s) ⇒ StateT s (NondetAppendT m) ↝ NondetAppendT (StateT s m)
stateNondetAppendCommute aMM = NondetAppendT $ StateT $ \ s → ff ^$ runNondetAppendT $ runStateTWith s aMM
  where
    ff ∷ [(a,s)] → ([a],s)
    ff asL = (fst ^$ asL,concat $ snd ^$ asL)

nondetAppendStateCommute ∷ ∀ s m. (Functor m) ⇒ NondetAppendT (StateT s m) ↝ StateT s (NondetAppendT m)
nondetAppendStateCommute aMM = StateT $ \ s → NondetAppendT $ ff ^$ runStateTWith s $ runNondetAppendT aMM
  where
    ff ∷ ([a],s) → [(a,s)]
    ff (xs,s) = (,s) ^$ xs

instance (Functor m,MonadState s m,Monoid s) ⇒ MonadState s (NondetAppendT m) where
  stateE ∷ StateT s (NondetAppendT m) ↝ NondetAppendT m
  stateE = fmap stateE ∘ stateNondetAppendCommute
  stateI ∷ NondetAppendT m ↝ StateT s (NondetAppendT m)
  stateI = nondetAppendStateCommute ∘ fmap stateI

instance (Functor m,MonadNondetAppend m,Monoid s) ⇒ MonadNondetAppend (StateT s m) where
  nondetAppendE ∷ NondetAppendT (StateT s m) ↝ StateT s m
  nondetAppendE = fmap nondetAppendE ∘ nondetAppendStateCommute
  nondetAppendI ∷ StateT s m ↝ NondetAppendT (StateT s m)
  nondetAppendI = stateNondetAppendCommute ∘ fmap nondetAppendI

stateNondetJoinCommute ∷ ∀ s m. (Functor m,JoinLattice s) ⇒ StateT s (NondetJoinT m) ↝ NondetJoinT (StateT s m)
stateNondetJoinCommute aMM = NondetJoinT $ StateT $ \ s → (mapFst lazySet ∘ ff ∘ list) ^$ runNondetJoinT $ runStateTWith s aMM
  where
    ff ∷ [(a,s)] → ([a],s)
    ff asL = (fst ^$ asL,joins $ snd ^$ asL)

nondetJoinStateCommute ∷ ∀ s m. (Functor m) ⇒ NondetJoinT (StateT s m) ↝ StateT s (NondetJoinT m)
nondetJoinStateCommute aMM = StateT $ \ s → NondetJoinT $ (lazySet ∘ ff ∘ mapFst list) ^$ runStateTWith s $ runNondetJoinT aMM
  where
    ff ∷ ([a],s) → [(a,s)]
    ff (xs,s) = (,s) ^$ xs

instance (Functor m,MonadState s m,JoinLattice s) ⇒ MonadState s (NondetJoinT m) where
  stateE ∷ StateT s (NondetJoinT m) ↝ NondetJoinT m
  stateE = fmap stateE ∘ stateNondetJoinCommute
  stateI ∷ NondetJoinT m ↝ StateT s (NondetJoinT m)
  stateI = nondetJoinStateCommute ∘ fmap stateI

instance (Functor m,MonadNondetJoin m,JoinLattice s) ⇒ MonadNondetJoin (StateT s m) where
  nondetJoinE ∷ NondetJoinT (StateT s m) ↝ StateT s m
  nondetJoinE = fmap nondetJoinE ∘ nondetJoinStateCommute
  nondetJoinI ∷ StateT s m ↝ NondetJoinT (StateT s m)
  nondetJoinI = stateNondetJoinCommute ∘ fmap nondetJoinI

-- ## State // Flow [ADJ]

stateFlowAppendCommute ∷ ∀ s₁ s₂ m. (Functor m,Monoid s₁) ⇒ StateT s₁ (FlowAppendT s₂ m) ↝ FlowAppendT s₂ (StateT s₁ m)
stateFlowAppendCommute xMM = FlowAppendT $ \ s₂ → StateT $ \ s₁ → ff ^$ runFlowAppendT (runStateT xMM s₁) s₂
  where
    ff ∷ ((a,s₁) ⇰♭⧺ s₂) → (a ⇰♭⧺ s₂,s₁)
    ff xs₁s₂s =
      let ((xs,s₁s),s₂s) = mapFst unzip $ unzip $ list xs₁s₂s
      in (lazyDictAppend $ zipAssumeSameLength xs s₂s,concat s₁s)

flowAppendStateCommute ∷ ∀ s₁ s₂ m. (Functor m,Monoid s₁) ⇒ FlowAppendT s₁ (StateT s₂ m) ↝ StateT s₂ (FlowAppendT s₁ m)
flowAppendStateCommute xMM = StateT $ \ s₂ → FlowAppendT $ \ s₁ → ff ^$ runStateT (runFlowAppendT xMM s₁) s₂
  where
    ff ∷ (a ⇰♭⧺ s₁,s₂) → ((a,s₂) ⇰♭⧺ s₁)
    ff (xs₁s,s₂) = lazyDictAppend $ map (mapFst (,s₂)) $ list xs₁s

-- instance (Functor m,MonadState s m,Monoid s,Monoid s') ⇒ MonadState s (FlowAppendT s' m) where
--   stateE ∷ StateT s (FlowAppendT s' m) ↝ FlowAppendT s' m
--   stateE = fmap stateE ∘ stateFlowAppendCommute
--   stateI ∷ FlowAppendT s' m ↝ StateT s (FlowAppendT s' m)
--   stateI = flowAppendStateCommute ∘ fmap stateI
-- 
-- instance (Functor m,MonadFlowAppend s m,Monoid s,Monoid s') ⇒ MonadFlowAppend s (StateT s' m) where
--   flowAppendE ∷ FlowAppendT s (StateT s' m) ↝ StateT s' m
--   flowAppendE = fmap flowAppendE ∘ flowAppendStateCommute
--   flowAppendI ∷ StateT s' m ↝ FlowAppendT s (StateT s' m)
--   flowAppendI = stateFlowAppendCommute ∘ fmap flowAppendI

stateFlowJoinCommute ∷ ∀ s₁ s₂ m. (Functor m,JoinLattice s₁) ⇒ StateT s₁ (FlowJoinT s₂ m) ↝ FlowJoinT s₂ (StateT s₁ m)
stateFlowJoinCommute xMM = FlowJoinT $ \ s₂ → StateT $ \ s₁ → ff ^$ runFlowJoinT (runStateT xMM s₁) s₂
  where
    ff ∷ ((a,s₁) ⇰♭⊔ s₂) → (a ⇰♭⊔ s₂,s₁)
    ff xs₁s₂s =
      let ((xs,s₁s),s₂s) = mapFst unzip $ unzip $ list $ runLazyDictJoin xs₁s₂s
      in (lazyDictJoin $ zipAssumeSameLength xs s₂s,joins s₁s)

flowJoinStateCommute ∷ ∀ s₁ s₂ m. (Functor m,JoinLattice s₁) ⇒ FlowJoinT s₁ (StateT s₂ m) ↝ StateT s₂ (FlowJoinT s₁ m)
flowJoinStateCommute xMM = StateT $ \ s₂ → FlowJoinT $ \ s₁ → ff ^$ runStateT (runFlowJoinT xMM s₁) s₂
  where
    ff ∷ (a ⇰♭⊔ s₁,s₂) → ((a,s₂) ⇰♭⊔ s₁)
    ff (xs₁s,s₂) = lazyDictJoin $ map (mapFst (,s₂)) $ list xs₁s

-- instance (Functor m,MonadState s m,JoinLattice s,JoinLattice s') ⇒ MonadState s (FlowJoinT s' m) where
--   stateE ∷ StateT s (FlowJoinT s' m) ↝ FlowJoinT s' m
--   stateE = fmap stateE ∘ stateFlowJoinCommute
--   stateI ∷ FlowJoinT s' m ↝ StateT s (FlowJoinT s' m)
--   stateI = flowJoinStateCommute ∘ fmap stateI
-- 
-- instance (Functor m,MonadFlowJoin s m,JoinLattice s,JoinLattice s') ⇒ MonadFlowJoin s (StateT s' m) where
--   flowJoinE ∷ FlowJoinT s (StateT s' m) ↝ StateT s' m
--   flowJoinE = fmap flowJoinE ∘ flowJoinStateCommute
--   flowJoinI ∷ StateT s' m ↝ FlowJoinT s (StateT s' m)
--   flowJoinI = stateFlowJoinCommute ∘ fmap flowJoinI

-- ## State // Cont [???]

stateKonCommute ∷ StateT s (ContT (r,s) m) ↝ ContT r (StateT s m)
stateKonCommute aSK = ContT $ \ (k ∷ a → StateT s m r) → StateT $ \ s →
  runContT (runStateTWith s aSK) $ \ (a,s') → runStateTWith s' $ k a

konStateCommute ∷ ContT r (StateT s m) ↝ StateT s (ContT (r,s) m)
konStateCommute aKS = StateT $ \ s → ContT $ \ (k ∷ (a,s) → m (r,s)) →
  runStateTWith s $ runContT aKS $ \ a → StateT $ \ s' → k (a,s')

instance (Monad m,MonadState s m) ⇒ MonadState s (ContT r m) where
  stateE ∷ StateT s (ContT r m) ↝ ContT r m
  stateE =
    fisomap (stateE,stateI)
    ∘ stateKonCommute
    ∘ stateE
    ∘ fmap (konStateCommute ∘ fisomap (stateI,stateE ∷ StateT s m ↝ m))
  stateI ∷ ContT r m ↝ StateT s (ContT r m)
  stateI =
    fmap (fisomap (stateE,stateI) ∘ stateKonCommute)
    ∘ stateI
    ∘ konStateCommute
    ∘ fisomap (stateI,stateE ∷ StateT s m ↝ m)

-- # State // OpaqueCont [???]

instance (Monad m,MonadState s m,Isomorphic3 (ContFun r) (k r)) ⇒ MonadState s (OpaqueContT k r m) where
  stateE ∷ StateT s (OpaqueContT k r m) ↝ OpaqueContT k r m
  stateE =
    opaque
    ∘ stateE
    ∘ fmap meta
  stateI ∷ OpaqueContT k r m ↝ StateT s (OpaqueContT k r m)
  stateI =
    fmap opaque
    ∘ stateI
    ∘ meta

---------
-- RWS --
---------

newtype RWST r o s m a = RWST { runRWST ∷ ReaderT r (WriterT o (StateT s m)) a }
  deriving
  ( Functor,Monad
  , MonadFailure
  , MonadError e
  , MonadReader r
  , MonadWriter o
  , MonadState s
  )
runRWSTWith ∷ ∀ r o s m a. (Functor m) ⇒ r → s → RWST r o s m a → m (a,o,s)
runRWSTWith r s₀ aM = ff ^$ runStateTWith s₀ $ runWriterT $ runReaderTWith r $ runRWST aM 
  where
    ff ∷ ((a,o),s) → (a,o,s)
    ff ((a,o),s) = (a,o,s)

-- Base Effect

type RWS r o s = RWST r o s ID

runRWSWith ∷ r → s → RWS r o s a → (a,o,s)
runRWSWith r s aM = runID $ runRWSTWith r s aM

-- Higher Functor

instance FunctorFunctor (RWST r o s) where
  fmap ∷ (m ↝ n) → RWST r o s m a → RWST r o s n a
  fmap f = RWST ∘ fmap (fmap (fmap f)) ∘ runRWST

-- --------------------
-- -- Adding Effects --
-- --------------------
-- 
-- -- # AddWriterT
-- 
-- newtype AddWriterT o₁₂ o₁ m a = AddWriterT { runAddWriterT ∷ WriterT o₁ m a }
--   deriving 
--     ( Functor,Monad
--     , MonadMonoid,MonadBot,MonadJoin
--     , MonadFailure
--     , MonadError e
--     , MonadReader r
--     , MonadState s
--     -- TODO: implement 
--     -- , MonadCont r
--     -- TODO: implement and role annotation
--     -- , MonadOpaqueCont k r
--     )
-- 
-- mergeWriter ∷ (Functor m) ⇒ WriterT o₁ (WriterT o₂ m) a → WriterT (o₁,o₂) m a
-- mergeWriter = WriterT ∘ ff ^∘ runWriterT ∘ runWriterT
--   where
--     ff ∷ ((a,o₁),o₂) → (a,(o₁,o₂))
--     ff ((a,o₁),o₂) = (a,(o₁,o₂))
-- 
-- splitWriter ∷ (Functor m) ⇒ WriterT (o₁,o₂) m a → WriterT o₁ (WriterT o₂ m) a
-- splitWriter = WriterT ∘ WriterT ∘ ff ^∘ runWriterT
--   where
--     ff ∷ (a,(o₁,o₂)) → ((a,o₁),o₂)
--     ff (a,(o₁,o₂)) = ((a,o₁),o₂)
-- 
-- instance (Functor m,MonadWriter o₂ m,Monoid o₁,Isomorphism o₁₂ (o₁,o₂)) ⇒ MonadWriter o₁₂ (AddWriterT o₁₂ o₁ m) where
--   writerI ∷ AddWriterT o₁₂ o₁ m ↝ WriterT o₁₂ (AddWriterT o₁₂ o₁ m)
--   writerI = 
--     fmap AddWriterT
--     ∘ mapOutput isoFrom
--     ∘ mergeWriter
--     ∘ fmap (writerCommute ∘ fmap writerI)
--     ∘ writerI
--     ∘ runAddWriterT
--   writerE ∷ WriterT o₁₂ (AddWriterT o₁₂ o₁ m) ↝ AddWriterT o₁₂ o₁ m
--   writerE = 
--     AddWriterT
--     ∘ writerE
--     ∘ fmap (fmap writerE ∘ writerCommute) 
--     ∘ splitWriter
--     ∘ mapOutput isoTo
--     ∘ fmap runAddWriterT
-- 
-- -- # AddStateT
-- 
-- newtype AddStateT s₁₂ s₁ m a = AddStateT { runAddStateT ∷ StateT s₁ m a }
--   deriving 
--     ( Functor,Monad
--     , MonadMonoid,MonadBot,MonadJoin
--     , MonadFailure
--     , MonadError e
--     , MonadReader r
--     , MonadWriter o
--     -- TODO: implement
--     -- , MonadCont r
--     -- TODO: implement
--     -- , MonadOpaqueCont k r
--     )
-- 
-- instance (Functor m,MonadState s₂ m,Isomorphism s₁₂ (s₁,s₂)) ⇒ MonadState s₁₂ (AddStateT s₁₂ s₁ m) where
--   stateI ∷ AddStateT s₁₂ s₁ m ↝ StateT s₁₂ (AddStateT s₁₂ s₁ m)
--   stateI = 
--     fmap AddStateT
--     ∘ mapStateT isoFrom isoTo
--     ∘ mergeState
--     ∘ fmap (stateCommute ∘ fmap stateI)
--     ∘ stateI
--     ∘ runAddStateT
--   stateE ∷ StateT s₁₂ (AddStateT s₁₂ s₁ m) ↝ AddStateT s₁₂ s₁ m
--   stateE = 
--     AddStateT
--     ∘ stateE
--     ∘ fmap (fmap stateE ∘ stateCommute) 
--     ∘ splitState
--     ∘ mapStateT isoTo isoFrom
--     ∘ fmap runAddStateT