module Control.Monad.Ology.General.Function
( TransKind
, Raised
, type (-->)
, WRaised(..)
, wLift
, wLiftIO
, Backraised
, type (-/->)
, backraisedToRaised
, WBackraised(..)
, wBackraisedToWRaised
, Unlift
, WUnlift(..)
, wUnliftToWRaised
, 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 m = forall a. m a -> a
type WExtract :: (Type -> Type) -> Type
newtype m =
{ :: Extract m
}