Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- class (Associative cat t1, Associative cat t2, Associative cat to) => Semigroupal cat t1 t2 to f where
- combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y'))
- class Unital cat i1 i2 io f where
- introduce :: cat io (f i1 i2)
- class (Tensor cat t1 i1, Tensor cat t2 i2, Tensor cat to io, Semigroupal cat t1 t2 to f, Unital cat i1 i2 io f) => Monoidal cat t1 i1 t2 i2 to io f
Semigroupal
class (Associative cat t1, Associative cat t2, Associative cat to) => Semigroupal cat t1 t2 to f where Source #
Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\).
A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is Semigroupal
if it supports a
natural transformation \(\phi_{AB,CD} : F\ A\ B \bullet F\ C\ D \to F\ (A \otimes C)\ (B \otimes D)\), which we call combine
.
Laws
Associativity:
\[ \require{AMScd} \begin{CD} (F A B \bullet F C D) \bullet F X Y @>>{\alpha_{\mathcal{D}}}> F A B \bullet (F C D \bullet F X Y) \\ @VV{\phi_{AB,CD} \bullet 1}V @VV{1 \bullet \phi_{CD,FY}}V \\ F (A \otimes C) (B \otimes D) \bullet F X Y @. F A B \bullet (F (C \otimes X) (D \otimes Y) \\ @VV{\phi_{(A \otimes C)(B \otimes D),XY}}V @VV{\phi_{AB,(C \otimes X)(D \otimes Y)}}V \\ F ((A \otimes C) \otimes X) ((B \otimes D) \otimes Y) @>>{F \alpha_{\mathcal{C_1}}} \alpha_{\mathcal{C_2}}> F (A \otimes (C \otimes X)) (B \otimes (D \otimes Y)) \\ \end{CD} \]
combine
.
grmap
combine
.
bwd
assoc
≡fmap
(bwd
assoc
).
combine
.
glmap
combine
combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y')) Source #
A natural transformation \(\phi_{AB,CD} : F\ A\ B \bullet F\ C\ D \to F\ (A \otimes C)\ (B \otimes D)\).
Examples
>>>
:t combine @(->) @(,) @(,) @(,) @(,)
combine @(->) @(,) @(,) @(,) @(,) :: ((x, y), (x', y')) -> ((x, x'), (y, y'))
>>>
combine @(->) @(,) @(,) @(,) @(,) ((True, "Hello"), ((), "World"))
((True,()),("Hello","World"))
>>>
combine @(->) @(,) @(,) @(,) @(->) (show, (>10)) (True, 11)
("True",True)
Instances
Unital
class Unital cat i1 i2 io f where Source #
Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\).
A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is Unital
if it supports a morphism
\(\phi : I_{\mathcal{D}} \to F\ I_{\mathcal{C_1}}\ I_{\mathcal{C_2}}\), which we call introduce
.
introduce :: cat io (f i1 i2) Source #
introduce
maps from the identity in \(\mathcal{C_1} \times \mathcal{C_2}\) to the
identity in \(\mathcal{D}\).
Examples
>>>
introduce @(->) @() @() @() @(,) ()
((),())
>>>
:t introduce @(->) @Void @() @() @Either
introduce @(->) @Void @() @() @Either :: () -> Either Void ()
>>>
introduce @(->) @Void @() @() @Either ()
Right ()
Instances
Unital (->) Void Void Void Either Source # | |
Unital (->) Void Void Void (,) Source # | |
Unital (->) Void () () Either Source # | |
Unital (->) () () () (,) Source # | |
Defined in Data.Bifunctor.Monoidal | |
Alternative f => Unital (->) Void Void Void (Star f) Source # | |
Unital (->) Void Void Void (->) Source # | |
Unital (->) Void Void () (Star f) Source # | |
Unital (->) Void Void () (->) Source # | |
Alternative f => Unital (->) () Void () (Star f) Source # | |
Applicative f => Unital (->) () () () (Star f) Source # | |
Defined in Data.Bifunctor.Monoidal | |
Unital (->) () () () (->) Source # | |
Defined in Data.Bifunctor.Monoidal | |
Unital (->) Void Void Void (Joker f :: Type -> Type -> Type) Source # | |
Alternative f => Unital (->) Void Void () (Joker f :: Type -> Type -> Type) Source # | |
Applicative f => Unital (->) () () () (Joker f :: Type -> Type -> Type) Source # | |
Defined in Data.Bifunctor.Monoidal |
Monoidal
class (Tensor cat t1 i1, Tensor cat t2 i2, Tensor cat to io, Semigroupal cat t1 t2 to f, Unital cat i1 i2 io f) => Monoidal cat t1 i1 t2 i2 to io f Source #
Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\).
A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is Monoidal
if it maps between \(\mathcal{C_1} \times \mathcal{C_2}\)
and \(\mathcal{D}\) while preserving their monoidal structure. Eg., a homomorphism of monoidal categories.
See NCatlab for more details.
Laws
Right Unitality:
\[ \require{AMScd} \begin{CD} F A B \bullet I_{\mathcal{D}} @>{1 \bullet \phi}>> F A B \bullet F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}}\\ @VV{\rho_{\mathcal{D}}}V @VV{\phi AB,I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}}}V \\ F A B @<<{F \rho_{\mathcal{C_{1}}} \rho_{\mathcal{C_{2}}}}< F (A \otimes I_{\mathcal{C_{1}}}) (B \otimes I_{\mathcal{C_{2}}}) \end{CD} \]
combine
.
grmap
introduce
≡bwd
unitr
.
fwd
unitr
Left Unitality:
\[ \begin{CD} I_{\mathcal{D}} \bullet F A B @>{\phi \bullet 1}>> F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}} \bullet F A B\\ @VV{\lambda_{\mathcal{D}}}V @VV{I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}},\phi AB}V \\ F A B @<<{F \lambda_{\mathcal{C_{1}}} \lambda_{\mathcal{C_{2}}}}< F (I_{\mathcal{C_{1}}} \otimes A) (I_{\mathcal{C_{2}}} \otimes B) \end{CD} \]
combine
.
glmap
introduce
≡fmap
(bwd
unitl
).
fwd
unitl