Kind-polymorphic Category

Categories.hs

{-# LANGUAGE PolyKinds, KindSignatures, TypeOperators, TypeFamilies #-}
{-# LANGUAGE ConstraintKinds, GADTs, RankNTypes #-}
module Categories where
import qualified Prelude
import GHC.Prim (Constraint)

--------------------------------------------------------------------------------
-- Kind-polymorphic Category

class Category cat where
  -- inferred: 'cat :: k -> k -> *'
  id  :: cat a a
  (.) :: cat b c -> cat a b -> cat a c

instance Category (->) where
  id  = Prelude.id
  (.) = (Prelude..)

--------------------------------------------------------------------------------
-- Logical entailment

data Dict :: Constraint -> * where
  Dict :: ctx => Dict ctx

newtype (|-) a b = Sub (a => Dict b)

(\\) :: a => (b => r) -> (a |- b) -> r
r \\ Sub Dict = r

reflexive :: a |- a
reflexive = Sub Dict

transitive :: (b |- c) -> (a |- b) -> (a |- c)
transitive f g = Sub (Dict \\ f \\ g)

instance Category (|-) where
  id  = reflexive
  (.) = transitive