module UVMHS.Core.Transformers where

import UVMHS.Core.Init
import UVMHS.Core.Classes
import UVMHS.Core.Data

import UVMHS.Core.Effects

import qualified Prelude as HS

-------------
-- COMPOSE --
-------------

infixl 7 ⊡

newtype (⊡) (t₁ ∷ (★ → ★) → (★ → ★)) (t₂ ∷ (★ → ★) → (★ → ★)) m a = Compose2 { forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 ∷ t₁ (t₂ m) a }

instance (∀ m'. Monad m' ⇒ Monad (t₁ m'),∀ m'. Monad m' ⇒ Monad (t₂ m'),Monad m) ⇒ Functor ((t₁ ⊡ t₂) m) where 
  map :: forall a b. (a -> b) -> (⊡) t₁ t₂ m a -> (⊡) t₁ t₂ m b
map = (a -> b) -> (⊡) t₁ t₂ m a -> (⊡) t₁ t₂ m b
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
mmap
instance (∀ m'. Monad m' ⇒ Monad (t₁ m'),∀ m'. Monad m' ⇒ Monad (t₂ m'),Monad m) ⇒ Return ((t₁ ⊡ t₂) m) where
  return ∷ ∀ a. a → (t₁ ⊡ t₂) m a
  return :: forall a. a -> (⊡) t₁ t₂ m a
return a
x = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall a b. (a -> b) -> a -> b
$ a -> t₁ (t₂ m) a
forall a. a -> t₁ (t₂ m) a
forall (m :: * -> *) a. Return m => a -> m a
return a
x
instance (∀ m'. Monad m' ⇒ Monad (t₁ m'),∀ m'. Monad m' ⇒ Monad (t₂ m'),Monad m) ⇒ Bind ((t₁ ⊡ t₂) m) where
  (≫=) ∷ ∀ a b. (t₁ ⊡ t₂) m a → (a → (t₁ ⊡ t₂) m b) → (t₁ ⊡ t₂) m b
  (⊡) t₁ t₂ m a
xM ≫= :: forall a b. (⊡) t₁ t₂ m a -> (a -> (⊡) t₁ t₂ m b) -> (⊡) t₁ t₂ m b
≫= a -> (⊡) t₁ t₂ m b
k = t₁ (t₂ m) b -> (⊡) t₁ t₂ m b
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) b -> (⊡) t₁ t₂ m b) -> t₁ (t₂ m) b -> (⊡) t₁ t₂ m b
forall a b. (a -> b) -> a -> b
$ do
    a
x ← (⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 (⊡) t₁ t₂ m a
xM
    (⊡) t₁ t₂ m b -> t₁ (t₂ m) b
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 ((⊡) t₁ t₂ m b -> t₁ (t₂ m) b) -> (⊡) t₁ t₂ m b -> t₁ (t₂ m) b
forall a b. (a -> b) -> a -> b
$ a -> (⊡) t₁ t₂ m b
k a
x
instance (∀ m'. Monad m' ⇒ Monad (t₁ m'),∀ m'. Monad m' ⇒ Monad (t₂ m'),Monad m) ⇒ Monad ((t₁ ⊡ t₂) m)

instance (Functor2 t₁,Functor2 t₂) ⇒ Functor2 (t₁ ⊡ t₂) where
  map2 ∷ ∀ m₁ m₂. (∀ a. m₁ a → m₂ a) → (∀ a. (t₁ ⊡ t₂) m₁ a → (t₁ ⊡ t₂) m₂ a)
  map2 :: forall (t :: * -> *) (u :: * -> *).
(t →⁻ u) -> (⊡) t₁ t₂ t →⁻ (⊡) t₁ t₂ u
map2 forall a. m₁ a -> m₂ a
f = t₁ (t₂ m₂) a -> (⊡) t₁ t₂ m₂ a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m₂) a -> (⊡) t₁ t₂ m₂ a)
-> (t₁ (t₂ m₁) a -> t₁ (t₂ m₂) a) -> t₁ (t₂ m₁) a -> (⊡) t₁ t₂ m₂ a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (t₂ m₁ →⁻ t₂ m₂) -> t₁ (t₂ m₁) →⁻ t₁ (t₂ m₂)
forall (t :: * -> *) (u :: * -> *). (t →⁻ u) -> t₁ t →⁻ t₁ u
forall (w :: (* -> *) -> * -> *) (t :: * -> *) (u :: * -> *).
Functor2 w =>
(t →⁻ u) -> w t →⁻ w u
map2 ((forall a. m₁ a -> m₂ a) -> t₂ m₁ →⁻ t₂ m₂
forall (t :: * -> *) (u :: * -> *). (t →⁻ u) -> t₂ t →⁻ t₂ u
forall (w :: (* -> *) -> * -> *) (t :: * -> *) (u :: * -> *).
Functor2 w =>
(t →⁻ u) -> w t →⁻ w u
map2 m₁ a -> m₂ a
forall a. m₁ a -> m₂ a
f) (t₁ (t₂ m₁) a -> (⊡) t₁ t₂ m₂ a)
-> ((⊡) t₁ t₂ m₁ a -> t₁ (t₂ m₁) a)
-> (⊡) t₁ t₂ m₁ a
-> (⊡) t₁ t₂ m₂ a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (⊡) t₁ t₂ m₁ a -> t₁ (t₂ m₁) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2

instance (∀ m'. Monad m' ⇒ Monad (t₂ m'),LiftIO t₁,LiftIO t₂) ⇒ LiftIO (t₁ ⊡ t₂) where
  liftIO ∷ ∀ m. (Monad m) ⇒ (∀ a. IO a → m a) → (∀ a. IO a → (t₁ ⊡ t₂) m a)
  liftIO :: forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> forall a. IO a -> (⊡) t₁ t₂ m a
liftIO forall a. IO a -> m a
ioM IO a
xM = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall a b. (a -> b) -> a -> b
$ (forall a. IO a -> t₂ m a) -> forall a. IO a -> t₁ (t₂ m) a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> forall a. IO a -> t₁ m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *).
(LiftIO t, Monad m) =>
(forall a. IO a -> m a) -> forall a. IO a -> t m a
liftIO ((forall a. IO a -> m a) -> forall a. IO a -> t₂ m a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> forall a. IO a -> t₂ m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *).
(LiftIO t, Monad m) =>
(forall a. IO a -> m a) -> forall a. IO a -> t m a
liftIO IO a -> m a
forall a. IO a -> m a
ioM) IO a
xM

