Control.Category.Tensor

Iso

data Iso cat a b

An invertible mapping between a and b in category cat.

Laws

fwd . bwd ≡ id
bwd . fwd ≡ id

Constructors

Iso

Fields

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

Instances

Category cat => Category (Iso cat :: Type -> Type -> Type)

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

Defined in Control.Category.Tensor

Methods

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

GBifunctor

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

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 id ≡ id
grmap id ≡ id
glmap id ≡ id

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)

Covariantly map over both variables.

gbimap f g ≡ glmap f . grmap g

Examples

>>> 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

GBifunctor (->) (->) (->) t => GBifunctor Op Op Op t

Defined in Control.Category.Tensor

Methods

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

GBifunctor cat cat cat t => GBifunctor (Iso cat) (Iso cat) (Iso cat) t

Defined in Control.Category.Tensor

Methods

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

GBifunctor (Star Maybe) (Star Maybe) (Star Maybe) These

Defined in Control.Category.Tensor

Methods

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

Bifunctor t => GBifunctor (->) (->) (->) t

Defined in Control.Category.Tensor

Methods

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

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

Infix operator for gbimap.

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

Covariantally map over the right variable.

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

Covariantally map over the left variable.

Associative

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

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 assoc ≡ id
bwd assoc . fwd assoc ≡ id

Methods

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

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

Examples

>>> :t assoc @(->) @(,)
assoc @(->) @(,) :: Iso (->) (a, (b, c)) ((a, b), c)

>>> fwd (assoc @(->) @(,)) (1, ("hello", True))
((1,"hello"),True)

Instances

Associative (->) t => Associative Op t

Defined in Control.Category.Tensor

Methods

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

(Monad m, Associative (->) t, GBifunctor (Star m) (Star m) (Star m) t) => Associative (Star m) t

Defined in Control.Category.Tensor

Methods

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

Associative (->) Either

Defined in Control.Category.Tensor

Methods

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

Associative (->) These

Defined in Control.Category.Tensor

Methods

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

Associative (->) (,)

Defined in Control.Category.Tensor

Methods

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

Tensor

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

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

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

Examples

>>> 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

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

Examples

>>> 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

Tensor (->) t i => Tensor Op t i

Defined in Control.Category.Tensor

Methods

unitl :: Iso Op (t i a) a

unitr :: Iso Op (t a i) a

(Monad m, Tensor (->) t i, Associative (Star m) t) => Tensor (Star m) t i

Defined in Control.Category.Tensor

Methods

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

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

Tensor (->) Either Void

Defined in Control.Category.Tensor

Methods

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

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

Tensor (->) These Void

Defined in Control.Category.Tensor

Methods

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

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

Tensor (->) (,) ()

Defined in Control.Category.Tensor

Methods

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

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

Symmetric

class Associative cat t => Symmetric cat t where

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 . swap ≡ id

Methods

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

swap is a symmetry isomorphism for t

Examples

>>> :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

Symmetric (->) t => Symmetric Op t

Defined in Control.Category.Tensor

Methods

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

(Monad m, Symmetric (->) t, Associative (Star m) t) => Symmetric (Star m) t

Defined in Control.Category.Tensor

Methods

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

Symmetric (->) Either

Defined in Control.Category.Tensor

Methods

swap :: Either a b -> Either b a

Symmetric (->) These

Defined in Control.Category.Tensor

Methods

swap :: These a b -> These b a

Symmetric (->) (,)

Defined in Control.Category.Tensor

Methods

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