monoidal-functors-0.2.0.0: Monoidal Functors Library
Safe HaskellSafe-Inferred
LanguageHaskell2010

Control.Category.Tensor

Synopsis

Iso

data Iso cat a b Source #

An invertible mapping between a and b in category cat.

Laws

fwd . bwdid
bwd . fwdid

Constructors

Iso 

Fields

  • fwd :: cat a b
     
  • bwd :: cat b a
     

Instances

Instances details
Category cat => Category (Iso cat :: Type -> Type -> Type) Source # 
Instance details

Defined in Control.Category.Tensor

Methods

id :: forall (a :: k). Iso cat a a #

(.) :: forall (b :: k) (c :: k) (a :: k). Iso cat b c -> Iso cat a b -> Iso cat a c #

GBifunctor cat cat cat t => GBifunctor (Iso cat) (Iso cat) (Iso cat) t Source # 
Instance details

Defined in Control.Category.Tensor

Methods

gbimap :: Iso cat a b -> Iso cat c d -> Iso cat (t a c) (t b d) Source #

GBifunctor

class (Category cat1, Category cat2, Category cat3) => GBifunctor cat1 cat2 cat3 t | t cat3 -> cat1 cat2 where Source #

A Bifunctor t is a Functor whose domain is the product of two categories. GBifunctor is equivalent to the ordinary Bifunctor class but we replace the implicit (->) Category with three distinct higher kinded variables cat1, cat2, and cat3 allowing the user to pickout a functor from \(cat_1 \times cat_2\) to \(cat_3\).

Laws

gbimap id idid
grmap idid
glmap idid

gbimap (f . g) (h . i) ≡ gbimap f h . gbimap g i
grmap (f . g) ≡ grmap f . grmap g
glmap (f . g) ≡ glmap f . glmap g

Methods

gbimap :: cat1 a b -> cat2 c d -> cat3 (a `t` c) (b `t` d) Source #

Covariantly map over both variables.

gbimap f g ≡ glmap f . grmap g

Examples

Expand
>>> gbimap @(->) @(->) @(->) @(,) show not (123, False)
("123",True)
>>> gbimap @(->) @(->) @(->) @Either show not (Right False)
Right True
>>> getOp (gbimap @Op @Op @Op @Either (Op (+ 1)) (Op show)) (Right True)
Right "True"

Instances

Instances details
GBifunctor (->) (->) (->) t => GBifunctor Op Op Op t Source # 
Instance details

Defined in Control.Category.Tensor

Methods

gbimap :: Op a b -> Op c d -> Op (t a c) (t b d) Source #

GBifunctor cat cat cat t => GBifunctor (Iso cat) (Iso cat) (Iso cat) t Source # 
Instance details

Defined in Control.Category.Tensor

Methods

gbimap :: Iso cat a b -> Iso cat c d -> Iso cat (t a c) (t b d) Source #

GBifunctor (Star Maybe) (Star Maybe) (Star Maybe) These Source # 
Instance details

Defined in Control.Category.Tensor

Methods

gbimap :: Star Maybe a b -> Star Maybe c d -> Star Maybe (These a c) (These b d) Source #

Bifunctor t => GBifunctor (->) (->) (->) t Source # 
Instance details

Defined in Control.Category.Tensor

Methods

gbimap :: (a -> b) -> (c -> d) -> t a c -> t b d Source #