instance (∀ m'. Monad m' ⇒ Monad (t₂ m'),LiftReader t₁,LiftReader t₂) ⇒ LiftReader (t₁ ⊡ t₂) where
  liftAskL ∷ ∀ m r. (Monad m) ⇒ (∀ r'. r ⟢ r' → m r') → ∀ r'. r ⟢ r' → (t₁ ⊡ t₂) m r'
  liftAskL :: forall (m :: * -> *) r.
Monad m =>
(forall r'. (r ⟢ r') -> m r')
-> forall r'. (r ⟢ r') -> (⊡) t₁ t₂ m r'
liftAskL forall r'. (r ⟢ r') -> m r'
askLM = t₁ (t₂ m) r' -> (⊡) t₁ t₂ m r'
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) r' -> (⊡) t₁ t₂ m r')
-> ((r ⟢ r') -> t₁ (t₂ m) r') -> (r ⟢ r') -> (⊡) t₁ t₂ m r'
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (forall r'. (r ⟢ r') -> t₂ m r')
-> forall r'. (r ⟢ r') -> t₁ (t₂ m) r'
forall (m :: * -> *) r.
Monad m =>
(forall r'. (r ⟢ r') -> m r') -> forall r'. (r ⟢ r') -> t₁ m r'
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftReader t, Monad m) =>
(forall r'. (r ⟢ r') -> m r') -> forall r'. (r ⟢ r') -> t m r'
liftAskL ((forall r'. (r ⟢ r') -> m r') -> forall r'. (r ⟢ r') -> t₂ m r'
forall (m :: * -> *) r.
Monad m =>
(forall r'. (r ⟢ r') -> m r') -> forall r'. (r ⟢ r') -> t₂ m r'
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftReader t, Monad m) =>
(forall r'. (r ⟢ r') -> m r') -> forall r'. (r ⟢ r') -> t m r'
liftAskL (r ⟢ r') -> m r'
forall r'. (r ⟢ r') -> m r'
askLM)

  liftLocalL ∷ ∀ m r. (Monad m) ⇒ (∀ r' a. r ⟢ r' → r' → m a → m a) → (∀ r' a. r ⟢ r' → r' → (t₁ ⊡ t₂) m a → (t₁ ⊡ t₂) m a)
  liftLocalL :: forall (m :: * -> *) r.
Monad m =>
(forall r' a. (r ⟢ r') -> r' -> m a -> m a)
-> forall r' a. (r ⟢ r') -> r' -> (⊡) t₁ t₂ m a -> (⊡) t₁ t₂ m a
liftLocalL forall r' a. (r ⟢ r') -> r' -> m a -> m a
localLM r ⟢ r'
ℓ r'
r = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a)
-> (t₁ (t₂ m) a -> t₁ (t₂ m) a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((forall r' a. (r ⟢ r') -> r' -> t₂ m a -> t₂ m a)
-> forall r' a. (r ⟢ r') -> r' -> t₁ (t₂ m) a -> t₁ (t₂ m) a
forall (m :: * -> *) r.
Monad m =>
(forall r' a. (r ⟢ r') -> r' -> m a -> m a)
-> forall r' a. (r ⟢ r') -> r' -> t₁ m a -> t₁ m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftReader t, Monad m) =>
(forall r' a. (r ⟢ r') -> r' -> m a -> m a)
-> forall r' a. (r ⟢ r') -> r' -> t m a -> t m a
liftLocalL ((forall r' a. (r ⟢ r') -> r' -> t₂ m a -> t₂ m a)
 -> forall r' a. (r ⟢ r') -> r' -> t₁ (t₂ m) a -> t₁ (t₂ m) a)
-> (forall r' a. (r ⟢ r') -> r' -> t₂ m a -> t₂ m a)
-> forall r' a. (r ⟢ r') -> r' -> t₁ (t₂ m) a -> t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
HS.$ (forall r' a. (r ⟢ r') -> r' -> m a -> m a)
-> forall r' a. (r ⟢ r') -> r' -> t₂ m a -> t₂ m a
forall (m :: * -> *) r.
Monad m =>
(forall r' a. (r ⟢ r') -> r' -> m a -> m a)
-> forall r' a. (r ⟢ r') -> r' -> t₂ m a -> t₂ m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftReader t, Monad m) =>
(forall r' a. (r ⟢ r') -> r' -> m a -> m a)
-> forall r' a. (r ⟢ r') -> r' -> t m a -> t m a
liftLocalL (r ⟢ r') -> r' -> m a -> m a
forall r' a. (r ⟢ r') -> r' -> m a -> m a
localLM) r ⟢ r'
ℓ r'
r (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a)
-> ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a) -> (⊡) t₁ t₂ m a -> (⊡) t₁ t₂ m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2

instance (∀ m'. Monad m' ⇒ Monad (t₂ m'),LiftWriter t₁,LiftWriter t₂) ⇒ LiftWriter (t₁ ⊡ t₂) where
  liftTell ∷ ∀ m o. (Monad m) ⇒ (o → m ()) → (o → (t₁ ⊡ t₂) m ())
  liftTell :: forall (m :: * -> *) o.
Monad m =>
(o -> m ()) -> o -> (⊡) t₁ t₂ m ()
liftTell o -> m ()
tellM = t₁ (t₂ m) () -> (⊡) t₁ t₂ m ()
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) () -> (⊡) t₁ t₂ m ())
-> (o -> t₁ (t₂ m) ()) -> o -> (⊡) t₁ t₂ m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((o -> t₂ m ()) -> o -> t₁ (t₂ m) ()
forall (m :: * -> *) o. Monad m => (o -> m ()) -> o -> t₁ m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) o.
(LiftWriter t, Monad m) =>
(o -> m ()) -> o -> t m ()
liftTell ((o -> t₂ m ()) -> o -> t₁ (t₂ m) ())
-> (o -> t₂ m ()) -> o -> t₁ (t₂ m) ()
forall a b. (a -> b) -> a -> b
$ (o -> m ()) -> o -> t₂ m ()
forall (m :: * -> *) o. Monad m => (o -> m ()) -> o -> t₂ m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) o.
(LiftWriter t, Monad m) =>
(o -> m ()) -> o -> t m ()
liftTell o -> m ()
tellM)

  liftHijack ∷ ∀ m o. (Monad m) ⇒ (∀ a. m a → m (o ∧ a)) → (∀ a. (t₁ ⊡ t₂) m a → (t₁ ⊡ t₂) m (o ∧ a))
  liftHijack :: forall (m :: * -> *) o.
Monad m =>
(forall a. m a -> m (o ∧ a))
-> forall a. (⊡) t₁ t₂ m a -> (⊡) t₁ t₂ m (o ∧ a)
liftHijack forall a. m a -> m (o ∧ a)
hijackM = t₁ (t₂ m) (o ∧ a) -> (⊡) t₁ t₂ m (o ∧ a)
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) (o ∧ a) -> (⊡) t₁ t₂ m (o ∧ a))
-> (t₁ (t₂ m) a -> t₁ (t₂ m) (o ∧ a))
-> t₁ (t₂ m) a
-> (⊡) t₁ t₂ m (o ∧ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((forall a. t₂ m a -> t₂ m (o ∧ a))
-> forall a. t₁ (t₂ m) a -> t₁ (t₂ m) (o ∧ a)
forall (m :: * -> *) o.
Monad m =>
(forall a. m a -> m (o ∧ a)) -> forall a. t₁ m a -> t₁ m (o ∧ a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) o.
(LiftWriter t, Monad m) =>
(forall a. m a -> m (o ∧ a)) -> forall a. t m a -> t m (o ∧ a)
liftHijack ((forall a. t₂ m a -> t₂ m (o ∧ a))
 -> forall a. t₁ (t₂ m) a -> t₁ (t₂ m) (o ∧ a))
-> (forall a. t₂ m a -> t₂ m (o ∧ a))
-> forall a. t₁ (t₂ m) a -> t₁ (t₂ m) (o ∧ a)
forall a b. (a -> b) -> a -> b
HS.$ (forall a. m a -> m (o ∧ a)) -> forall a. t₂ m a -> t₂ m (o ∧ a)
forall (m :: * -> *) o.
Monad m =>
(forall a. m a -> m (o ∧ a)) -> forall a. t₂ m a -> t₂ m (o ∧ a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) o.
(LiftWriter t, Monad m) =>
(forall a. m a -> m (o ∧ a)) -> forall a. t m a -> t m (o ∧ a)
liftHijack m a -> m (o ∧ a)
forall a. m a -> m (o ∧ a)
hijackM) (t₁ (t₂ m) a -> (⊡) t₁ t₂ m (o ∧ a))
-> ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a)
-> (⊡) t₁ t₂ m a
-> (⊡) t₁ t₂ m (o ∧ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2

instance (∀ m'. Monad m' ⇒ Monad (t₂ m'),LiftState t₁,LiftState t₂) ⇒ LiftState (t₁ ⊡ t₂) where
  liftGet ∷ ∀ m s. (Monad m) ⇒ m s → (t₁ ⊡ t₂) m s
  liftGet :: forall (m :: * -> *) s. Monad m => m s -> (⊡) t₁ t₂ m s
liftGet m s
getM = t₁ (t₂ m) s -> (⊡) t₁ t₂ m s
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) s -> (⊡) t₁ t₂ m s) -> t₁ (t₂ m) s -> (⊡) t₁ t₂ m s
forall a b. (a -> b) -> a -> b
$ t₂ m s -> t₁ (t₂ m) s
forall (m :: * -> *) s. Monad m => m s -> t₁ m s
forall (t :: (* -> *) -> * -> *) (m :: * -> *) s.
(LiftState t, Monad m) =>
m s -> t m s
liftGet (t₂ m s -> t₁ (t₂ m) s) -> t₂ m s -> t₁ (t₂ m) s
forall a b. (a -> b) -> a -> b
$ m s -> t₂ m s
forall (m :: * -> *) s. Monad m => m s -> t₂ m s
forall (t :: (* -> *) -> * -> *) (m :: * -> *) s.
(LiftState t, Monad m) =>
m s -> t m s
liftGet m s
getM

  liftPut ∷ ∀ m s. (Monad m) ⇒ (s → m ()) → (s → (t₁ ⊡ t₂) m ())
  liftPut :: forall (m :: * -> *) s.
Monad m =>
(s -> m ()) -> s -> (⊡) t₁ t₂ m ()
liftPut s -> m ()
putM = t₁ (t₂ m) () -> (⊡) t₁ t₂ m ()
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) () -> (⊡) t₁ t₂ m ())
-> (s -> t₁ (t₂ m) ()) -> s -> (⊡) t₁ t₂ m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s -> t₂ m ()) -> s -> t₁ (t₂ m) ()
forall (m :: * -> *) s. Monad m => (s -> m ()) -> s -> t₁ m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) s.
(LiftState t, Monad m) =>
(s -> m ()) -> s -> t m ()
liftPut ((s -> t₂ m ()) -> s -> t₁ (t₂ m) ())
-> (s -> t₂ m ()) -> s -> t₁ (t₂ m) ()
forall a b. (a -> b) -> a -> b
$ (s -> m ()) -> s -> t₂ m ()
forall (m :: * -> *) s. Monad m => (s -> m ()) -> s -> t₂ m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) s.
(LiftState t, Monad m) =>
(s -> m ()) -> s -> t m ()
liftPut s -> m ()
putM)

