Kind-indexed categories with kind-tagging

CatTagged.hs

{-# LANGUAGE 
    GADTs
  , MultiParamTypeClasses
  , RankNTypes
  , TypeApplications
  , TypeFamilies
  , TypeOperators
  , PolyKinds
  , DataKinds
  , InstanceSigs
  , TypeSynonymInstances
  , ScopedTypeVariables
  , FlexibleInstances
  , UndecidableInstances
  , UndecidableSuperClasses 
  #-}
import Prelude hiding (id, (.), Functor(..))
import GHC.Types (Type, Constraint, Any)
import Control.Monad (Monad, (<=<), return)
import Data.Constraint


class Empty a
instance Empty a

type Cat obj = obj -> obj -> Type
class Category (obj :: Type) where
  type (-->) :: Cat obj
  type Ob :: obj -> Constraint
  type Ob = Empty
  id :: Ob (a :: obj) => a --> a
  (.) :: (b --> c) -> (a --> b) -> (a --> (c :: obj))


class (Category src, Category tgt) => Functor (f :: src -> tgt) where
  omap :: Ob a :- Ob (f a)
  fmap :: (a --> b) -> (f a --> f b)


instance Category Type where
  type (-->) = (->)
  id x = x
  f . g = \x -> f (g x)


newtype (~>) :: Cat (src -> tgt) where
  Nat :: (forall a. Ob a => f a --> g a) -> (f ~> g)
instance Category tgt => Category (src -> tgt) where
  type (-->) = (~>)
  type Ob = Functor
  id :: forall f. Functor (f :: src -> tgt) => f ~> f
  id = nat $ \(_ :: Any a) -> id \\ omap @src @tgt @f @a
  Nat m . Nat n = Nat (m . n)

nat :: forall f g. (forall a. Ob a => Any a -> f a --> g a) -> f ~> g
nat f = Nat (f (undefined :: Any a) :: forall a. Ob a => f a --> g a)


instance Category Constraint where
  type (-->) = (:-)
  id = refl
  (.) = trans


data Hom obj :: Op obj -> obj -> Type where
  Hom :: (a --> b) -> Hom obj ('Tag a) b
instance (Category obj, Ob a) => Functor (Hom obj a) where
  omap = Sub Dict
  fmap f (Hom g) = Hom (f . g)
instance Category obj => Functor (Hom obj) where
  omap = Sub Dict
  fmap (Op f) = Nat $ \(Hom g) -> Hom (g . f)


data (*->) :: Cat (ob1, ob2) where
  (:*:) :: (a1 --> b1) -> (a2 --> b2) -> ('(a1, a2) *-> '(b1, b2))

type family Fst (pair :: (a, b)) :: a where Fst '(a, b) = a
type family Snd (pair :: (a, b)) :: b where Fst '(a, b) = b
class    (p ~ '(Fst p, Snd p), Ob (Fst p), Ob (Snd p)) => IsPair p
instance (p ~ '(Fst p, Snd p), Ob (Fst p), Ob (Snd p)) => IsPair p

instance (Category ob1, Category ob2) => Category (ob1, ob2) where
  type (-->) = (*->)
  type Ob = IsPair
  id = id :*: id
  (f1 :*: f2) . (g1 :*: g2) = (f1 . g1) :*: (f2 . g2)


data (+->) :: Cat (Either obl obr) where
  Inl :: (a --> b) -> 'Left a +-> 'Left b
  Inr :: (a --> b) -> 'Right a +-> 'Right b

class IsEither (e :: Either obl obr) where eitherId :: e --> e
instance Category obl => IsEither ('Left obl) where eitherId = Inl id
instance Category obr => IsEither ('Right obr) where eitherId = Inr id

instance (Category obl, Category obr) => Category (Either obl obr) where
  type (-->) = (+->)
  type Ob = IsEither
  id = eitherId
  Inl f . Inl g = Inl (f . g)
  Inr f . Inr g = Inr (f . g)


data Boolean :: Cat Bool where
  Fls :: Boolean 'False 'False
  F2T :: Boolean 'False 'True
  Tru :: Boolean 'True 'True
class IsBool (b :: Bool) where boolId :: b --> b
instance IsBool 'False where boolId = Fls
instance IsBool 'True where boolId = Tru
instance Category Bool where
  type (-->) = Boolean
  type Ob = IsBool
  id = boolId
  Fls . Fls = Fls
  F2T . Fls = F2T
  Tru . F2T = F2T
  Tru . Tru = Tru


data Tagged tag a = Tag a
type family Untag (tagged :: Tagged tag a) :: a where Untag ('Tag a) = a
class    t ~ 'Tag (Untag t) => IsTagged t
instance t ~ 'Tag (Untag t) => IsTagged t
  
class    (IsTagged t, Ob (Untag t)) => IsTaggedOb t
instance (IsTagged t, Ob (Untag t)) => IsTaggedOb t


data OpTag
type Op = Tagged OpTag
data (<--) :: Cat (Tagged OpTag ob) where
  Op :: (a --> b) -> 'Tag b <-- 'Tag a

instance Category ob => Category (Tagged OpTag ob) where
  type (-->) = ((<--) :: Cat (Tagged OpTag ob))
  type Ob = IsTaggedOb
  id = Op id
  Op f . Op g = Op (g . f)


data KleisliTag m
data Kleisli m :: Cat (Tagged (KleisliTag m) Type) where
  MkKleisli :: (a -> m b) -> Kleisli m ('Tag a) ('Tag b)

instance Monad m => Category (Tagged (KleisliTag m) Type) where
  type (-->) = (Kleisli m :: Cat (Tagged (KleisliTag m) Type))
  type Ob = IsTagged
  id = MkKleisli return
  MkKleisli f . MkKleisli g = MkKleisli (f <=< g)


-- data CatTag
-- data CAT :: Cat (Tagged CatTag Type) where
--   SomeFunctor :: (forall a b. (a --> b) -> (f :: src -> tgt) a --> f b) -> CAT ('Tag src) ('Tag tgt)
-- instance Category (Tagged CatTag Type) where
--   type (-->) = (CAT :: Cat (Tagged CatTag Type))
--   type Ob = IsTagged
--   id = SomeFunctor _
--   SomeFunctor f . SomeFunctor g = SomeFunctor _