module Data.Category.Limit (
Diag(..)
, DiagF
, Cone
, Cocone
, coneVertex
, coconeVertex
, LimitFam
, Limit
, LimitUniversal
, limitUniversal
, limit
, limitFactorizer
, ColimitFam
, Colimit
, ColimitUniversal
, colimitUniversal
, colimit
, colimitFactorizer
, HasLimits(..)
, HasColimits(..)
, LimitFunctor(..)
, ColimitFunctor(..)
, HasTerminalObject(..)
, HasInitialObject(..)
, Zero
, BinaryProduct
, HasBinaryProducts(..)
, BinaryCoproduct
, HasBinaryCoproducts(..)
, ForAll(..)
, endoHaskLimit
, Exists(..)
, endoHaskColimit
) where
import Prelude hiding ((.), id, Functor, product)
import qualified Prelude (Functor)
import qualified Control.Arrow as A ((&&&), (***), (|||), (+++))
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Void
import Data.Category.Pair
import Data.Category.Unit
import Data.Category.Product
import Data.Category.Discrete
infixr 3 ***
infixr 3 &&&
infixr 2 +++
infixr 2 |||
data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
Diag :: (Category j, Category (~>)) => Diag j (~>)
type instance Dom (Diag j (~>)) = (~>)
type instance Cod (Diag j (~>)) = Nat j (~>)
type instance Diag j (~>) :% a = Const j (~>) a
instance Functor (Diag j (~>)) where
Diag %% x = NatO $ Const x
Diag % f = Nat (Const $ src f) (Const $ tgt f) $ const f
type DiagF f = Diag (Dom f) (Cod f)
type Cone f n = Nat (Dom f) (Cod f) (ConstF f n) f
type Cocone f n = Nat (Dom f) (Cod f) f (ConstF f n)
coneVertex :: Cone f n -> Obj (Cod f) n
coneVertex (Nat (Const x) _ _) = x
coconeVertex :: Cocone f n -> Obj (Cod f) n
coconeVertex (Nat _ (Const x) _) = x
type family LimitFam j (~>) f :: *
type Limit f = LimitFam (Dom f) (Cod f) f
type LimitUniversal f = TerminalUniversal f (DiagF f) (Limit f)
limitUniversal :: (Cod f ~ (~>))
=> Cone f (Limit f)
-> (forall n. Cone f n -> n ~> Limit f)
-> LimitUniversal f
limitUniversal l lf = TerminalUniversal
{ tuObject = coneVertex l
, terminalMorphism = l
, terminalFactorizer = const lf
}
limit :: LimitUniversal f -> Cone f (Limit f)
limit = terminalMorphism
limitFactorizer :: (Cod f ~ (~>)) => LimitUniversal f -> (forall n. Cone f n -> n ~> Limit f)
limitFactorizer lu c = terminalFactorizer lu (coneVertex c) c
type family ColimitFam j (~>) f :: *
type Colimit f = ColimitFam (Dom f) (Cod f) f
type ColimitUniversal f = InitialUniversal f (DiagF f) (Colimit f)
colimitUniversal :: (Cod f ~ (~>))
=> Cocone f (Colimit f)
-> (forall n. Cocone f n -> Colimit f ~> n)
-> ColimitUniversal f
colimitUniversal l lf = InitialUniversal
{ iuObject = coconeVertex l
, initialMorphism = l
, initialFactorizer = const lf
}
colimit :: ColimitUniversal f -> Cocone f (Colimit f)
colimit = initialMorphism
colimitFactorizer :: (Cod f ~ (~>)) => ColimitUniversal f -> (forall n. Cocone f n -> Colimit f ~> n)
colimitFactorizer cu c = initialFactorizer cu (coconeVertex c) c
class (Category j, Category (~>)) => HasLimits j (~>) where
limitUniv :: Obj (Nat j (~>)) f -> LimitUniversal f
data LimitFunctor :: (* -> * -> *) -> (* -> * -> *) -> * where
LimitFunctor :: HasLimits j (~>) => LimitFunctor j (~>)
type instance Dom (LimitFunctor j (~>)) = Nat j (~>)
type instance Cod (LimitFunctor j (~>)) = (~>)
type instance LimitFunctor j (~>) :% f = LimitFam j (~>) f
instance Functor (LimitFunctor j (~>)) where
LimitFunctor %% f @ NatO{} = tuObject (limitUniv f)
LimitFunctor % n @ Nat{} = limitFactorizer (limitUniv (tgt n)) (n . limit (limitUniv (src n)))
class (Category j, Category (~>)) => HasColimits j (~>) where
colimitUniv :: Obj (Nat j (~>)) f -> ColimitUniversal f
data ColimitFunctor :: (* -> * -> *) -> (* -> * -> *) -> * where
ColimitFunctor :: HasColimits j (~>) => ColimitFunctor j (~>)
type instance Dom (ColimitFunctor j (~>)) = Nat j (~>)
type instance Cod (ColimitFunctor j (~>)) = (~>)
type instance ColimitFunctor j (~>) :% f = ColimitFam j (~>) f
instance Functor (ColimitFunctor j (~>)) where
ColimitFunctor %% f @ NatO{} = iuObject (colimitUniv f)
ColimitFunctor % n @ Nat{} = colimitFactorizer (colimitUniv (src n)) (colimit (colimitUniv (tgt n)) . n)
class Category (~>) => HasTerminalObject (~>) where
type TerminalObject (~>) :: *
terminalObject :: Obj (~>) (TerminalObject (~>))
terminate :: Obj (~>) a -> a ~> TerminalObject (~>)
type instance LimitFam Void (~>) f = TerminalObject (~>)
instance (HasTerminalObject (~>)) => HasLimits Void (~>) where
limitUniv (NatO f) = limitUniversal
(voidNat (Const terminalObject) f)
(terminate . coneVertex)
instance HasTerminalObject (->) where
type TerminalObject (->) = ()
terminalObject = HaskO
terminate HaskO _ = ()
instance HasTerminalObject Cat where
type TerminalObject Cat = CatW Unit
terminalObject = CatO
terminate CatO = CatA $ Const UnitO
class Category (~>) => HasInitialObject (~>) where
type InitialObject (~>) :: *
initialObject :: Obj (~>) (InitialObject (~>))
initialize :: Obj (~>) a -> InitialObject (~>) ~> a
type instance ColimitFam Void (~>) f = InitialObject (~>)
instance HasInitialObject (~>) => HasColimits Void (~>) where
colimitUniv (NatO f) = colimitUniversal
(voidNat f (Const initialObject))
(initialize . coconeVertex)
data Zero
instance HasInitialObject (->) where
type InitialObject (->) = Zero
initialObject = HaskO
initialize HaskO x = x `seq` error "we never get this far"
instance HasInitialObject Cat where
type InitialObject Cat = CatW Void
initialObject = CatO
initialize CatO = CatA VoidDiagram
type family BinaryProduct ((~>) :: * -> * -> *) x y :: *
class Category (~>) => HasBinaryProducts (~>) where
product :: Obj (~>) x -> Obj (~>) y -> Obj (~>) (BinaryProduct (~>) x y)
proj :: Obj (~>) x -> Obj (~>) y -> (BinaryProduct (~>) x y ~> x, BinaryProduct (~>) x y ~> y)
(&&&) :: (a ~> x) -> (a ~> y) -> (a ~> BinaryProduct (~>) x y)
(***) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryProduct (~>) a1 a2 ~> BinaryProduct (~>) b1 b2)
l *** r = (l . proj1) &&& (r . proj2) where
(proj1, proj2) = proj (src l) (src r)
type instance LimitFam Pair (~>) f = BinaryProduct (~>) (f :% P1) (f :% P2)
instance HasBinaryProducts (~>) => HasLimits Pair (~>) where
limitUniv (NatO f) = limitUniversal
(pairNat (Const prod) f (Com $ fst prj) (Com $ snd prj))
(\c -> c ! Fst &&& c ! Snd)
where
x = f %% Fst
y = f %% Snd
prod = product x y
prj = proj x y
type instance BinaryProduct (->) x y = (x, y)
instance HasBinaryProducts (->) where
product HaskO HaskO = HaskO
proj _ _ = (fst, snd)
(&&&) = (A.&&&)
(***) = (A.***)
type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :*: c2)
instance HasBinaryProducts Cat where
product CatO CatO = CatO
proj CatO CatO = (CatA Proj1, CatA Proj2)
CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)
CatA f1 *** CatA f2 = CatA (f1 :***: f2)
type family BinaryCoproduct ((~>) :: * -> * -> *) x y :: *
class Category (~>) => HasBinaryCoproducts (~>) where
coproduct :: Obj (~>) x -> Obj (~>) y -> Obj (~>) (BinaryCoproduct (~>) x y)
inj :: Obj (~>) x -> Obj (~>) y -> (x ~> BinaryCoproduct (~>) x y, y ~> BinaryCoproduct (~>) x y)
(|||) :: (x ~> a) -> (y ~> a) -> (BinaryCoproduct (~>) x y ~> a)
(+++) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryCoproduct (~>) a1 a2 ~> BinaryCoproduct (~>) b1 b2)
l +++ r = (inj1 . l) ||| (inj2 . r) where
(inj1, inj2) = inj (tgt l) (tgt r)
type instance ColimitFam Pair (~>) f = BinaryCoproduct (~>) (f :% P1) (f :% P2)
instance HasBinaryCoproducts (~>) => HasColimits Pair (~>) where
colimitUniv (NatO f) = colimitUniversal
(pairNat f (Const cop) (Com $ fst i) (Com $ snd i))
(\c -> c ! Fst ||| c ! Snd)
where
x = f %% Fst
y = f %% Snd
cop = coproduct x y
i = inj x y
type instance BinaryCoproduct (->) x y = Either x y
instance HasBinaryCoproducts (->) where
coproduct HaskO HaskO = HaskO
inj _ _ = (Left, Right)
(|||) = (A.|||)
(+++) = (A.+++)
newtype ForAll f = ForAll { unForAll :: forall a. f a }
type instance LimitFam (->) (->) (EndoHask f) = ForAll f
endoHaskLimit :: Prelude.Functor f => LimitUniversal (EndoHask f)
endoHaskLimit = limitUniversal
(Nat (Const HaskO) EndoHask $ \HaskO -> unForAll)
(\c n -> ForAll ((c ! HaskO) n))
data Exists f = forall a. Exists (f a)
type instance ColimitFam (->) (->) (EndoHask f) = Exists f
endoHaskColimit :: Prelude.Functor f => ColimitUniversal (EndoHask f)
endoHaskColimit = colimitUniversal
(Nat EndoHask (Const HaskO) $ \HaskO -> Exists)
(\c (Exists fa) -> (c ! HaskO) fa)