instance (∀ m'. Monad m' ⇒ Monad (t₂ m'),LiftFail t₁,LiftFail t₂) ⇒ LiftFail (t₁ ⊡ t₂) where
  liftAbort ∷ ∀ m. (Monad m) ⇒ (∀ a. m a) → (∀ a. (t₁ ⊡ t₂) m a)
  liftAbort :: forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. (⊡) t₁ t₂ m a
liftAbort forall a. m a
abortM = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall a b. (a -> b) -> a -> b
$ (forall a. t₂ m a) -> forall a. t₁ (t₂ m) a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftFail t, Monad m) =>
(forall a. m a) -> forall (a :: k). t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. t₁ m a
liftAbort ((forall a. t₂ m a) -> forall a. t₁ (t₂ m) a)
-> (forall a. t₂ m a) -> forall a. t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
HS.$ (forall a. m a) -> forall a. t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftFail t, Monad m) =>
(forall a. m a) -> forall (a :: k). t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. t₂ m a
liftAbort m a
forall a. m a
abortM

  liftTry ∷ ∀ m. (Monad m) ⇒ (∀ a. m a → m a → m a) → (∀ a. (t₁ ⊡ t₂) m a → (t₁ ⊡ t₂) m a → (t₁ ⊡ t₂) m a)
  liftTry :: forall (m :: * -> *).
Monad m =>
(forall a. m a -> m a -> m a)
-> forall a. (⊡) t₁ t₂ m a -> (⊡) t₁ t₂ m a -> (⊡) t₁ t₂ m a
liftTry forall a. m a -> m a -> m a
tryM (⊡) t₁ t₂ m a
xM₁ (⊡) t₁ t₂ m a
xM₂ = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall a b. (a -> b) -> a -> b
$ ((forall a. t₂ m a -> t₂ m a -> t₂ m a)
-> forall a. t₁ (t₂ m) a -> t₁ (t₂ m) a -> t₁ (t₂ m) a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftFail t, Monad m) =>
(forall a. m a -> m a -> m a)
-> forall (a :: k). t m a -> t m a -> t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a -> m a -> m a)
-> forall a. t₁ m a -> t₁ m a -> t₁ m a
liftTry ((forall a. t₂ m a -> t₂ m a -> t₂ m a)
 -> forall a. t₁ (t₂ m) a -> t₁ (t₂ m) a -> t₁ (t₂ m) a)
-> (forall a. t₂ m a -> t₂ m a -> t₂ m a)
-> forall a. t₁ (t₂ m) a -> t₁ (t₂ m) a -> t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
HS.$ (forall a. m a -> m a -> m a)
-> forall a. t₂ m a -> t₂ m a -> t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftFail t, Monad m) =>
(forall a. m a -> m a -> m a)
-> forall (a :: k). t m a -> t m a -> t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a -> m a -> m a)
-> forall a. t₂ m a -> t₂ m a -> t₂ m a
liftTry m a -> m a -> m a
forall a. m a -> m a -> m a
tryM) ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 (⊡) t₁ t₂ m a
xM₁) ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 (⊡) t₁ t₂ m a
xM₂)

instance (∀ m'. Monad m' ⇒ Monad (t₂ m'),LiftError t₁,LiftError t₂) ⇒ LiftError (t₁ ⊡ t₂) where
  liftThrow ∷ ∀ m e. (Monad m) ⇒ (∀ a. e → m a) → (∀ a. e → (t₁ ⊡ t₂) m a)
  liftThrow :: forall (m :: * -> *) e.
Monad m =>
(forall a. e -> m a) -> forall a. e -> (⊡) t₁ t₂ m a
liftThrow forall a. e -> m a
throwM = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a)
-> (e -> t₁ (t₂ m) a) -> e -> (⊡) t₁ t₂ m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((forall a. e -> t₂ m a) -> forall a. e -> t₁ (t₂ m) a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *) e.
(LiftError t, Monad m) =>
(forall a. e -> m a) -> forall (a :: k). e -> t m a
forall (m :: * -> *) e.
Monad m =>
(forall a. e -> m a) -> forall a. e -> t₁ m a
liftThrow ((forall a. e -> t₂ m a) -> forall a. e -> t₁ (t₂ m) a)
-> (forall a. e -> t₂ m a) -> forall a. e -> t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
HS.$ (forall a. e -> m a) -> forall a. e -> t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *) e.
(LiftError t, Monad m) =>
(forall a. e -> m a) -> forall (a :: k). e -> t m a
forall (m :: * -> *) e.
Monad m =>
(forall a. e -> m a) -> forall a. e -> t₂ m a
liftThrow e -> m a
forall a. e -> m a
throwM)

  liftCatch ∷ ∀ m e. (Monad m) ⇒ (∀ a. m a → (e → m a) → m a) → (∀ a. (t₁ ⊡ t₂) m a → (e → (t₁ ⊡ t₂) m a) → (t₁ ⊡ t₂) m a)
  liftCatch :: forall (m :: * -> *) e.
Monad m =>
(forall a. m a -> (e -> m a) -> m a)
-> forall a. (⊡) t₁ t₂ m a -> (e -> (⊡) t₁ t₂ m a) -> (⊡) t₁ t₂ m a
liftCatch forall a. m a -> (e -> m a) -> m a
catchM (⊡) t₁ t₂ m a
xM e -> (⊡) t₁ t₂ m a
k = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall a b. (a -> b) -> a -> b
$ ((forall a. t₂ m a -> (e -> t₂ m a) -> t₂ m a)
-> forall a. t₁ (t₂ m) a -> (e -> t₁ (t₂ m) a) -> t₁ (t₂ m) a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *) e.
(LiftError t, Monad m) =>
(forall a. m a -> (e -> m a) -> m a)
-> forall (a :: k). t m a -> (e -> t m a) -> t m a
forall (m :: * -> *) e.
Monad m =>
(forall a. m a -> (e -> m a) -> m a)
-> forall a. t₁ m a -> (e -> t₁ m a) -> t₁ m a
liftCatch ((forall a. t₂ m a -> (e -> t₂ m a) -> t₂ m a)
 -> forall a. t₁ (t₂ m) a -> (e -> t₁ (t₂ m) a) -> t₁ (t₂ m) a)
