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
class FunctorUnit (t ∷ (★ → ★) → (★ → ★)) where funit ∷ (Functor m) ⇒ m ↝ t m
class FunctorDiscard (t ∷ (★ → ★) → (★ → ★)) where fdiscard ∷ (Functor m) ⇒ t (t m) ↝ t m
class FunctorFunctor (t ∷ (★ → ★) → (★ → ★)) where fmap ∷ m ↝ n → t m ↝ t n
class FunctorIsoFunctor (t ∷ (★ → ★) → (★ → ★)) where fisomap ∷ (m ↝ n,n ↝ m) → (t m ↝ t n)
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
type Failure = FailureT ID
failure ∷ Maybe a → Failure a
failure = abortMaybe
runFailure ∷ Failure a → Maybe a
runFailure = runID ∘ runFailureT
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)
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
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
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)
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
instance MonadFailure Maybe where
failureE ∷ FailureT Maybe ↝ Maybe
failureE = runFailure ∘ failureE ∘ fmap failure
failureI ∷ Maybe ↝ FailureT Maybe
failureI = fmap runFailure ∘ failureI ∘ failure
type Error e = ErrorT e ID
runError ∷ Error e a → e ⨄ a
runError = runID ∘ runErrorT
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
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
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
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₂
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
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
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
readerCommute ∷ ReaderT r₁ (ReaderT r₂ m) ↝ ReaderT r₂ (ReaderT r₁ m)
readerCommute aMM = ReaderT $ \ r₂ → ReaderT $ \ r₁ → runReaderTWith r₂ $ runReaderTWith r₁ aMM
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
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
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)
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
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
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
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₁)
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')
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
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)
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
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
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
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
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₁)
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'
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
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
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
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
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
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
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
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
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 (<⊔>) = (⊔)
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
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)
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'
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
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)
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
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
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
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
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
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)
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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₁)
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
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
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
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)
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
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)
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
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