{-# LANGUAGE MonoLocalBinds #-}
module Control.Category.Tensor where

import Prelude hiding (id)
import Control.Applicative
import Control.Category (Category, id)
import Data.Biapplicative
import Data.Functor.Contravariant
import Data.Profunctor
import Data.These
import Data.Void

{-

| Tensor | Unit |
+--------|------+
| Either | Void |
|  (,)   |  ()  |
| These  | Void |

tensor = monoidal structure =
    category
  + bifunctor on that category `t`
  + unit object in that category `i`
  + isomorphisms in that category `t i a <-> a`, `t a i <-> a`, `t a (t b c) <-> t (t a b) c`
  + some equalities

monoidal functor = a functor that goes between the underlying
categories of two different monoidal structure, and has a pair of
operations `t2 (f a) (f b) -> f (t1 a b)` and `i2 -> f i1`

-}

class (Category cat1, Category cat2) => GBifunctor cat1 cat2 r t | t r -> cat1 cat2 where
  gbimap :: a `cat1` b -> c `cat2` d -> t a c `r` t b d

instance GBifunctor (->) (->) (->) t => GBifunctor Op Op Op t where
  gbimap :: Op a b -> Op c d -> Op (t a c) (t b d)
  gbimap :: Op a b -> Op c d -> Op (t a c) (t b d)
gbimap (Op b -> a
f) (Op d -> c
g) = (t b d -> t a c) -> Op (t a c) (t b d)
forall a b. (b -> a) -> Op a b
Op ((t b d -> t a c) -> Op (t a c) (t b d))
-> (t b d -> t a c) -> Op (t a c) (t b d)
forall a b. (a -> b) -> a -> b
$ (b -> a) -> (d -> c) -> t b d -> t a c
forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (r :: * -> * -> *) (t :: * -> * -> *) a b c d.
GBifunctor cat1 cat2 r t =>
cat1 a b -> cat2 c d -> r (t a c) (t b d)
gbimap b -> a
f d -> c
g

instance GBifunctor (->) (->) (->) (,) where
  gbimap :: (a -> b) -> (c -> d) -> (a, c) -> (b, d)
  gbimap :: (a -> b) -> (c -> d) -> (a, c) -> (b, d)
gbimap a -> b
f c -> d
g = (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f c -> d
g

instance GBifunctor (->) (->) (->) Either where
  gbimap :: (a -> b) -> (c -> d) -> Either a c -> Either b d
  gbimap :: (a -> b) -> (c -> d) -> Either a c -> Either b d
gbimap a -> b
f c -> d
g = (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f c -> d
g

instance GBifunctor (->) (->) (->) These where
  gbimap :: (a -> b) -> (c -> d) -> These a c -> These b d
  gbimap :: (a -> b) -> (c -> d) -> These a c -> These b d
gbimap a -> b
f c -> d
g = (a -> b) -> (c -> d) -> These a c -> These b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f c -> d
g

instance GBifunctor (Star Maybe) (Star Maybe) (Star Maybe) These where
  gbimap :: Star Maybe a b -> Star Maybe c d -> Star Maybe (These a c) (These b d)
  gbimap :: Star Maybe a b
-> Star Maybe c d -> Star Maybe (These a c) (These b d)
gbimap (Star a -> Maybe b
f) (Star c -> Maybe d
g) =
    (These a c -> Maybe (These b d))
-> Star Maybe (These a c) (These b d)
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((These a c -> Maybe (These b d))
 -> Star Maybe (These a c) (These b d))
-> (These a c -> Maybe (These b d))
-> Star Maybe (These a c) (These b d)
forall a b. (a -> b) -> a -> b
$ \case
      This a
a -> b -> These b d
forall a b. a -> These a b
This (b -> These b d) -> Maybe b -> Maybe (These b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
a
      That c
c -> d -> These b d
forall a b. b -> These a b
That (d -> These b d) -> Maybe d -> Maybe (These b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Maybe d
g c
c
      These a
a c
c -> (b -> d -> These b d) -> Maybe b -> Maybe d -> Maybe (These b d)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 b -> d -> These b d
forall a b. a -> b -> These a b
These (a -> Maybe b
f a
a) (c -> Maybe d
g c
c)

grmap :: GBifunctor cat1 cat2 r t => c `cat2` d -> t a c `r` t a d
grmap :: cat2 c d -> r (t a c) (t a d)
grmap = cat1 a a -> cat2 c d -> r (t a c) (t a d)
forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (r :: * -> * -> *) (t :: * -> * -> *) a b c d.
GBifunctor cat1 cat2 r t =>
cat1 a b -> cat2 c d -> r (t a c) (t b d)
gbimap cat1 a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

glmap :: GBifunctor cat1 cat2 r t => a `cat1` b -> t a c `r` t b c
glmap :: cat1 a b -> r (t a c) (t b c)
glmap = (cat1 a b -> cat2 c c -> r (t a c) (t b c))
-> cat2 c c -> cat1 a b -> r (t a c) (t b c)
forall a b c. (a -> b -> c) -> b -> a -> c
flip cat1 a b -> cat2 c c -> r (t a c) (t b c)
forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (r :: * -> * -> *) (t :: * -> * -> *) a b c d.
GBifunctor cat1 cat2 r t =>
cat1 a b -> cat2 c d -> r (t a c) (t b d)
gbimap cat2 c c
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

data Iso cat a b = Iso { Iso cat a b -> cat a b
fwd :: a `cat` b, Iso cat a b -> cat b a
bwd :: b `cat` a }

class (Category cat, GBifunctor cat cat cat t) => Associative t cat where
  assoc :: Iso cat (a `t` (b `t` c)) ((a `t` b) `t` c)

instance Associative t (->) => Associative t Op where
  assoc :: Iso Op (t a (t b c)) (t (t a b) c)
  assoc :: Iso Op (t a (t b c)) (t (t a b) c)
assoc = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: Op (t a (t b c)) (t (t a b) c)
fwd = (t (t a b) c -> t a (t b c)) -> Op (t a (t b c)) (t (t a b) c)
forall a b. (b -> a) -> Op a b
Op ((t (t a b) c -> t a (t b c)) -> Op (t a (t b c)) (t (t a b) c))
-> (t (t a b) c -> t a (t b c)) -> Op (t a (t b c)) (t (t a b) c)
forall a b. (a -> b) -> a -> b
$ Iso (->) (t a (t b c)) (t (t a b) c) -> t (t a b) c -> t a (t b c)
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd Iso (->) (t a (t b c)) (t (t a b) c)
forall (t :: * -> * -> *) (cat :: * -> * -> *) a b c.
Associative t cat =>
Iso cat (t a (t b c)) (t (t a b) c)
assoc
    , bwd :: Op (t (t a b) c) (t a (t b c))
bwd = (t a (t b c) -> t (t a b) c) -> Op (t (t a b) c) (t a (t b c))
forall a b. (b -> a) -> Op a b
Op ((t a (t b c) -> t (t a b) c) -> Op (t (t a b) c) (t a (t b c)))
-> (t a (t b c) -> t (t a b) c) -> Op (t (t a b) c) (t a (t b c))
forall a b. (a -> b) -> a -> b
$ Iso (->) (t a (t b c)) (t (t a b) c) -> t a (t b c) -> t (t a b) c
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd Iso (->) (t a (t b c)) (t (t a b) c)
forall (t :: * -> * -> *) (cat :: * -> * -> *) a b c.
Associative t cat =>
Iso cat (t a (t b c)) (t (t a b) c)
assoc
    }

instance (Monad m, Associative t (->), GBifunctor (Star m) (Star m) (Star m) t) => Associative t (Star m) where
  assoc :: Iso (Star m) (t a (t b c)) (t (t a b) c)
  assoc :: Iso (Star m) (t a (t b c)) (t (t a b) c)
assoc = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: Star m (t a (t b c)) (t (t a b) c)
fwd = ((t a (t b c) -> t (t a b) c)
-> Star m (t a (t b c)) (t a (t b c))
-> Star m (t a (t b c)) (t (t a b) c)
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` Star m (t a (t b c)) (t a (t b c))
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (Iso (->) (t a (t b c)) (t (t a b) c) -> t a (t b c) -> t (t a b) c
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd Iso (->) (t a (t b c)) (t (t a b) c)
forall (t :: * -> * -> *) (cat :: * -> * -> *) a b c.
Associative t cat =>
Iso cat (t a (t b c)) (t (t a b) c)
assoc)
    , bwd :: Star m (t (t a b) c) (t a (t b c))
bwd = ((t (t a b) c -> t a (t b c))
-> Star m (t (t a b) c) (t (t a b) c)
-> Star m (t (t a b) c) (t a (t b c))
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` Star m (t (t a b) c) (t (t a b) c)
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (Iso (->) (t a (t b c)) (t (t a b) c) -> t (t a b) c -> t a (t b c)
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd Iso (->) (t a (t b c)) (t (t a b) c)
forall (t :: * -> * -> *) (cat :: * -> * -> *) a b c.
Associative t cat =>
Iso cat (t a (t b c)) (t (t a b) c)
assoc)
    }

instance Associative (,) (->) where
  assoc :: Iso (->) (a, (b, c)) ((a, b), c)
  assoc :: Iso (->) (a, (b, c)) ((a, b), c)
assoc = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: (a, (b, c)) -> ((a, b), c)
fwd = \(a
a, (b
b, c
c)) -> ((a
a, b
b), c
c)
    , bwd :: ((a, b), c) -> (a, (b, c))
bwd = \((a
a, b
b), c
c) -> (a
a, (b
b, c
c))
    }

instance Associative Either (->) where
  assoc :: Iso (->) (Either a (Either b c)) (Either (Either a b) c)
  assoc :: Iso (->) (Either a (Either b c)) (Either (Either a b) c)
assoc = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: Either a (Either b c) -> Either (Either a b) c
fwd = (a -> Either (Either a b) c)
-> (Either b c -> Either (Either a b) c)
-> Either a (Either b c)
-> Either (Either a b) c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (Either a b -> Either (Either a b) c)
-> (a -> Either a b) -> a -> Either (Either a b) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either a b
forall a b. a -> Either a b
Left) ((b -> Either (Either a b) c)
-> (c -> Either (Either a b) c)
-> Either b c
-> Either (Either a b) c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (Either a b -> Either (Either a b) c)
-> (b -> Either a b) -> b -> Either (Either a b) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Either a b
forall a b. b -> Either a b
Right) c -> Either (Either a b) c
forall a b. b -> Either a b
Right)
    , bwd :: Either (Either a b) c -> Either a (Either b c)
bwd = (Either a b -> Either a (Either b c))
-> (c -> Either a (Either b c))
-> Either (Either a b) c
-> Either a (Either b c)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((b -> Either b c) -> Either a b -> Either a (Either b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either b c
forall a b. a -> Either a b
Left) (Either b c -> Either a (Either b c)
forall a b. b -> Either a b
Right (Either b c -> Either a (Either b c))
-> (c -> Either b c) -> c -> Either a (Either b c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> Either b c
forall a b. b -> Either a b
Right)
    }

instance Associative These (->) where
  assoc :: Iso (->) (These a (These b c)) (These (These a b) c)
  assoc :: Iso (->) (These a (These b c)) (These (These a b) c)
assoc = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: These a (These b c) -> These (These a b) c
fwd = (a -> These (These a b) c)
-> (These b c -> These (These a b) c)
-> (a -> These b c -> These (These a b) c)
-> These a (These b c)
-> These (These a b) c
forall a c b.
(a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these (These a b -> These (These a b) c
forall a b. a -> These a b
This (These a b -> These (These a b) c)
-> (a -> These a b) -> a -> These (These a b) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> These a b
forall a b. a -> These a b
This) ((b -> These a b) -> These b c -> These (These a b) c
forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (r :: * -> * -> *) (t :: * -> * -> *) a b c.
GBifunctor cat1 cat2 r t =>
cat1 a b -> r (t a c) (t b c)
glmap b -> These a b
forall a b. b -> These a b
That) ((b -> These a b) -> These b c -> These (These a b) c
forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (r :: * -> * -> *) (t :: * -> * -> *) a b c.
GBifunctor cat1 cat2 r t =>
cat1 a b -> r (t a c) (t b c)
glmap ((b -> These a b) -> These b c -> These (These a b) c)
-> (a -> b -> These a b) -> a -> These b c -> These (These a b) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> These a b
forall a b. a -> b -> These a b
These)
    , bwd :: These (These a b) c -> These a (These b c)
bwd = (These a b -> These a (These b c))
-> (c -> These a (These b c))
-> (These a b -> c -> These a (These b c))
-> These (These a b) c
-> These a (These b c)
forall a c b.
(a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these ((b -> These b c) -> These a b -> These a (These b c)
forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (r :: * -> * -> *) (t :: * -> * -> *) c d a.
GBifunctor cat1 cat2 r t =>
cat2 c d -> r (t a c) (t a d)
grmap b -> These b c
forall a b. a -> These a b
This) (These b c -> These a (These b c)
forall a b. b -> These a b
That (These b c -> These a (These b c))
-> (c -> These b c) -> c -> These a (These b c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> These b c
forall a b. b -> These a b
That) ((c -> These a b -> These a (These b c))
-> These a b -> c -> These a (These b c)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((c -> These a b -> These a (These b c))
 -> These a b -> c -> These a (These b c))
-> (c -> These a b -> These a (These b c))
-> These a b
-> c
-> These a (These b c)
forall a b. (a -> b) -> a -> b
$ (b -> These b c) -> These a b -> These a (These b c)
forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (r :: * -> * -> *) (t :: * -> * -> *) c d a.
GBifunctor cat1 cat2 r t =>
cat2 c d -> r (t a c) (t a d)
grmap ((b -> These b c) -> These a b -> These a (These b c))
-> (c -> b -> These b c) -> c -> These a b -> These a (These b c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> c -> These b c) -> c -> b -> These b c
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> c -> These b c
forall a b. a -> b -> These a b
These)
    }

class Associative t cat => Tensor t i cat | t -> i where
  lunit :: Iso cat (t i a) a
  runit :: Iso cat (t a i) a

instance (Tensor t i (->)) => Tensor t i Op where
  lunit :: Iso Op (t i a) a
  lunit :: Iso Op (t i a) a
lunit = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: Op (t i a) a
fwd = (a -> t i a) -> Op (t i a) a
forall a b. (b -> a) -> Op a b
Op ((a -> t i a) -> Op (t i a) a) -> (a -> t i a) -> Op (t i a) a
forall a b. (a -> b) -> a -> b
$ Iso (->) (t i a) a -> a -> t i a
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd Iso (->) (t i a) a
forall (t :: * -> * -> *) i (cat :: * -> * -> *) a.
Tensor t i cat =>
Iso cat (t i a) a
lunit
    , bwd :: Op a (t i a)
bwd = (t i a -> a) -> Op a (t i a)
forall a b. (b -> a) -> Op a b
Op ((t i a -> a) -> Op a (t i a)) -> (t i a -> a) -> Op a (t i a)
forall a b. (a -> b) -> a -> b
$ Iso (->) (t i a) a -> t i a -> a
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd Iso (->) (t i a) a
forall (t :: * -> * -> *) i (cat :: * -> * -> *) a.
Tensor t i cat =>
Iso cat (t i a) a
lunit
    }

  runit :: Iso Op (t a i) a
  runit :: Iso Op (t a i) a
runit = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: Op (t a i) a
fwd = (a -> t a i) -> Op (t a i) a
forall a b. (b -> a) -> Op a b
Op ((a -> t a i) -> Op (t a i) a) -> (a -> t a i) -> Op (t a i) a
forall a b. (a -> b) -> a -> b
$ Iso (->) (t a i) a -> a -> t a i
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd Iso (->) (t a i) a
forall (t :: * -> * -> *) i (cat :: * -> * -> *) a.
Tensor t i cat =>
Iso cat (t a i) a
runit
    , bwd :: Op a (t a i)
bwd = (t a i -> a) -> Op a (t a i)
forall a b. (b -> a) -> Op a b
Op ((t a i -> a) -> Op a (t a i)) -> (t a i -> a) -> Op a (t a i)
forall a b. (a -> b) -> a -> b
$ Iso (->) (t a i) a -> t a i -> a
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd Iso (->) (t a i) a
forall (t :: * -> * -> *) i (cat :: * -> * -> *) a.
Tensor t i cat =>
Iso cat (t a i) a
runit
    }

instance (Monad m, Tensor t i (->), Associative t (Star m)) => Tensor t i (Star m) where
  lunit :: Iso (Star m) (t i a) a
  lunit :: Iso (Star m) (t i a) a
lunit = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: Star m (t i a) a
fwd = ((t i a -> a) -> Star m (t i a) (t i a) -> Star m (t i a) a
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` Star m (t i a) (t i a)
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (Iso (->) (t i a) a -> t i a -> a
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd Iso (->) (t i a) a
forall (t :: * -> * -> *) i (cat :: * -> * -> *) a.
Tensor t i cat =>
Iso cat (t i a) a
lunit)
    , bwd :: Star m a (t i a)
bwd = ((a -> t i a) -> Star m a a -> Star m a (t i a)
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` Star m a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (Iso (->) (t i a) a -> a -> t i a
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd Iso (->) (t i a) a
forall (t :: * -> * -> *) i (cat :: * -> * -> *) a.
Tensor t i cat =>
Iso cat (t i a) a
lunit)
    }

  runit :: Iso (Star m) (t a i) a
runit = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: Star m (t a i) a
fwd = ((t a i -> a) -> Star m (t a i) (t a i) -> Star m (t a i) a
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` Star m (t a i) (t a i)
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (Iso (->) (t a i) a -> t a i -> a
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd Iso (->) (t a i) a
forall (t :: * -> * -> *) i (cat :: * -> * -> *) a.
Tensor t i cat =>
Iso cat (t a i) a
runit)
    , bwd :: Star m a (t a i)
bwd = ((a -> t a i) -> Star m a a -> Star m a (t a i)
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` Star m a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (Iso (->) (t a i) a -> a -> t a i
forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd Iso (->) (t a i) a
forall (t :: * -> * -> *) i (cat :: * -> * -> *) a.
Tensor t i cat =>
Iso cat (t a i) a
runit)
    }

instance Tensor (,) () (->) where
  lunit :: Iso (->) ((), a) a
  lunit :: Iso (->) ((), a) a
lunit = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: ((), a) -> a
fwd = ((), a) -> a
forall a b. (a, b) -> b
snd
    , bwd :: a -> ((), a)
bwd = () -> a -> ((), a)
forall (p :: * -> * -> *) a b. Biapplicative p => a -> b -> p a b
bipure ()
    }

  runit :: Iso (->) (a, ()) a
  runit :: Iso (->) (a, ()) a
runit = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: (a, ()) -> a
fwd = (a, ()) -> a
forall a b. (a, b) -> a
fst
    , bwd :: a -> (a, ())
bwd = (a -> () -> (a, ())
forall (p :: * -> * -> *) a b. Biapplicative p => a -> b -> p a b
`bipure` ())
    }