-> (forall a. t₂ m a -> (e -> t₂ m a) -> t₂ m a)
-> forall a. t₁ (t₂ m) a -> (e -> t₁ (t₂ m) a) -> t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
HS.$ (forall a. m a -> (e -> m a) -> m a)
-> forall a. t₂ m a -> (e -> t₂ m a) -> t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *) e.
(LiftError t, Monad m) =>
(forall a. m a -> (e -> m a) -> m a)
-> forall (a :: k). t m a -> (e -> t m a) -> t m a
forall (m :: * -> *) e.
Monad m =>
(forall a. m a -> (e -> m a) -> m a)
-> forall a. t₂ m a -> (e -> t₂ m a) -> t₂ m a
liftCatch m a -> (e -> m a) -> m a
forall a. m a -> (e -> m a) -> m a
catchM) ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 (⊡) t₁ t₂ m a
xM) ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a)
-> (e -> (⊡) t₁ t₂ m a) -> e -> t₁ (t₂ m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ e -> (⊡) t₁ t₂ m a
k)

instance (∀ m'. Monad m' ⇒ Monad (t₂ m'),LiftDelay t₁,LiftDelay t₂) ⇒ LiftDelay (t₁ ⊡ t₂) where
  liftDelay ∷ ∀ m. (Monad m) ⇒ (∀ a. (() → m a) → m a) → (∀ a. (() → (t₁ ⊡ t₂) m a) → (t₁ ⊡ t₂) m a)
  liftDelay :: forall (m :: * -> *).
Monad m =>
(forall a. (() -> m a) -> m a)
-> forall a. (() -> (⊡) t₁ t₂ m a) -> (⊡) t₁ t₂ m a
liftDelay forall a. (() -> m a) -> m a
delayM () -> (⊡) t₁ t₂ m a
xMU = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall a b. (a -> b) -> a -> b
$ ((forall a. (() -> t₂ m a) -> t₂ m a)
-> forall a. (() -> t₁ (t₂ m) a) -> t₁ (t₂ m) a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftDelay t, Monad m) =>
(forall a. (() -> m a) -> m a)
-> forall (a :: k). (() -> t m a) -> t m a
forall (m :: * -> *).
Monad m =>
(forall a. (() -> m a) -> m a)
-> forall a. (() -> t₁ m a) -> t₁ m a
liftDelay ((forall a. (() -> t₂ m a) -> t₂ m a)
 -> forall a. (() -> t₁ (t₂ m) a) -> t₁ (t₂ m) a)
-> (forall a. (() -> t₂ m a) -> t₂ m a)
-> forall a. (() -> t₁ (t₂ m) a) -> t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
HS.$ (forall a. (() -> m a) -> m a)
-> forall a. (() -> t₂ m a) -> t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftDelay t, Monad m) =>
(forall a. (() -> m a) -> m a)
-> forall (a :: k). (() -> t m a) -> t m a
forall (m :: * -> *).
Monad m =>
(forall a. (() -> m a) -> m a)
-> forall a. (() -> t₂ m a) -> t₂ m a
liftDelay (() -> m a) -> m a
forall a. (() -> m a) -> m a
delayM) ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a)
-> (() -> (⊡) t₁ t₂ m a) -> () -> t₁ (t₂ m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ () -> (⊡) t₁ t₂ m a
xMU)

instance (∀ m'. Monad m' ⇒ Monad (t₂ m'),LiftNondet t₁,LiftNondet t₂) ⇒ LiftNondet (t₁ ⊡ t₂) where
  liftMzero ∷ ∀ m. (Monad m) ⇒ (∀ a. m a) → (∀ a. (t₁ ⊡ t₂) m a)
  liftMzero :: forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. (⊡) t₁ t₂ m a
liftMzero forall a. m a
mzeroM = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall a b. (a -> b) -> a -> b
$ (forall a. t₂ m a) -> forall a. t₁ (t₂ m) a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftNondet t, Monad m) =>
(forall a. m a) -> forall (a :: k). t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. t₁ m a
liftMzero ((forall a. t₂ m a) -> forall a. t₁ (t₂ m) a)
-> (forall a. t₂ m a) -> forall a. t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
HS.$ (forall a. m a) -> forall a. t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftNondet t, Monad m) =>
(forall a. m a) -> forall (a :: k). t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. t₂ m a
liftMzero m a
forall a. m a
mzeroM

  liftMplus ∷ ∀ m. (Monad m) ⇒ (∀ a. m a → m a → m a) → (∀ a. (t₁ ⊡ t₂) m a → (t₁ ⊡ t₂) m a → (t₁ ⊡ t₂) m a)
  liftMplus :: forall (m :: * -> *).
Monad m =>
(forall a. m a -> m a -> m a)
-> forall a. (⊡) t₁ t₂ m a -> (⊡) t₁ t₂ m a -> (⊡) t₁ t₂ m a
liftMplus forall a. m a -> m a -> m a
mplusM (⊡) t₁ t₂ m a
xM₁ (⊡) t₁ t₂ m a
xM₂ = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall a b. (a -> b) -> a -> b
$ ((forall a. t₂ m a -> t₂ m a -> t₂ m a)
-> forall a. t₁ (t₂ m) a -> t₁ (t₂ m) a -> t₁ (t₂ m) a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftNondet t, Monad m) =>
(forall a. m a -> m a -> m a)
-> forall (a :: k). t m a -> t m a -> t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a -> m a -> m a)
-> forall a. t₁ m a -> t₁ m a -> t₁ m a
liftMplus ((forall a. t₂ m a -> t₂ m a -> t₂ m a)
 -> forall a. t₁ (t₂ m) a -> t₁ (t₂ m) a -> t₁ (t₂ m) a)
-> (forall a. t₂ m a -> t₂ m a -> t₂ m a)
-> forall a. t₁ (t₂ m) a -> t₁ (t₂ m) a -> t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
HS.$ (forall a. m a -> m a -> m a)
-> forall a. t₂ m a -> t₂ m a -> t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftNondet t, Monad m) =>
(forall a. m a -> m a -> m a)
-> forall (a :: k). t m a -> t m a -> t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a -> m a -> m a)
-> forall a. t₂ m a -> t₂ m a -> t₂ m a
liftMplus m a -> m a -> m a
forall a. m a -> m a -> m a
mplusM) ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 (⊡) t₁ t₂ m a
xM₁) ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 (⊡) t₁ t₂ m a
xM₂)

instance (∀ m'. Monad m' ⇒ Monad (t₂ m'),LiftTop t₁,LiftTop t₂) ⇒ LiftTop (t₁ ⊡ t₂) where
  liftMtop ∷ ∀ m. (Monad m) ⇒ (∀ a. m a) → (∀ a. (t₁ ⊡ t₂) m a)
  liftMtop :: forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. (⊡) t₁ t₂ m a
liftMtop forall a. m a
mtopM = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall a b. (a -> b) -> a -> b
$ (forall a. t₂ m a) -> forall a. t₁ (t₂ m) a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftTop t, Monad m) =>
(forall a. m a) -> forall (a :: k). t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. t₁ m a
liftMtop ((forall a. t₂ m a) -> forall a. t₁ (t₂ m) a)
-> (forall a. t₂ m a) -> forall a. t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
HS.$ (forall a. m a) -> forall a. t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftTop t, Monad m) =>
(forall a. m a) -> forall (a :: k). t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. t₂ m a
liftMtop m a
forall a. m a
mtopM

