{-# LANGUAGE KindSignatures #-}
{- |
Basic definitions in the category @(* -> *)@.
-}
module Control.Monad.Trans.Category ((:->), (:$)(..), (:.)(..), Inst) where
-- | @m :-> n@ is the set of morphisms (from @m@ to @n@, naturally) in our category.
type m :-> n = forall a. m a -> n a
-- | If @m@ is an algebra over an endofunctor @t@, then it's structure morphism has the type @Inst t m@.
type Inst c m = c m :-> m
infixr 0 :$
-- | If @t@ is an endofunctor in our category, then @t :$ m@ is basically the same as @t m@.
newtype (t :$ (m :: * -> *)) a = ApplyF {runApplyF :: t m a}
infixr 9 :.
-- | If @t1@ and @t2@ are endofunctorsm then @t2 :. t1@ is their composition (which is also an endofunctor)
newtype (t2 :. t1) m a = ComposeF {runComposeF :: (t2 :$ (t1 :$ m)) a}