instance Tensor Either Void (->) where
  lunit :: Iso (->) (Either Void a) a
  lunit :: Iso (->) (Either Void a) a
lunit = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
     { fwd :: Either Void a -> a
fwd = (Void -> a) -> (a -> a) -> Either Void a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Void -> a
forall a. Void -> a
absurd a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
     , bwd :: a -> Either Void a
bwd = a -> Either Void a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
     }

  runit :: Iso (->) (Either a Void) a
  runit :: Iso (->) (Either a Void) a
runit = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: Either a Void -> a
fwd = (a -> a) -> (Void -> a) -> Either a Void -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id Void -> a
forall a. Void -> a
absurd
    , bwd :: a -> Either a Void
bwd = a -> Either a Void
forall a b. a -> Either a b
Left
    }

instance Tensor These Void (->) where
  lunit :: Iso (->) (These Void a) a
  lunit :: Iso (->) (These Void a) a
lunit = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: These Void a -> a
fwd = (Void -> a) -> (a -> a) -> (Void -> a -> a) -> These Void a -> a
forall a c b.
(a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these Void -> a
forall a. Void -> a
absurd a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (\ Void
_ a
x -> a
x)
    , bwd :: a -> These Void a
bwd = a -> These Void a
forall a b. b -> These a b
That
    }

  runit :: Iso (->) (These a Void) a
  runit :: Iso (->) (These a Void) a