instance (∀ m'. Monad m' ⇒ Monad (t₂ m'),LiftCont t₁,LiftCont t₂) ⇒ LiftCont (t₁ ⊡ t₂) where
  liftCallCC ∷ ∀ m r. (Monad m) ⇒ (∀ a. ((a → m r) → m r) → m a) → (∀ a. ((a → (t₁ ⊡ t₂) m r) → (t₁ ⊡ t₂) m r) → (t₁ ⊡ t₂) m a)
  liftCallCC :: forall (m :: * -> *) r.
Monad m =>
(forall a. ((a -> m r) -> m r) -> m a)
-> forall a.
   ((a -> (⊡) t₁ t₂ m r) -> (⊡) t₁ t₂ m r) -> (⊡) t₁ t₂ m a
liftCallCC forall a. ((a -> m r) -> m r) -> m a
callCCM (a -> (⊡) t₁ t₂ m r) -> (⊡) t₁ t₂ m r
kk = t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) a -> (⊡) t₁ t₂ m a) -> t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
forall a b. (a -> b) -> a -> b
$ ((forall a. ((a -> t₂ m r) -> t₂ m r) -> t₂ m a)
-> forall a. ((a -> t₁ (t₂ m) r) -> t₁ (t₂ m) r) -> t₁ (t₂ m) a
forall (m :: * -> *) r.
Monad m =>
(forall a. ((a -> m r) -> m r) -> m a)
-> forall a. ((a -> t₁ m r) -> t₁ m r) -> t₁ m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftCont t, Monad m) =>
(forall a. ((a -> m r) -> m r) -> m a)
-> forall a. ((a -> t m r) -> t m r) -> t m a
liftCallCC ((forall a. ((a -> t₂ m r) -> t₂ m r) -> t₂ m a)
 -> forall a. ((a -> t₁ (t₂ m) r) -> t₁ (t₂ m) r) -> t₁ (t₂ m) a)
-> (forall a. ((a -> t₂ m r) -> t₂ m r) -> t₂ m a)
-> forall a. ((a -> t₁ (t₂ m) r) -> t₁ (t₂ m) r) -> t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
HS.$ (forall a. ((a -> m r) -> m r) -> m a)
-> forall a. ((a -> t₂ m r) -> t₂ m r) -> t₂ m a
forall (m :: * -> *) r.
Monad m =>
(forall a. ((a -> m r) -> m r) -> m a)
-> forall a. ((a -> t₂ m r) -> t₂ m r) -> t₂ m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftCont t, Monad m) =>
(forall a. ((a -> m r) -> m r) -> m a)
-> forall a. ((a -> t m r) -> t m r) -> t m a
liftCallCC ((a -> m r) -> m r) -> m a
forall a. ((a -> m r) -> m r) -> m a
callCCM) (((a -> t₁ (t₂ m) r) -> t₁ (t₂ m) r) -> t₁ (t₂ m) a)
-> ((a -> t₁ (t₂ m) r) -> t₁ (t₂ m) r) -> t₁ (t₂ m) a
forall a b. (a -> b) -> a -> b
$ \ (a -> t₁ (t₂ m) r
k ∷ a → t₁ (t₂ m) r) → (⊡) t₁ t₂ m r -> t₁ (t₂ m) r
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 ((⊡) t₁ t₂ m r -> t₁ (t₂ m) r) -> (⊡) t₁ t₂ m r -> t₁ (t₂ m) r
forall a b. (a -> b) -> a -> b
$ (a -> (⊡) t₁ t₂ m r) -> (⊡) t₁ t₂ m r
kk (t₁ (t₂ m) r -> (⊡) t₁ t₂ m r
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) r -> (⊡) t₁ t₂ m r)
-> (a -> t₁ (t₂ m) r) -> a -> (⊡) t₁ t₂ m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> t₁ (t₂ m) r
k)

  liftWithC ∷ ∀ m r. (Monad m) ⇒ (∀ a. (a → m r) → m a → m r) →  (∀ a. (a → (t₁ ⊡ t₂) m r) → (t₁ ⊡ t₂) m a → (t₁ ⊡ t₂) m r)
  liftWithC :: forall (m :: * -> *) r.
Monad m =>
(forall a. (a -> m r) -> m a -> m r)
-> forall a. (a -> (⊡) t₁ t₂ m r) -> (⊡) t₁ t₂ m a -> (⊡) t₁ t₂ m r
liftWithC forall a. (a -> m r) -> m a -> m r
withCM a -> (⊡) t₁ t₂ m r
k (⊡) t₁ t₂ m a
xM = t₁ (t₂ m) r -> (⊡) t₁ t₂ m r
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
t₁ (t₂ m) a -> (⊡) t₁ t₂ m a
Compose2 (t₁ (t₂ m) r -> (⊡) t₁ t₂ m r) -> t₁ (t₂ m) r -> (⊡) t₁ t₂ m r
forall a b. (a -> b) -> a -> b
$ ((forall a. (a -> t₂ m r) -> t₂ m a -> t₂ m r)
-> forall a. (a -> t₁ (t₂ m) r) -> t₁ (t₂ m) a -> t₁ (t₂ m) r
forall (m :: * -> *) r.
Monad m =>
(forall a. (a -> m r) -> m a -> m r)
-> forall a. (a -> t₁ m r) -> t₁ m a -> t₁ m r
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftCont t, Monad m) =>
(forall a. (a -> m r) -> m a -> m r)
-> forall a. (a -> t m r) -> t m a -> t m r
liftWithC ((forall a. (a -> t₂ m r) -> t₂ m a -> t₂ m r)
 -> forall a. (a -> t₁ (t₂ m) r) -> t₁ (t₂ m) a -> t₁ (t₂ m) r)
-> (forall a. (a -> t₂ m r) -> t₂ m a -> t₂ m r)
-> forall a. (a -> t₁ (t₂ m) r) -> t₁ (t₂ m) a -> t₁ (t₂ m) r
forall a b. (a -> b) -> a -> b
HS.$ (forall a. (a -> m r) -> m a -> m r)
-> forall a. (a -> t₂ m r) -> t₂ m a -> t₂ m r
forall (m :: * -> *) r.
Monad m =>
(forall a. (a -> m r) -> m a -> m r)
-> forall a. (a -> t₂ m r) -> t₂ m a -> t₂ m r
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftCont t, Monad m) =>
(forall a. (a -> m r) -> m a -> m r)
-> forall a. (a -> t m r) -> t m a -> t m r
liftWithC (a -> m r) -> m a -> m r
forall a. (a -> m r) -> m a -> m r
withCM) ((⊡) t₁ t₂ m r -> t₁ (t₂ m) r
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 ((⊡) t₁ t₂ m r -> t₁ (t₂ m) r)
-> (a -> (⊡) t₁ t₂ m r) -> a -> t₁ (t₂ m) r
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> (⊡) t₁ t₂ m r
k) ((⊡) t₁ t₂ m a -> t₁ (t₂ m) a
forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(⊡) t₁ t₂ m a -> t₁ (t₂ m) a
unCompose2 (⊡) t₁ t₂ m a
xM)

-------------
-- LIFTING --
-------------

