{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, PolyKinds, NoImplicitPrelude #-}
module Data.Category (
Category(..)
, Obj
, Kind
, Op(..)
) where
infixr 8 .
type Obj k a = k a a
class Category k where
src :: k a b -> Obj k a
tgt :: k a b -> Obj k b
(.) :: k b c -> k a b -> k a c
instance Category (->) where
src :: (a -> b) -> Obj (->) a
src a -> b
_ = \a
x -> a
x
tgt :: (a -> b) -> Obj (->) b
tgt a -> b
_ = \b
x -> b
x
b -> c
f . :: (b -> c) -> (a -> b) -> a -> c
. a -> b
g = \a
x -> b -> c
f (a -> b
g a
x)
newtype Op k a b = Op { Op k a b -> k b a
unOp :: k b a }
instance Category k => Category (Op k) where
src :: Op k a b -> Obj (Op k) a
src (Op k b a
a) = k a a -> Obj (Op k) a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k b a -> k a a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k b a
a)
tgt :: Op k a b -> Obj (Op k) b
tgt (Op k b a
a) = k b b -> Obj (Op k) b
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k b a -> k b b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k b a
a)
(Op k c b
a) . :: Op k b c -> Op k a b -> Op k a c
. (Op k b a
b) = k c a -> Op k a c
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k b a
b k b a -> k c b -> k c a
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k c b
a)
type Kind (cat :: k -> k -> *) = k