runit = Iso :: forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso
    { fwd :: These a Void -> a
fwd = (a -> a) -> (Void -> a) -> (a -> Void -> a) -> These a Void -> a
forall a c b.
(a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id Void -> a
forall a. Void -> a
absurd a -> Void -> a
forall a b. a -> b -> a
const
    , bwd :: a -> These a Void
bwd = a -> These a Void
forall a b. a -> These a b
This
    }

class Associative t cat => Symmetric t cat where
  swap :: t a b `cat` t b a

instance (Symmetric t (->)) => Symmetric t Op where
  swap :: Op (t a b) (t b a)
  swap :: Op (t a b) (t b a)
swap = (t b a -> t a b) -> Op (t a b) (t b a)
forall a b. (b -> a) -> Op a b
Op t b a -> t a b
forall (t :: * -> * -> *) (cat :: * -> * -> *) a b.
Symmetric t cat =>
cat (t a b) (t b a)
swap

instance (Monad m, Symmetric t (->), Associative t (Star m)) => Symmetric t (Star m) where
  swap :: Star m (t a b) (t b a)
  swap :: Star m (t a b) (t b a)
swap = (t a b -> m (t b a)) -> Star m (t a b) (t b a)
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((t a b -> m (t b a)) -> Star m (t a b) (t b a))
-> (t a b -> m (t b a)) -> Star m (t a b) (t b a)
forall a b. (a -> b) -> a -> b
$ t b a -> m (t b a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t b a -> m (t b a)) -> (t a b -> t b a) -> t a b -> m (t b a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a b -> t b a
forall (t :: * -> * -> *) (cat :: * -> * -> *) a b.
Symmetric t cat =>
cat (t a b) (t b a)
swap

instance Symmetric (,) (->) where
  swap :: (a, b) -> (b, a)
  swap :: (a, b) -> (b, a)
swap (a
a, b
b) = (b
b, a
a)

instance Symmetric Either (->) where
  swap :: Either a b -> Either b a
  swap :: Either a b -> Either b a
swap = (a -> Either b a) -> (b -> Either b a) -> Either a b -> Either b a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Either b a
forall a b. b -> Either a b
Right b -> Either b a
forall a b. a -> Either a b
Left

instance Symmetric These (->) where
  swap :: These a b -> These b a
  swap :: These a b -> These b a
swap = (a -> These b a)
-> (b -> These b a)
-> (a -> b -> These b a)
-> These a b
-> These b a
forall a c b.
(a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these a -> These b a
forall a b. b -> These a b
That b -> These b a
forall a b. a -> These a b
This ((b -> a -> These b a) -> a -> b -> These b a
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> a -> These b a
forall a b. a -> b -> These a b
These)

class (Symmetric t cat, Tensor t i cat) => Cartesian t i cat | i -> t, t -> i where
  diagonal :: a `cat` t a a
  terminal :: a `cat` i

instance Cartesian (,) () (->) where
  diagonal :: a -> (a , a)
  diagonal :: a -> (a, a)
diagonal = a -> (a, a)
forall a. a -> (a, a)
dup

  terminal :: a -> ()
  terminal :: a -> ()
terminal = () -> a -> ()
forall a b. a -> b -> a
const ()

instance Cartesian Either Void Op where
  diagonal :: Op a (Either a a)
  diagonal :: Op a (Either a a)
diagonal = (Either a a -> a) -> Op a (Either a a)
forall a b. (b -> a) -> Op a b
Op Either a a -> a
forall a. Either a a -> a
merge

  terminal :: Op a Void
  terminal :: Op a Void
terminal = (Void -> a) -> Op a Void
forall a b. (b -> a) -> Op a b
Op Void -> a
forall a. Void -> a
absurd

dup :: a -> (a, a)
dup :: a -> (a, a)
dup a
a = (a
a, a
a)

merge :: Either a a -> a
merge :: Either a a -> a
merge = (a -> a) -> (a -> a) -> Either a a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id