-- instance {-# OVERLAPPABLE #-} (Monad m,MonadIO m,LiftIO t) ⇒ MonadIO (t m) where
--   io = liftIO io
-- instance {-# OVERLAPPABLE #-} (Monad m,MonadReader r m,LiftReader t) ⇒ MonadReader r (t m) where
--   askL = liftAskL askL
--   localL = liftLocalL localL
-- instance {-# OVERLAPPABLE #-} (Monad m,MonadWriter o m,LiftWriter t) ⇒ MonadWriter o (t m) where
--   tell = liftTell tell
--   hijack = liftHijack hijack
-- instance {-# OVERLAPPABLE #-} (Monad m,MonadState s m,LiftState t) ⇒ MonadState s (t m) where
--   get = liftGet get
--   put = liftPut put
-- instance {-# OVERLAPPABLE #-} (Monad m,MonadFail m,LiftFail t) ⇒ MonadFail (t m) where
--   abort = liftAbort abort
--   (⎅) = liftTry (⎅)
-- instance {-# OVERLAPPABLE #-} (Monad m,MonadError e m,LiftError t) ⇒ MonadError e (t m) where
--   throw = liftThrow throw
--   catch = liftCatch catch
-- instance {-# OVERLAPPABLE #-} (Monad m,MonadDelay m,LiftDelay t) ⇒ MonadDelay (t m) where
--   delay = liftDelay delay
-- instance {-# OVERLAPPABLE #-} (Monad m,MonadNondet m,LiftNondet t) ⇒ MonadNondet (t m) where
--   mzero = liftMzero mzero
--   (⊞) = liftMplus (⊞)
-- instance {-# OVERLAPPABLE #-} (Monad m,MonadTop m,LiftTop t) ⇒ MonadTop (t m) where
--   mtop = liftMtop mtop
-- instance {-# OVERLAPPABLE #-} (Monad m,MonadCont r m,LiftCont t) ⇒ MonadCont r (t m) where
--   callCC = liftCallCC callCC
--   withC = liftWithC withC

--------------
-- DERIVING --
--------------

deriveLiftIO ∷ ∀ t₁ t₂ m. (Monad m,t₁ ⇄⁼ t₂,LiftIO t₂) ⇒ (∀ a. IO a → m a) → (∀ a. IO a → t₁ m a)
deriveLiftIO :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *).
(Monad m, t₁ ⇄⁼ t₂, LiftIO t₂) =>
(forall a. IO a -> m a) -> forall a. IO a -> t₁ m a
deriveLiftIO forall a. IO a -> m a
ioM IO a
xM = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> t₂ m a -> t₁ m a
forall a b. (a -> b) -> a -> b
$ (forall a. IO a -> m a) -> forall a. IO a -> t₂ m a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> forall a. IO a -> t₂ m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *).
(LiftIO t, Monad m) =>
(forall a. IO a -> m a) -> forall a. IO a -> t m a
liftIO IO a -> m a
forall a. IO a -> m a
ioM IO a
xM

deriveLiftAskL ∷ ∀ t₁ t₂ m r. (Monad m,t₁ ⇄⁼ t₂,LiftReader t₂) ⇒ (∀ r'. r ⟢ r' → m r') → (∀ r'. r ⟢ r' → t₁ m r')
deriveLiftAskL :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) r.
(Monad m, t₁ ⇄⁼ t₂, LiftReader t₂) =>
(forall r'. (r ⟢ r') -> m r') -> forall r'. (r ⟢ r') -> t₁ m r'
deriveLiftAskL forall r'. (r ⟢ r') -> m r'
askLM = t₂ m r' -> t₁ m r'
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m r' -> t₁ m r')
-> ((r ⟢ r') -> t₂ m r') -> (r ⟢ r') -> t₁ m r'
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (forall r'. (r ⟢ r') -> m r') -> forall r'. (r ⟢ r') -> t₂ m r'
forall (m :: * -> *) r.
Monad m =>
(forall r'. (r ⟢ r') -> m r') -> forall r'. (r ⟢ r') -> t₂ m r'
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftReader t, Monad m) =>
(forall r'. (r ⟢ r') -> m r') -> forall r'. (r ⟢ r') -> t m r'
liftAskL (r ⟢ r') -> m r'
forall r'. (r ⟢ r') -> m r'
askLM

deriveLiftLocalL ∷ ∀ t₁ t₂ m r. (Monad m,t₁ ⇄⁼ t₂,LiftReader t₂) ⇒ (∀ r' a. r ⟢ r' → r' → m a → m a) → (∀ r' a. r ⟢ r' → r' → t₁ m a → t₁ m a)
deriveLiftLocalL :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) r.
(Monad m, t₁ ⇄⁼ t₂, LiftReader t₂) =>
(forall r' a. (r ⟢ r') -> r' -> m a -> m a)
-> forall r' a. (r ⟢ r') -> r' -> t₁ m a -> t₁ m a
deriveLiftLocalL forall r' a. (r ⟢ r') -> r' -> m a -> m a
localLM r ⟢ r'
ℓ r'
r = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> (t₂ m a -> t₂ m a) -> t₂ m a -> t₁ m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (forall r' a. (r ⟢ r') -> r' -> m a -> m a)
-> forall r' a. (r ⟢ r') -> r' -> t₂ m a -> t₂ m a
forall (m :: * -> *) r.
Monad m =>
(forall r' a. (r ⟢ r') -> r' -> m a -> m a)
-> forall r' a. (r ⟢ r') -> r' -> t₂ m a -> t₂ m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftReader t, Monad m) =>
(forall r' a. (r ⟢ r') -> r' -> m a -> m a)
-> forall r' a. (r ⟢ r') -> r' -> t m a -> t m a
liftLocalL (r ⟢ r') -> r' -> m a -> m a
forall r' a. (r ⟢ r') -> r' -> m a -> m a
localLM r ⟢ r'
ℓ r'
r (t₂ m a -> t₁ m a) -> (t₁ m a -> t₂ m a) -> t₁ m a -> t₁ m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t₁ m a -> t₂ m a
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3

deriveLiftTell ∷ ∀ t₁ t₂ m o. (Monad m,t₁ ⇄⁼ t₂,LiftWriter t₂) ⇒ (o → m ()) → (o → t₁ m ())
deriveLiftTell :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) o.
(Monad m, t₁ ⇄⁼ t₂, LiftWriter t₂) =>
(o -> m ()) -> o -> t₁ m ()
deriveLiftTell o -> m ()
tellM = t₂ m () -> t₁ m ()
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m () -> t₁ m ()) -> (o -> t₂ m ()) -> o -> t₁ m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (o -> m ()) -> o -> t₂ m ()
forall (m :: * -> *) o. Monad m => (o -> m ()) -> o -> t₂ m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) o.
(LiftWriter t, Monad m) =>
(o -> m ()) -> o -> t m ()
liftTell o -> m ()
tellM

deriveLiftHijack ∷ ∀ t₁ t₂ m o. (Monad m,t₁ ⇄⁼ t₂,LiftWriter t₂) ⇒ (∀ a. m a → m (o ∧ a)) → (∀ a. t₁ m a → t₁ m (o ∧ a))
deriveLiftHijack :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) o.
(Monad m, t₁ ⇄⁼ t₂, LiftWriter t₂) =>
(forall a. m a -> m (o ∧ a)) -> forall a. t₁ m a -> t₁ m (o ∧ a)
deriveLiftHijack forall a. m a -> m (o ∧ a)
hijackM = t₂ m (o ∧ a) -> t₁ m (o ∧ a)
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m (o ∧ a) -> t₁ m (o ∧ a))
-> (t₂ m a -> t₂ m (o ∧ a)) -> t₂ m a -> t₁ m (o ∧ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (forall a. m a -> m (o ∧ a)) -> forall a. t₂ m a -> t₂ m (o ∧ a)
forall (m :: * -> *) o.
Monad m =>
(forall a. m a -> m (o ∧ a)) -> forall a. t₂ m a -> t₂ m (o ∧ a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) o.
(LiftWriter t, Monad m) =>
(forall a. m a -> m (o ∧ a)) -> forall a. t m a -> t m (o ∧ a)
liftHijack m a -> m (o ∧ a)
forall a. m a -> m (o ∧ a)
hijackM (t₂ m a -> t₁ m (o ∧ a))
-> (t₁ m a -> t₂ m a) -> t₁ m a -> t₁ m (o ∧ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t₁ m a -> t₂ m a
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3

deriveLiftGet ∷ ∀ t₁ t₂ m s. (Monad m,t₁ ⇄⁼ t₂,LiftState t₂) ⇒ m s → t₁ m s
deriveLiftGet :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) s.
(Monad m, t₁ ⇄⁼ t₂, LiftState t₂) =>
m s -> t₁ m s
deriveLiftGet m s
getM = t₂ m s -> t₁ m s
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m s -> t₁ m s) -> t₂ m s -> t₁ m s
forall a b. (a -> b) -> a -> b
$ m s -> t₂ m s
forall (m :: * -> *) s. Monad m => m s -> t₂ m s
forall (t :: (* -> *) -> * -> *) (m :: * -> *) s.
(LiftState t, Monad m) =>
m s -> t m s
liftGet m s
getM

