Portability | non-portable (class-associated types) |
---|---|
Stability | experimental |
Maintainer | Edward Kmett <ekmett@gmail.com> |
- class (Associative k (Product k), Disassociative k (Product k), Symmetric k (Product k), Braided k (Product k)) => PreCartesian k where
- bimapProduct :: (PreCartesian k, <*> ~ Product k) => (a `k` c) -> (b `k` d) -> (a <*> b) `k` (c <*> d)
- braidProduct :: PreCartesian k => Product k a b `k` Product k b a
- associateProduct :: PreCartesian k => Product k (Product k a b) c `k` Product k a (Product k b c)
- disassociateProduct :: PreCartesian k => Product k a (Product k b c) `k` Product k (Product k a b) c
- class (Associative k (Sum k), Disassociative k (Sum k), Symmetric k (Product k), Braided k (Sum k)) => PreCoCartesian k where
- bimapSum :: (PreCoCartesian k, Sum k ~ +) => (a `k` c) -> (b `k` d) -> (a + b) `k` (c + d)
- braidSum :: (PreCoCartesian k, + ~ Sum k) => (a + b) `k` (b + a)
- associateSum :: PreCoCartesian k => Sum k (Sum k a b) c `k` Sum k a (Sum k b c)
- disassociateSum :: PreCoCartesian k => Sum k a (Sum k b c) `k` Sum k (Sum k a b) c
- class (Monoidal k (Product k), PreCartesian k) => Cartesian k
- class (Comonoidal k (Sum k), PreCoCartesian k) => CoCartesian k
Pre-(Co)Cartesian categories
class (Associative k (Product k), Disassociative k (Product k), Symmetric k (Product k), Braided k (Product k)) => PreCartesian k whereSource
NB: This is weaker than traditional category with products! That is Cartesian, below.
The problem is (->)
lacks an initial object, since every type is inhabited in Haskell.
Consequently its coproduct is merely a semigroup, not a monoid (as it has no identity), and
since we want to be able to describe its dual category, which has this non-traditional
form being built over a category with an associative bifunctor rather than as a monoidal category
for the product monoid.
Minimum definition:
fst, snd, diag fst, snd, (&&&)
fst :: Product k a b `k` aSource
snd :: Product k a b `k` bSource
diag :: a `k` Product k a aSource
(&&&) :: (a `k` b) -> (a `k` c) -> a `k` Product k b cSource
PreCartesian (->) |
bimapProduct :: (PreCartesian k, <*> ~ Product k) => (a `k` c) -> (b `k` d) -> (a <*> b) `k` (c <*> d)Source
braidProduct :: PreCartesian k => Product k a b `k` Product k b aSource
associateProduct :: PreCartesian k => Product k (Product k a b) c `k` Product k a (Product k b c)Source
disassociateProduct :: PreCartesian k => Product k a (Product k b c) `k` Product k (Product k a b) cSource
class (Associative k (Sum k), Disassociative k (Sum k), Symmetric k (Product k), Braided k (Sum k)) => PreCoCartesian k whereSource
PreCoCartesian (->) |
bimapSum :: (PreCoCartesian k, Sum k ~ +) => (a `k` c) -> (b `k` d) -> (a + b) `k` (c + d)Source
braidSum :: (PreCoCartesian k, + ~ Sum k) => (a + b) `k` (b + a)Source
associateSum :: PreCoCartesian k => Sum k (Sum k a b) c `k` Sum k a (Sum k b c)Source
free construction of Associative
for the coproduct Bifunctor
Sum k
associateSum :: (PreCoCartesian k, (+) ~ Sum k) => ((a + b) + c) ~> (a + (b + c))
disassociateSum :: PreCoCartesian k => Sum k a (Sum k b c) `k` Sum k (Sum k a b) cSource
free construction of Disassociative
for the coproduct Bifunctor
Sum k
disassociateSum :: (PreCoCartesian k, (+) ~ Sum k) => (a + (b + c)) ~> ((a + b) + c)
(Co)Cartesian categories
class (Monoidal k (Product k), PreCartesian k) => Cartesian k Source
(Monoidal k (Product k), PreCartesian k) => Cartesian k |
class (Comonoidal k (Sum k), PreCoCartesian k) => CoCartesian k Source
(Comonoidal k (Sum k), PreCoCartesian k) => CoCartesian k |