{-# LANGUAGE PolyKinds, TypeOperators, TypeFamilies, PatternSynonyms, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-}
module Data.Category.Functor (
Cat(..)
, Functor(..)
, FunctorOf
, Id(..)
, (:.:)(..)
, Const(..), ConstF
, Opposite(..)
, OpOp(..)
, OpOpInv(..)
, Proj1(..)
, Proj2(..)
, (:***:)(..)
, DiagProd(..)
, Tuple1, pattern Tuple1
, Tuple2, pattern Tuple2
, Swap, pattern Swap
, Hom(..)
, (:*-:), pattern HomX_
, (:-*:), pattern Hom_X
, HomF, pattern HomF
, Star, pattern Star
, Costar, pattern Costar
) where
import Data.Category
import Data.Category.Product
infixr 9 %
infixr 9 :%
class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where
type Dom ftag :: * -> * -> *
type Cod ftag :: * -> * -> *
type ftag :% a :: *
(%) :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
type FunctorOf a b t = (Functor t, Dom t ~ a, Cod t ~ b)
data Cat :: (* -> * -> *) -> (* -> * -> *) -> * where
CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (Dom ftag) (Cod ftag)
instance Category Cat where
src :: Cat a b -> Obj Cat a
src (CatA ftag
_) = Id a -> Cat (Dom (Id a)) (Cod (Id a))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Id a
forall (k :: * -> * -> *). Id k
Id
tgt :: Cat a b -> Obj Cat b
tgt (CatA ftag
_) = Id b -> Cat (Dom (Id b)) (Cod (Id b))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Id b
forall (k :: * -> * -> *). Id k
Id
CatA ftag
f1 . :: Cat b c -> Cat a b -> Cat a c
. CatA ftag
f2 = (ftag :.: ftag) -> Cat (Dom (ftag :.: ftag)) (Cod (ftag :.: ftag))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (ftag
f1 ftag -> ftag -> ftag :.: ftag
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: ftag
f2)
data Id (k :: * -> * -> *) = Id
instance Category k => Functor (Id k) where
type Dom (Id k) = k
type Cod (Id k) = k
type Id k :% a = a
Id k
_ % :: Id k -> Dom (Id k) a b -> Cod (Id k) (Id k :% a) (Id k :% b)
% Dom (Id k) a b
f = Dom (Id k) a b
Cod (Id k) (Id k :% a) (Id k :% b)
f
data (g :.: h) where
(:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h
instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where
type Dom (g :.: h) = Dom h
type Cod (g :.: h) = Cod g
type (g :.: h) :% a = g :% (h :% a)
(g
g :.: h
h) % :: (g :.: h)
-> Dom (g :.: h) a b
-> Cod (g :.: h) ((g :.: h) :% a) ((g :.: h) :% b)
% Dom (g :.: h) a b
f = g
g g
-> Dom g (h :% a) (h :% b) -> Cod g (g :% (h :% a)) (g :% (h :% b))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (h
h h -> Dom h a b -> Cod h (h :% a) (h :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom h a b
Dom (g :.: h) a b
f)
data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
Const :: Obj c2 x -> Const c1 c2 x
instance (Category c1, Category c2) => Functor (Const c1 c2 x) where
type Dom (Const c1 c2 x) = c1
type Cod (Const c1 c2 x) = c2
type Const c1 c2 x :% a = x
Const Obj c2 x
x % :: Const c1 c2 x
-> Dom (Const c1 c2 x) a b
-> Cod (Const c1 c2 x) (Const c1 c2 x :% a) (Const c1 c2 x :% b)
% Dom (Const c1 c2 x) a b
_ = Obj c2 x
Cod (Const c1 c2 x) (Const c1 c2 x :% a) (Const c1 c2 x :% b)
x
type ConstF f = Const (Dom f) (Cod f)
data Opposite f where
Opposite :: Functor f => f -> Opposite f
instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where
type Dom (Opposite f) = Op (Dom f)
type Cod (Opposite f) = Op (Cod f)
type Opposite f :% a = f :% a
Opposite f
f % :: Opposite f
-> Dom (Opposite f) a b
-> Cod (Opposite f) (Opposite f :% a) (Opposite f :% b)
% Op a = Cod f (f :% b) (f :% a) -> Op (Cod f) (f :% a) (f :% b)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (f
f f -> Dom f b a -> Cod f (f :% b) (f :% a)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f b a
a)
data OpOp (k :: * -> * -> *) = OpOp
instance Category k => Functor (OpOp k) where
type Dom (OpOp k) = Op (Op k)
type Cod (OpOp k) = k
type OpOp k :% a = a
OpOp k
OpOp % :: OpOp k
-> Dom (OpOp k) a b -> Cod (OpOp k) (OpOp k :% a) (OpOp k :% b)
% Op (Op f) = k a b
Cod (OpOp k) (OpOp k :% a) (OpOp k :% b)
f
data OpOpInv (k :: * -> * -> *) = OpOpInv
instance Category k => Functor (OpOpInv k) where
type Dom (OpOpInv k) = k
type Cod (OpOpInv k) = Op (Op k)
type OpOpInv k :% a = a
OpOpInv k
OpOpInv % :: OpOpInv k
-> Dom (OpOpInv k) a b
-> Cod (OpOpInv k) (OpOpInv k :% a) (OpOpInv k :% b)
% Dom (OpOpInv k) a b
f = Op k b a -> Op (Op k) a b
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k a b -> Op k b a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k a b
Dom (OpOpInv k) a b
f)
data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1
instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where
type Dom (Proj1 c1 c2) = c1 :**: c2
type Cod (Proj1 c1 c2) = c1
type Proj1 c1 c2 :% (a1, a2) = a1
Proj1 c1 c2
Proj1 % :: Proj1 c1 c2
-> Dom (Proj1 c1 c2) a b
-> Cod (Proj1 c1 c2) (Proj1 c1 c2 :% a) (Proj1 c1 c2 :% b)
% (f1 :**: _) = c1 a1 b1
Cod (Proj1 c1 c2) (Proj1 c1 c2 :% a) (Proj1 c1 c2 :% b)
f1
data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2
instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where
type Dom (Proj2 c1 c2) = c1 :**: c2
type Cod (Proj2 c1 c2) = c2
type Proj2 c1 c2 :% (a1, a2) = a2
Proj2 c1 c2
Proj2 % :: Proj2 c1 c2
-> Dom (Proj2 c1 c2) a b
-> Cod (Proj2 c1 c2) (Proj2 c1 c2 :% a) (Proj2 c1 c2 :% b)
% (_ :**: f2) = c2 a2 b2
Cod (Proj2 c1 c2) (Proj2 c1 c2 :% a) (Proj2 c1 c2 :% b)
f2
data f1 :***: f2 where (:***:) :: (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2
instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where
type Dom (f1 :***: f2) = Dom f1 :**: Dom f2
type Cod (f1 :***: f2) = Cod f1 :**: Cod f2
type (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)
(f1
g1 :***: f2
g2) % :: (f1 :***: f2)
-> Dom (f1 :***: f2) a b
-> Cod (f1 :***: f2) ((f1 :***: f2) :% a) ((f1 :***: f2) :% b)
% (f1 :**: f2) = (f1
g1 f1 -> Dom f1 a1 b1 -> Cod f1 (f1 :% a1) (f1 :% b1)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f1 a1 b1
f1) Cod f1 (f1 :% a1) (f1 :% b1)
-> Cod f2 (f2 :% a2) (f2 :% b2)
-> (:**:)
(Cod f1) (Cod f2) (f1 :% a1, f2 :% a2) (f1 :% b1, f2 :% b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (f2
g2 f2 -> Dom f2 a2 b2 -> Cod f2 (f2 :% a2) (f2 :% b2)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f2 a2 b2
f2)
data DiagProd (k :: * -> * -> *) = DiagProd
instance Category k => Functor (DiagProd k) where
type Dom (DiagProd k) = k
type Cod (DiagProd k) = k :**: k
type DiagProd k :% a = (a, a)
DiagProd k
DiagProd % :: DiagProd k
-> Dom (DiagProd k) a b
-> Cod (DiagProd k) (DiagProd k :% a) (DiagProd k :% b)
% Dom (DiagProd k) a b
f = k a b
Dom (DiagProd k) a b
f k a b -> k a b -> (:**:) k k (a, a) (b, b)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: k a b
Dom (DiagProd k) a b
f
type Tuple1 c1 c2 a = (Const c2 c1 a :***: Id c2) :.: DiagProd c2
pattern Tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a
pattern $bTuple1 :: Obj c1 a -> Tuple1 c1 c2 a
$mTuple1 :: forall r (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Tuple1 c1 c2 a -> (Obj c1 a -> r) -> (Void# -> r) -> r
Tuple1 a = (Const a :***: Id) :.: DiagProd
type Swap (c1 :: * -> * -> *) (c2 :: * -> * -> *) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)
pattern Swap :: (Category c1, Category c2) => Swap c1 c2
pattern $bSwap :: Swap c1 c2
$mSwap :: forall r (c1 :: * -> * -> *) (c2 :: * -> * -> *).
(Category c1, Category c2) =>
Swap c1 c2 -> (Void# -> r) -> (Void# -> r) -> r
Swap = (Proj2 :***: Proj1) :.: DiagProd
type Tuple2 c1 c2 a = Swap c2 c1 :.: Tuple1 c2 c1 a
pattern Tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a
pattern $bTuple2 :: Obj c2 a -> Tuple2 c1 c2 a
$mTuple2 :: forall r (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Tuple2 c1 c2 a -> (Obj c2 a -> r) -> (Void# -> r) -> r
Tuple2 a = Swap :.: Tuple1 a
data Hom (k :: * -> * -> *) = Hom
instance Category k => Functor (Hom k) where
type Dom (Hom k) = Op k :**: k
type Cod (Hom k) = (->)
type (Hom k) :% (a1, a2) = k a1 a2
Hom k
Hom % :: Hom k -> Dom (Hom k) a b -> Cod (Hom k) (Hom k :% a) (Hom k :% b)
% (Op f1 :**: f2) = \k a1 a2
g -> k a2 b2
f2 k a2 b2 -> k b1 a2 -> k b1 b2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k a1 a2
g k a1 a2 -> k b1 a1 -> k b1 a2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k b1 a1
f1
type x :*-: k = Hom k :.: Tuple1 (Op k) k x
pattern HomX_ :: Category k => Obj k x -> x :*-: k
pattern $bHomX_ :: Obj k x -> x :*-: k
$mHomX_ :: forall r (k :: * -> * -> *) x.
Category k =>
(x :*-: k) -> (Obj k x -> r) -> (Void# -> r) -> r
HomX_ x = Hom :.: Tuple1 (Op x)
type k :-*: x = Hom k :.: Tuple2 (Op k) k x
pattern Hom_X :: Category k => Obj k x -> k :-*: x
pattern $bHom_X :: Obj k x -> k :-*: x
$mHom_X :: forall r (k :: * -> * -> *) x.
Category k =>
(k :-*: x) -> (Obj k x -> r) -> (Void# -> r) -> r
Hom_X x = Hom :.: Tuple2 x
type HomF f g = Hom (Cod f) :.: (Opposite f :***: g)
pattern HomF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g
pattern $bHomF :: f -> g -> HomF f g
$mHomF :: forall r f g.
(Functor f, Functor g, Cod f ~ Cod g) =>
HomF f g -> (f -> g -> r) -> (Void# -> r) -> r
HomF f g = Hom :.: (Opposite f :***: g)
type Star f = HomF (Id (Cod f)) f
pattern Star :: Functor f => f -> Star f
pattern $bStar :: f -> Star f
$mStar :: forall r f. Functor f => Star f -> (f -> r) -> (Void# -> r) -> r
Star f = HomF Id f
type Costar f = HomF f (Id (Cod f))
pattern Costar :: Functor f => f -> Costar f
pattern $bCostar :: f -> Costar f
$mCostar :: forall r f. Functor f => Costar f -> (f -> r) -> (Void# -> r) -> r
Costar f = HomF f Id