deriveLiftPut ∷ ∀ t₁ t₂ m s. (Monad m,t₁ ⇄⁼ t₂,LiftState t₂) ⇒ (s → m ()) → (s → t₁ m ())
deriveLiftPut :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) s.
(Monad m, t₁ ⇄⁼ t₂, LiftState t₂) =>
(s -> m ()) -> s -> t₁ m ()
deriveLiftPut s -> m ()
putM = t₂ m () -> t₁ m ()
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m () -> t₁ m ()) -> (s -> t₂ m ()) -> s -> t₁ m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s -> m ()) -> s -> t₂ m ()
forall (m :: * -> *) s. Monad m => (s -> m ()) -> s -> t₂ m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) s.
(LiftState t, Monad m) =>
(s -> m ()) -> s -> t m ()
liftPut s -> m ()
putM

deriveLiftAbort ∷ ∀ t₁ t₂ m. (Monad m,t₁ ⇄⁼ t₂,LiftFail t₂) ⇒ (∀ a. m a) → (∀ a. t₁ m a)
deriveLiftAbort :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *).
(Monad m, t₁ ⇄⁼ t₂, LiftFail t₂) =>
(forall a. m a) -> forall a. t₁ m a
deriveLiftAbort forall a. m a
abortM = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> t₂ m a -> t₁ m a
forall a b. (a -> b) -> a -> b
$ (forall a. m a) -> forall a. t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftFail t, Monad m) =>
(forall a. m a) -> forall (a :: k). t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. t₂ m a
liftAbort m a
forall a. m a
abortM

deriveLiftTry ∷ ∀ t₁ t₂ m. (Monad m,t₁ ⇄⁼ t₂,LiftFail t₂) ⇒ (∀ a. m a → m a → m a) → (∀ a. t₁ m a → t₁ m a → t₁ m a)
deriveLiftTry :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *).
(Monad m, t₁ ⇄⁼ t₂, LiftFail t₂) =>
(forall a. m a -> m a -> m a)
-> forall a. t₁ m a -> t₁ m a -> t₁ m a
deriveLiftTry forall a. m a -> m a -> m a
tryM t₁ m a
xM₁ t₁ m a
xM₂ = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> t₂ m a -> t₁ m a
forall a b. (a -> b) -> a -> b
$ (forall a. m a -> m a -> m a)
-> forall a. t₂ m a -> t₂ m a -> t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftFail t, Monad m) =>
(forall a. m a -> m a -> m a)
-> forall (a :: k). t m a -> t m a -> t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a -> m a -> m a)
-> forall a. t₂ m a -> t₂ m a -> t₂ m a
liftTry m a -> m a -> m a
forall a. m a -> m a -> m a
tryM (t₁ m a -> t₂ m a
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 t₁ m a
xM₁) (t₁ m a -> t₂ m a
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 t₁ m a
xM₂)

deriveLiftThrow ∷ ∀ t₁ t₂ m e. (Monad m,t₁ ⇄⁼ t₂,LiftError t₂) ⇒ (∀ a. e → m a) → (∀ a. e → t₁ m a)
deriveLiftThrow :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) e.
(Monad m, t₁ ⇄⁼ t₂, LiftError t₂) =>
(forall a. e -> m a) -> forall a. e -> t₁ m a
deriveLiftThrow forall a. e -> m a
throwM e
e = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> t₂ m a -> t₁ m a
forall a b. (a -> b) -> a -> b
$ (forall a. e -> m a) -> forall a. e -> t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *) e.
(LiftError t, Monad m) =>
(forall a. e -> m a) -> forall (a :: k). e -> t m a
forall (m :: * -> *) e.
Monad m =>
(forall a. e -> m a) -> forall a. e -> t₂ m a
liftThrow e -> m a
forall a. e -> m a
throwM e
e

deriveLiftCatch ∷ ∀ t₁ t₂ m e. (Monad m,t₁ ⇄⁼ t₂,LiftError t₂) ⇒ (∀ a. m a → (e → m a) → m a) → (∀ a. t₁ m a → (e → t₁ m a) → t₁ m a)
deriveLiftCatch :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) e.
(Monad m, t₁ ⇄⁼ t₂, LiftError t₂) =>
(forall a. m a -> (e -> m a) -> m a)
-> forall a. t₁ m a -> (e -> t₁ m a) -> t₁ m a
deriveLiftCatch forall a. m a -> (e -> m a) -> m a
catchM t₁ m a
xM e -> t₁ m a
k = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> t₂ m a -> t₁ m a
forall a b. (a -> b) -> a -> b
$ (forall a. m a -> (e -> m a) -> m a)
-> forall a. t₂ m a -> (e -> t₂ m a) -> t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *) e.
(LiftError t, Monad m) =>
(forall a. m a -> (e -> m a) -> m a)
-> forall (a :: k). t m a -> (e -> t m a) -> t m a
forall (m :: * -> *) e.
Monad m =>
(forall a. m a -> (e -> m a) -> m a)
-> forall a. t₂ m a -> (e -> t₂ m a) -> t₂ m a
liftCatch m a -> (e -> m a) -> m a
forall a. m a -> (e -> m a) -> m a
catchM (t₁ m a -> t₂ m a
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 t₁ m a
xM) (t₁ m a -> t₂ m a
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 (t₁ m a -> t₂ m a) -> (e -> t₁ m a) -> e -> t₂ m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ e -> t₁ m a
k)

deriveLiftDelay ∷ ∀ t₁ t₂ m. (Monad m,t₁ ⇄⁼ t₂,LiftDelay t₂) ⇒ (∀ a. (() → m a) → m a) → (∀ a. (() → t₁ m a) → t₁ m a)
deriveLiftDelay :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *).
(Monad m, t₁ ⇄⁼ t₂, LiftDelay t₂) =>
(forall a. (() -> m a) -> m a)
-> forall a. (() -> t₁ m a) -> t₁ m a
deriveLiftDelay forall a. (() -> m a) -> m a
delayM () -> t₁ m a
xMU = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> t₂ m a -> t₁ m a
forall a b. (a -> b) -> a -> b
$ (forall a. (() -> m a) -> m a)
-> forall a. (() -> t₂ m a) -> t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftDelay t, Monad m) =>
(forall a. (() -> m a) -> m a)
-> forall (a :: k). (() -> t m a) -> t m a
forall (m :: * -> *).
Monad m =>
(forall a. (() -> m a) -> m a)
-> forall a. (() -> t₂ m a) -> t₂ m a
liftDelay (() -> m a) -> m a
forall a. (() -> m a) -> m a
delayM ((() -> t₂ m a) -> t₂ m a) -> (() -> t₂ m a) -> t₂ m a
forall a b. (a -> b) -> a -> b
$ t₁ m a -> t₂ m a
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 (t₁ m a -> t₂ m a) -> (() -> t₁ m a) -> () -> t₂ m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ () -> t₁ m a
xMU

deriveLiftMzero ∷ ∀ t₁ t₂ m. (Monad m,t₁ ⇄⁼ t₂,LiftNondet t₂) ⇒ (∀ a. m a) → (∀ a. t₁ m a)
deriveLiftMzero :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *).
(Monad m, t₁ ⇄⁼ t₂, LiftNondet t₂) =>
(forall a. m a) -> forall a. t₁ m a
deriveLiftMzero forall a. m a
mzeroM = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> t₂ m a -> t₁ m a
forall a b. (a -> b) -> a -> b
$ (forall a. m a) -> forall a. t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftNondet t, Monad m) =>
(forall a. m a) -> forall (a :: k). t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. t₂ m a
liftMzero m a
forall a. m a
mzeroM

