Product Category

{-# LANGUAGE TypeFamilies, ConstraintKinds, GADTs, ScopedTypeVariables #-}
module CCC where
import GHC.Exts (Constraint)

data Uncurried x y where
  Uncurried :: (a -> c) -> (b -> d) -> Uncurried (a,b) (c,d)

data IsPairPf a where IsPairPf :: IsPairPf (x,y)

class IsPair a where
    isPairPf :: IsPairPf a

class RCat cat where
    type CatElt cat a :: Constraint

    cid :: CatElt cat a => cat a a
    (!) :: (CatElt cat a, CatElt cat b, CatElt cat c) => cat b c -> cat a b -> cat a c

idUncurried :: IsPairPf a -> Uncurried a a
idUncurried IsPairPf = Uncurried id id

compUncurried :: Uncurried b c -> Uncurried a b -> Uncurried a c
compUncurried (Uncurried f1 f2) (Uncurried g1 g2) = Uncurried (f1 . g1) (f2 . g2)

instance RCat Uncurried where
    type CatElt Uncurried a  = IsPair a
    cid = idUncurried isPairPf
    (!) = compUncurried