(#) :: GBifunctor cat1 cat2 cat3 t => cat1 a b -> cat2 c d -> cat3 (a `t` c) (b `t` d) infixr 9 Source #

Infix operator for gbimap.

grmap :: GBifunctor cat1 cat2 cat3 t => cat2 c d -> cat3 (a `t` c) (a `t` d) Source #

Covariantally map over the right variable.

glmap :: GBifunctor cat1 cat2 cat3 t => cat1 a b -> cat3 (a `t` c) (b `t` c) Source #

Covariantally map over the left variable.

Associative

class (Category cat, GBifunctor cat cat cat t) => Associative cat t where Source #

A bifunctor \(\_\otimes\_: \mathcal{C} \times \mathcal{C} \to \mathcal{C}\) is Associative if it is equipped with a natural isomorphism of the form \(\alpha_{x,y,z} : (x \otimes (y \otimes z)) \to ((x \otimes y) \otimes z)\), which we call assoc.

Laws

fwd assoc . bwd associd
bwd assoc . fwd associd

Methods

assoc :: Iso cat (a `t` (b `t` c)) ((a `t` b) `t` c) Source #

The natural isomorphism between left and right associated nestings of t.

Examples

Expand
>>> :t assoc @(->) @(,)
assoc @(->) @(,) :: Iso (->) (a, (b, c)) ((a, b), c)
>>> fwd (assoc @(->) @(,)) (1, ("hello", True))
((1,"hello"),True)

Instances

Instances details
Associative (->) t => Associative Op t Source # 
Instance details

Defined in Control.Category.Tensor

Methods

assoc :: Iso Op (t a (t b c)) (t (t a b) c) Source #

(Monad m, Associative (->) t, GBifunctor (Star m) (Star m) (Star m) t) => Associative (Star m) t Source # 
Instance details

Defined in Control.Category.Tensor

Methods

assoc :: Iso (Star m) (t a (t b c)) (t (t a b) c) Source #

Associative (->) Either Source # 
Instance details

Defined in Control.Category.Tensor

Methods

assoc :: Iso (->) (Either a (Either b c)) (Either (Either a b) c) Source #

Associative (->) These Source # 
Instance details

Defined in Control.Category.Tensor

Methods

assoc :: Iso (->) (These a (These b c)) (These (These a b) c) Source #

Associative (->) (,) Source # 
Instance details

Defined in Control.Category.Tensor

Methods

assoc :: Iso (->) (a, (b, c)) ((a, b), c) Source #

Tensor

class Associative cat t => Tensor cat t i | t -> i where Source #

A bifunctor \(\_ \otimes\_ \ : \mathcal{C} \times \mathcal{C} \to \mathcal{C}\) that maps out of the product category \(\mathcal{C} \times \mathcal{C}\) is a Tensor if it has:

  1. a corresponding identity type \(I\)
  2. Left and right unitor operations \(\lambda_{x} : 1 \otimes x \to x\) and \(\rho_{x} : x \otimes 1 \to x\), which we call unitr and unitl.

Laws

fwd unitr (a ⊗ i) ≡ a
bwd unitr a ≡ (a ⊗ i)

fwd unitl (i ⊗ a) ≡ a 
bwd unitl a ≡ (i ⊗ a)

Methods

unitl :: Iso cat (i `t` a) a Source #

The natural isomorphism between (i `t` a) and a.

Examples

Expand
>>> fwd (unitl @_ @(,)) ((), True)
True
>>> bwd (unitl @_ @(,)) True
((),True)
>>> bwd (unitl @_ @Either) True
Right True
>>> :t bwd (unitl @_ @Either) True
bwd (unitl @_ @Either) True :: Either Void Bool

unitr :: Iso cat (a `t` i) a Source #

The natural isomorphism between (a `t` i) and a.

Examples

Expand
>>> fwd (unitr @_ @(,)) (True, ())
True
>>> bwd (unitr @_ @(,)) True
(True,())
>>> bwd (unitr @_ @Either) True
Left True
>>> :t bwd (unitr @_ @Either) True
bwd (unitr @_ @Either) True :: Either Bool Void

Instances

Instances details
Tensor (->) t i => Tensor Op t i Source # 
Instance details

Defined in Control.Category.Tensor

Methods

unitl :: Iso Op (t i a) a Source #

unitr :: Iso Op (t a i) a Source #

(Monad m, Tensor (->) t i, Associative (Star m) t) => Tensor (Star m) t i Source # 
Instance details

Defined in Control.Category.Tensor

Methods

unitl :: Iso (Star m) (t i a) a Source #

unitr :: Iso (Star m) (t a i) a Source #

Tensor (->) Either Void Source # 
Instance details

Defined in Control.Category.Tensor

Methods

unitl :: Iso (->) (Either Void a) a Source #

unitr :: Iso (->) (Either a Void) a Source #

Tensor (->) These Void Source # 
Instance details

Defined in Control.Category.Tensor

Methods

unitl :: Iso (->) (These Void a) a Source #

unitr :: Iso (->) (These a Void) a Source #

Tensor (->) (,) () Source # 
Instance details

Defined in Control.Category.Tensor

Methods

unitl :: Iso (->) ((), a) a Source #

unitr :: Iso (->) (a, ()) a Source #

Symmetric

class Associative cat t => Symmetric cat t where Source #

A bifunctor \(\_ \otimes\_ \ : \mathcal{C} \times \mathcal{C} \to \mathcal{C}\) is Symmetric if it has a product operation \(B_{x,y} : x \otimes y \to y \otimes x\) such that \(B_{x,y} \circ B_{x,y} \equiv 1_{x \otimes y}\), which we call swap.

Laws

swap . swapid

Methods

swap :: cat (a `t` b) (b `t` a) Source #

swap is a symmetry isomorphism for t

Examples

Expand
>>> :t swap @(->) @(,)
swap @(->) @(,) :: (a, b) -> (b, a)
>>> swap @(->) @(,) (True, "hello")
("hello",True)
>>> :t swap @(->) @Either (Left True)
swap @(->) @Either (Left True) :: Either b Bool
>>> swap @(->) @Either (Left True)
Right True

Instances

Instances details
Symmetric (->) t => Symmetric Op t Source # 
Instance details

Defined in Control.Category.Tensor

Methods

swap :: Op (t a b) (t b a) Source #

(Monad m, Symmetric (->) t, Associative (Star m) t) => Symmetric (Star m) t Source # 
Instance details

Defined in Control.Category.Tensor

Methods

swap :: Star m (t a b) (t b a) Source #

Symmetric (->) Either Source # 
Instance details

Defined in Control.Category.Tensor

Methods

swap :: Either a b -> Either b a Source #

Symmetric (->) These Source # 
Instance details

Defined in Control.Category.Tensor

Methods

swap :: These a b -> These b a Source #

Symmetric (->) (,) Source # 
Instance details

Defined in Control.Category.Tensor

Methods

swap :: (a, b) -> (b, a) Source #