deriveLiftMplus ∷ ∀ t₁ t₂ m. (Monad m,t₁ ⇄⁼ t₂,LiftNondet t₂) ⇒ (∀ a. m a → m a → m a) → (∀ a. t₁ m a → t₁ m a → t₁ m a)
deriveLiftMplus :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *).
(Monad m, t₁ ⇄⁼ t₂, LiftNondet t₂) =>
(forall a. m a -> m a -> m a)
-> forall a. t₁ m a -> t₁ m a -> t₁ m a
deriveLiftMplus forall a. m a -> m a -> m a
mplusM t₁ m a
xM₁ t₁ m a
xM₂ = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> t₂ m a -> t₁ m a
forall a b. (a -> b) -> a -> b
$ (forall a. m a -> m a -> m a)
-> forall a. t₂ m a -> t₂ m a -> t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftNondet t, Monad m) =>
(forall a. m a -> m a -> m a)
-> forall (a :: k). t m a -> t m a -> t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a -> m a -> m a)
-> forall a. t₂ m a -> t₂ m a -> t₂ m a
liftMplus m a -> m a -> m a
forall a. m a -> m a -> m a
mplusM (t₁ m a -> t₂ m a
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 t₁ m a
xM₁) (t₁ m a -> t₂ m a
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 t₁ m a
xM₂)

deriveLiftMtop ∷ ∀ t₁ t₂ m. (Monad m,t₁ ⇄⁼ t₂,LiftTop t₂) ⇒ (∀ a. m a) → (∀ a. t₁ m a)
deriveLiftMtop :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *).
(Monad m, t₁ ⇄⁼ t₂, LiftTop t₂) =>
(forall a. m a) -> forall a. t₁ m a
deriveLiftMtop forall a. m a
mtopM = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> t₂ m a -> t₁ m a
forall a b. (a -> b) -> a -> b
$ (forall a. m a) -> forall a. t₂ m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *).
(LiftTop t, Monad m) =>
(forall a. m a) -> forall (a :: k). t m a
forall (m :: * -> *).
Monad m =>
(forall a. m a) -> forall a. t₂ m a
liftMtop m a
forall a. m a
mtopM

deriveLiftCallCC ∷ ∀ t₁ t₂ m r. (Monad m,t₁ ⇄⁼ t₂,LiftCont t₂) ⇒ (∀ a. ((a → m r) → m r) → m a) → (∀ a. ((a → t₁ m r) → t₁ m r) → t₁ m a)
deriveLiftCallCC :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) r.
(Monad m, t₁ ⇄⁼ t₂, LiftCont t₂) =>
(forall a. ((a -> m r) -> m r) -> m a)
-> forall a. ((a -> t₁ m r) -> t₁ m r) -> t₁ m a
deriveLiftCallCC forall a. ((a -> m r) -> m r) -> m a
callCCM (a -> t₁ m r) -> t₁ m r
kk = t₂ m a -> t₁ m a
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m a -> t₁ m a) -> t₂ m a -> t₁ m a
forall a b. (a -> b) -> a -> b
$ (forall a. ((a -> m r) -> m r) -> m a)
-> forall a. ((a -> t₂ m r) -> t₂ m r) -> t₂ m a
forall (m :: * -> *) r.
Monad m =>
(forall a. ((a -> m r) -> m r) -> m a)
-> forall a. ((a -> t₂ m r) -> t₂ m r) -> t₂ m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftCont t, Monad m) =>
(forall a. ((a -> m r) -> m r) -> m a)
-> forall a. ((a -> t m r) -> t m r) -> t m a
liftCallCC ((a -> m r) -> m r) -> m a
forall a. ((a -> m r) -> m r) -> m a
callCCM (((a -> t₂ m r) -> t₂ m r) -> t₂ m a)
-> ((a -> t₂ m r) -> t₂ m r) -> t₂ m a
forall a b. (a -> b) -> a -> b
$ \ (a -> t₂ m r
k ∷ a → t₂ m r) → t₁ m r -> t₂ m r
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 (t₁ m r -> t₂ m r) -> t₁ m r -> t₂ m r
forall a b. (a -> b) -> a -> b
$ (a -> t₁ m r) -> t₁ m r
kk (t₂ m r -> t₁ m r
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m r -> t₁ m r) -> (a -> t₂ m r) -> a -> t₁ m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> t₂ m r
k)

deriveLiftWithC ∷ ∀ t₁ t₂ m r. (Monad m,t₁ ⇄⁼ t₂,LiftCont t₂) ⇒ (∀ a. (a → m r) → m a → m r) → (∀ a. (a → t₁ m r) → t₁ m a → t₁ m r)
deriveLiftWithC :: forall (t₁ :: (* -> *) -> * -> *) (t₂ :: (* -> *) -> * -> *)
       (m :: * -> *) r.
(Monad m, t₁ ⇄⁼ t₂, LiftCont t₂) =>
(forall a. (a -> m r) -> m a -> m r)
-> forall a. (a -> t₁ m r) -> t₁ m a -> t₁ m r
deriveLiftWithC forall a. (a -> m r) -> m a -> m r
withCM a -> t₁ m r
k t₁ m a
xM = t₂ m r -> t₁ m r
t₂ →⁼ t₁
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 (t₂ m r -> t₁ m r) -> t₂ m r -> t₁ m r
forall a b. (a -> b) -> a -> b
$ (forall a. (a -> m r) -> m a -> m r)
-> forall a. (a -> t₂ m r) -> t₂ m a -> t₂ m r
forall (m :: * -> *) r.
Monad m =>
(forall a. (a -> m r) -> m a -> m r)
-> forall a. (a -> t₂ m r) -> t₂ m a -> t₂ m r
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r.
(LiftCont t, Monad m) =>
(forall a. (a -> m r) -> m a -> m r)
-> forall a. (a -> t m r) -> t m a -> t m r
liftWithC (a -> m r) -> m a -> m r
forall a. (a -> m r) -> m a -> m r
withCM (t₁ m r -> t₂ m r
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 (t₁ m r -> t₂ m r) -> (a -> t₁ m r) -> a -> t₂ m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> t₁ m r
k) (t₁ m a -> t₂ m a
t₁ →⁼ t₂
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 t₁ m a
xM)

-- instance {-# OVERLAPPABLE #-} (t₁ ⇄⁼ t₂,LiftIO t₂) ⇒ LiftIO t₁ where
--   liftIO = deriveLiftIO
-- instance {-# OVERLAPPABLE #-} (t₁ ⇄⁼ t₂,LiftReader t₂) ⇒ LiftReader t₁ where
--   liftAskL = deriveLiftAskL
--   liftLocalL = deriveLiftLocalL
-- instance {-# OVERLAPPABLE #-} (t₁ ⇄⁼ t₂,LiftWriter t₂) ⇒ LiftWriter t₁ where
--   liftTell = deriveLiftTell
--   liftHijack = deriveLiftHijack
-- instance {-# OVERLAPPABLE #-} (t₁ ⇄⁼ t₂,LiftState t₂) ⇒ LiftState t₁ where
--   liftGet = deriveLiftGet
--   liftPut = deriveLiftPut
-- instance {-# OVERLAPPABLE #-} (t₁ ⇄⁼ t₂,LiftFail t₂) ⇒ LiftFail t₁ where
--   liftAbort = deriveLiftAbort
--   liftTry = deriveLiftTry
-- instance {-# OVERLAPPABLE #-} (t₁ ⇄⁼ t₂,LiftError t₂) ⇒ LiftError t₁ where
--   liftThrow = deriveLiftThrow
--   liftCatch = deriveLiftCatch
-- instance {-# OVERLAPPABLE #-} (t₁ ⇄⁼ t₂,LiftDelay t₂) ⇒ LiftDelay t₁ where
--   liftDelay = deriveLiftDelay
-- instance {-# OVERLAPPABLE #-} (t₁ ⇄⁼ t₂,LiftNondet t₂) ⇒ LiftNondet t₁ where
--   liftMzero = deriveLiftMzero
--   liftMplus = deriveLiftMplus
-- instance {-# OVERLAPPABLE #-} (t₁ ⇄⁼ t₂,LiftTop t₂) ⇒ LiftTop t₁ where
--   liftMtop = deriveLiftMtop
-- instance {-# OVERLAPPABLE #-} (t₁ ⇄⁼ t₂,LiftCont t₂) ⇒ LiftCont t₁ where
--   liftCallCC = deriveLiftCallCC
--   liftWithC = deriveLiftWithC