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 (-->) :: forall k. (k -> Type) -> (k -> Type) -> Type
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 = (m --> t m) -> WRaised m (t m)
forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised m a -> t m a
m --> t m
forall (m :: Type -> Type) a. Monad m => m a -> t m a
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 = (IO --> m) -> WRaised IO m
forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised IO a -> m a
IO --> m
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 = (a --> a) -> WRaised a a
forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised a a -> a a
a --> a
forall a. a -> a
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) = (a --> c) -> WRaised a c
forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised ((a --> c) -> WRaised a c) -> (a --> c) -> WRaised a c
forall a b. (a -> b) -> a -> b
$ b a -> c a
b --> c
bc (b a -> c a) -> (a a -> b a) -> a a -> c a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a a -> b a
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 (-/->) :: forall k. (k -> Type) -> (k -> Type) -> Type
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 = ((mb --> ma) -> ma a) -> mb a
ma -/-> mb
mbf (((mb --> ma) -> ma a) -> mb a) -> ((mb --> ma) -> ma a) -> mb a
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 = (a -/-> a) -> WBackraised a a
forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised ((a -/-> a) -> WBackraised a a) -> (a -/-> a) -> WBackraised a a
forall a b. (a -> b) -> a -> b
$ \(a --> a) -> a r
f -> (a --> a) -> a r
f a a -> a a
a --> a
forall a. a -> a
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) = (a -/-> c) -> WBackraised a c
forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised ((a -/-> c) -> WBackraised a c) -> (a -/-> c) -> WBackraised a c
forall a b. (a -> b) -> a -> b
$ \(c --> a) -> a r
f -> ((c --> b) -> b r) -> c r
b -/-> c
bc (((c --> b) -> b r) -> c r) -> ((c --> b) -> b r) -> c r
forall a b. (a -> b) -> a -> b
$ \c --> b
mcmb -> ((b --> a) -> a r) -> b r
a -/-> b
ab (((b --> a) -> a r) -> b r) -> ((b --> a) -> a r) -> b r
forall a b. (a -> b) -> a -> b
$ \b --> a
mbma -> (c --> a) -> a r
f ((c --> a) -> a r) -> (c --> a) -> a r
forall a b. (a -> b) -> a -> b
$ b a -> a a
b --> a
mbma (b a -> a a) -> (c a -> b a) -> c a -> a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c a -> b a
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) = (ma --> mb) -> WRaised ma mb
forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised ((ma --> mb) -> WRaised ma mb) -> (ma --> mb) -> WRaised ma mb
forall a b. (a -> b) -> a -> b
$ (ma -/-> mb) -> ma --> mb
forall {k} (ma :: k -> Type) (mb :: k -> Type).
(ma -/-> mb) -> ma --> mb
backraisedToRaised ((mb --> ma) -> ma r) -> mb r
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) = (t m --> m) -> WRaised (t m) m
forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised t m a -> m a
t m --> m
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
    }