module Control.Monad.Ology.General.Function
    ( TransKind
    -- * Raised
    , Raised
    , type (-->)
    , WRaised(..)
    , wLift
    , wLiftIO
    -- * Backraised
    , Backraised
    , type (-/->)
    , backraisedToRaised
    , WBackraised(..)
    , wBackraisedToWRaised
    -- * Unlift
    , Unlift
    , WUnlift(..)
    , wUnliftToWRaised
    -- * Extract
    , Extract
    , WExtract(..)
    ) where

import Control.Monad.Ology.General.IO
import Control.Monad.Ology.General.Trans.Trans
import Import

type TransKind = (Type -> Type) -> (Type -> Type)

type Raised :: forall k. (k -> Type) -> (k -> Type) -> Type
type Raised p q = forall a. p a -> q a

type p --> q = Raised p q

type WRaised :: forall k. (k -> Type) -> (k -> Type) -> Type
newtype WRaised p q = MkWRaised
    { forall k (p :: k -> Type) (q :: k -> Type). WRaised p q -> p --> q
unWRaised :: p --> q
    }

wLift :: (MonadTrans t, Monad m) => WRaised m (t m)
wLift :: forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type).
(MonadTrans t, Monad m) =>
WRaised m (t m)
wLift = forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

wLiftIO :: MonadIO m => WRaised IO m
wLiftIO :: forall (m :: Type -> Type). MonadIO m => WRaised IO m
wLiftIO = forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO

instance Category WRaised where
    id :: forall (a :: k -> Type). WRaised a a
id = forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised forall {k} (cat :: k -> k -> Type) (a :: k).
Category cat =>
cat a a
id
    (MkWRaised b --> c
bc) . :: forall (b :: k -> Type) (c :: k -> Type) (a :: k -> Type).
WRaised b c -> WRaised a b -> WRaised a c
. (MkWRaised a --> b
ab) = forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised forall a b. (a -> b) -> a -> b
$ b --> c
bc forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a --> b
ab

type Backraised :: forall k. (k -> Type) -> (k -> Type) -> Type
type Backraised ma mb = forall r. ((mb --> ma) -> ma r) -> mb r

type ma -/-> mb = Backraised ma mb

backraisedToRaised :: (ma -/-> mb) -> ma --> mb
backraisedToRaised :: forall {k} (ma :: k -> Type) (mb :: k -> Type).
(ma -/-> mb) -> ma --> mb
backraisedToRaised ma -/-> mb
mbf ma a
ma = ma -/-> mb
mbf forall a b. (a -> b) -> a -> b
$ \mb --> ma
_ -> ma a
ma

type WBackraised :: forall k. (k -> Type) -> (k -> Type) -> Type
newtype WBackraised p q = MkWBackraised
    { forall k (p :: k -> Type) (q :: k -> Type).
WBackraised p q -> p -/-> q
unWBackraised :: p -/-> q
    }

instance Category WBackraised where
    id :: forall (a :: k -> Type). WBackraised a a
id = forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised forall a b. (a -> b) -> a -> b
$ \(a --> a) -> a r
f -> (a --> a) -> a r
f forall {k} (cat :: k -> k -> Type) (a :: k).
Category cat =>
cat a a
id
    (MkWBackraised b -/-> c
bc) . :: forall (b :: k -> Type) (c :: k -> Type) (a :: k -> Type).
WBackraised b c -> WBackraised a b -> WBackraised a c
. (MkWBackraised a -/-> b
ab) = forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised forall a b. (a -> b) -> a -> b
$ \(c --> a) -> a r
f -> b -/-> c
bc forall a b. (a -> b) -> a -> b
$ \c --> b
mcmb -> a -/-> b
ab forall a b. (a -> b) -> a -> b
$ \b --> a
mbma -> (c --> a) -> a r
f forall a b. (a -> b) -> a -> b
$ b --> a
mbma forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c --> b
mcmb

wBackraisedToWRaised :: WBackraised ma mb -> WRaised ma mb
wBackraisedToWRaised :: forall {k} (ma :: k -> Type) (mb :: k -> Type).
WBackraised ma mb -> WRaised ma mb
wBackraisedToWRaised (MkWBackraised ma -/-> mb
f) = forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised forall a b. (a -> b) -> a -> b
$ forall {k} (ma :: k -> Type) (mb :: k -> Type).
(ma -/-> mb) -> ma --> mb
backraisedToRaised ma -/-> mb
f

type Unlift :: ((Type -> Type) -> Constraint) -> TransKind -> Type
type Unlift c t = forall (m :: Type -> Type). c m => t m --> m

type WUnlift :: ((Type -> Type) -> Constraint) -> TransKind -> Type
newtype WUnlift c t = MkWUnlift
    { forall (c :: (Type -> Type) -> Constraint)
       (t :: (Type -> Type) -> Type -> Type).
WUnlift c t -> Unlift c t
unWUnlift :: Unlift c t
    }

wUnliftToWRaised :: c m => WUnlift c t -> WRaised (t m) m
wUnliftToWRaised :: forall (c :: (Type -> Type) -> Constraint) (m :: Type -> Type)
       (t :: (Type -> Type) -> Type -> Type).
c m =>
WUnlift c t -> WRaised (t m) m
wUnliftToWRaised (MkWUnlift Unlift c t
unlift) = forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised Unlift c t
unlift

type Extract :: (Type -> Type) -> Type
type Extract m = forall a. m a -> a

type WExtract :: (Type -> Type) -> Type
newtype WExtract m = MkWExtract
    { forall (m :: Type -> Type). WExtract m -> Extract m
unWExtract :: Extract m
    }