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(..)
, ProductFunctor(..)
, (:*:)(..)
, BinaryCoproduct
, HasBinaryCoproducts(..)
, CoproductFunctor(..)
, (:+:)(..)
, ForAll(..)
, endoHaskLimit
, Exists(..)
, endoHaskColimit
) where
import Prelude hiding ((.), 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.Product
import Data.Category.Coproduct
import Data.Category.Discrete
infixl 3 ***
infixl 3 &&&
infixl 2 +++
infixl 2 |||
data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
Diag :: Diag j (~>)
type instance Dom (Diag j (~>)) = (~>)
type instance Cod (Diag j (~>)) = Nat j (~>)
type instance Diag j (~>) :% a = Const j (~>) a
instance (Category j, Category (~>)) => Functor (Diag j (~>)) where
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 (Category j, Category (~>)) => Functor (LimitFunctor j (~>)) where
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 (Category j, Category (~>)) => Functor (ColimitFunctor j (~>)) where
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 (Nat f _ _) = limitUniversal
(voidNat (Const terminalObject) f)
(terminate . coneVertex)
instance HasTerminalObject (->) where
type TerminalObject (->) = ()
terminalObject = id
terminate _ _ = ()
instance HasTerminalObject Cat where
type TerminalObject Cat = CatW Unit
terminalObject = CatA Id
terminate (CatA _) = CatA $ Const Z
instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) where
type TerminalObject (Nat c d) = Const c d (TerminalObject d)
terminalObject = natId $ Const terminalObject
terminate (Nat f _ _) = Nat f (Const terminalObject) $ terminate . (f %)
instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) where
type TerminalObject (c1 :**: c2) = (TerminalObject c1, TerminalObject c2)
terminalObject = terminalObject :**: terminalObject
terminate (a1 :**: a2) = terminate a1 :**: terminate a2
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 (Nat f _ _) = colimitUniversal
(voidNat f (Const initialObject))
(initialize . coconeVertex)
data Zero
instance HasInitialObject (->) where
type InitialObject (->) = Zero
initialObject = id
initialize _ x = x `seq` error "we never get this far"
instance HasInitialObject Cat where
type InitialObject Cat = CatW Void
initialObject = CatA Id
initialize (CatA _) = CatA Nil
instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d) where
type InitialObject (Nat c d) = Const c d (InitialObject d)
initialObject = natId $ Const initialObject
initialize (Nat f _ _) = Nat (Const initialObject) f $ initialize . (f %)
instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) where
type InitialObject (c1 :**: c2) = (InitialObject c1, InitialObject c2)
initialObject = initialObject :**: initialObject
initialize (a1 :**: a2) = initialize a1 :**: initialize a2
type family BinaryProduct ((~>) :: * -> * -> *) x y :: *
class Category (~>) => HasBinaryProducts (~>) where
proj1 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> x
proj2 :: Obj (~>) x -> Obj (~>) y -> 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 (src l) (src r)) &&& (r . proj2 (src l) (src r)) where
type instance LimitFam (Discrete (S n)) (~>) f = BinaryProduct (~>) (f :% Z) (LimitFam (Discrete n) (~>) (Next f))
instance (HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) => HasLimits (Discrete (S n)) (~>) where
limitUniv (Nat l _ _) = limitUniv' l
where
limitUniv' :: forall f. (Functor f, Dom f ~ Discrete (S n), Cod f ~ (~>), HasLimits (Discrete n) (~>), HasBinaryProducts (~>))
=> f -> LimitUniversal f
limitUniv' f = limitUniversal
(Nat (Const $ x *** y) f (\z -> unCom $ h z))
(\c -> c ! Z &&& limitFactorizer luNext (Nat (Const $ coneVertex c) (Next f) $ \n -> c ! S n))
where
x = f % Z
y = coneVertex limNext
limNext = limit luNext
luNext = limitUniv (natId (Next f))
h :: Obj (Discrete (S n)) z -> Com (ConstF f (LimitFam (Discrete (S n)) (~>) f)) f z
h Z = Com $ proj1 x y
h (S n) = Com $ limNext ! n . proj2 x y
type instance BinaryProduct (->) x y = (x, y)
instance HasBinaryProducts (->) where
proj1 _ _ = fst
proj2 _ _ = snd
(&&&) = (A.&&&)
(***) = (A.***)
type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)
instance HasBinaryProducts Cat where
proj1 (CatA _) (CatA _) = CatA Proj1
proj2 (CatA _) (CatA _) = CatA Proj2
CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)
CatA f1 *** CatA f2 = CatA (f1 :***: f2)
type instance BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)
instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where
proj1 (x1 :**: x2) (y1 :**: y2) = proj1 x1 y1 :**: proj1 x2 y2
proj2 (x1 :**: x2) (y1 :**: y2) = proj2 x1 y1 :**: proj2 x2 y2
(f1 :**: f2) &&& (g1 :**: g2) = (f1 &&& g1) :**: (f2 &&& g2)
(f1 :**: f2) *** (g1 :**: g2) = (f1 *** g1) :**: (f2 *** g2)
data ProductFunctor ((~>) :: * -> * -> *) = ProductFunctor
type instance Dom (ProductFunctor (~>)) = (~>) :**: (~>)
type instance Cod (ProductFunctor (~>)) = (~>)
type instance ProductFunctor (~>) :% (a, b) = BinaryProduct (~>) a b
instance HasBinaryProducts (~>) => Functor (ProductFunctor (~>)) where
ProductFunctor % (a1 :**: a2) = a1 *** a2
data p :*: q where
(:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryProducts (~>)) => p -> q -> p :*: q
type instance Dom (p :*: q) = Dom p
type instance Cod (p :*: q) = Cod p
type instance (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)
instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q) where
(p :*: q) % f = (p % f) *** (q % f)
type instance BinaryProduct (Nat c d) x y = x :*: y
instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where
proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f $ \z -> proj1 (f % z) (g % z)
proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g $ \z -> proj2 (f % z) (g % z)
Nat a f af &&& Nat _ g ag = Nat a (f :*: g) $ \z -> af z &&& ag z
Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) $ \z -> f z *** g z
type family BinaryCoproduct ((~>) :: * -> * -> *) x y :: *
class Category (~>) => HasBinaryCoproducts (~>) where
inj1 :: Obj (~>) x -> Obj (~>) y -> x ~> BinaryCoproduct (~>) x y
inj2 :: Obj (~>) x -> Obj (~>) 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 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r) where
type instance ColimitFam (Discrete (S n)) (~>) f = BinaryCoproduct (~>) (f :% Z) (ColimitFam (Discrete n) (~>) (Next f))
instance (HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) => HasColimits (Discrete (S n)) (~>) where
colimitUniv (Nat l _ _) = colimitUniv' l
where
colimitUniv' :: forall f. (Functor f, Dom f ~ Discrete (S n), Cod f ~ (~>), HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>))
=> f -> ColimitUniversal f
colimitUniv' f = colimitUniversal
(Nat f (Const $ x +++ y) (\z -> unCom $ h z))
(\c -> c ! Z ||| colimitFactorizer cluNext (Nat (Next f) (Const $ coconeVertex c) $ \n -> c ! S n))
where
x = f % Z
y = coconeVertex colNext
colNext = colimit cluNext
cluNext = colimitUniv (natId (Next f))
h :: Obj (Discrete (S n)) z -> Com f (ConstF f (ColimitFam (Discrete (S n)) (~>) f)) z
h Z = Com $ inj1 x y
h (S n) = Com $ inj2 x y . colNext ! n
type instance BinaryCoproduct (->) x y = Either x y
instance HasBinaryCoproducts (->) where
inj1 _ _ = Left
inj2 _ _ = Right
(|||) = (A.|||)
(+++) = (A.+++)
type instance BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)
instance HasBinaryCoproducts Cat where
inj1 (CatA _) (CatA _) = CatA Inj1
inj2 (CatA _) (CatA _) = CatA Inj2
CatA f1 ||| CatA f2 = CatA (CodiagCoprod :.: (f1 :+++: f2))
CatA f1 +++ CatA f2 = CatA (f1 :+++: f2)
type instance BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)
instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where
inj1 (x1 :**: x2) (y1 :**: y2) = inj1 x1 y1 :**: inj1 x2 y2
inj2 (x1 :**: x2) (y1 :**: y2) = inj2 x1 y1 :**: inj2 x2 y2
(f1 :**: f2) ||| (g1 :**: g2) = (f1 ||| g1) :**: (f2 ||| g2)
(f1 :**: f2) +++ (g1 :**: g2) = (f1 +++ g1) :**: (f2 +++ g2)
data CoproductFunctor ((~>) :: * -> * -> *) = CoproductFunctor
type instance Dom (CoproductFunctor (~>)) = (~>) :**: (~>)
type instance Cod (CoproductFunctor (~>)) = (~>)
type instance CoproductFunctor (~>) :% (a, b) = BinaryCoproduct (~>) a b
instance HasBinaryCoproducts (~>) => Functor (CoproductFunctor (~>)) where
CoproductFunctor % (a1 :**: a2) = a1 +++ a2
data p :+: q where
(:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryCoproducts (~>)) => p -> q -> p :+: q
type instance Dom (p :+: q) = Dom p
type instance Cod (p :+: q) = Cod p
type instance (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)
instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q) where
(p :+: q) % f = (p % f) +++ (q % f)
type instance BinaryCoproduct (Nat c d) x y = x :+: y
instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where
inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) $ \z -> inj1 (f % z) (g % z)
inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) $ \z -> inj2 (f % z) (g % z)
Nat f a fa ||| Nat g _ ga = Nat (f :+: g) a $ \z -> fa z ||| ga z
Nat f1 f2 f +++ Nat g1 g2 g = Nat (f1 :+: g1) (f2 :+: g2) $ \z -> f z +++ g z
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 id) EndoHask $ \_ -> unForAll)
(\c n -> ForAll ((c ! id) 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 id) $ \_ -> Exists)
(\c (Exists fa) -> (c ! id) fa)