{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_HADDOCK hide #-}

module Data.Bifunctor.Linear.Internal.SymmetricMonoidal
  ( SymmetricMonoidal (..),
  )
where

import Data.Bifunctor.Linear.Internal.Bifunctor
import Data.Kind (Type)
import Data.Void
import Prelude.Linear

-- | A SymmetricMonoidal class
--
-- This allows you to shuffle around a bifunctor nested in itself and swap the
-- places of the two types held in the bifunctor. For instance, for tuples:
--
--  * You can use @lassoc :: (a,(b,c)) %1-> ((a,b),c)@ and then use 'first' to access the @a@
--  * You can use the dual, i.e., @ rassoc :: ((a,b),c) %1-> (a,(b,c))@ and then 'second'
--  * You can swap the first and second values with @swap :: (a,b) %1-> (b,a)@
--
--  == Laws
--
--  * @swap . swap = id@
--  * @rassoc . lassoc = id@
--  * @lassoc . rassoc = id@
--  * @second swap . rassoc . first swap = rassoc . swap . rassoc@
class
  (Bifunctor m) =>
  SymmetricMonoidal (m :: Type -> Type -> Type) (u :: Type)
    | m -> u,
      u -> m
  where
  {-# MINIMAL swap, (rassoc | lassoc) #-}
  rassoc :: (a `m` b) `m` c %1 -> a `m` (b `m` c)
  rassoc = m (m b c) a %1 -> m a (m b c)
forall a b. m a b %1 -> m b a
forall (m :: * -> * -> *) u a b.
SymmetricMonoidal m u =>
m a b %1 -> m b a
swap (m (m b c) a %1 -> m a (m b c))
-> (m (m a b) c %1 -> m (m b c) a) -> m (m a b) c %1 -> m a (m b c)
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. m b (m c a) %1 -> m (m b c) a
forall a b c. m a (m b c) %1 -> m (m a b) c
forall (m :: * -> * -> *) u a b c.
SymmetricMonoidal m u =>
m a (m b c) %1 -> m (m a b) c
lassoc (m b (m c a) %1 -> m (m b c) a)
-> (m (m a b) c %1 -> m b (m c a)) -> m (m a b) c %1 -> m (m b c) a
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. m (m c a) b %1 -> m b (m c a)
forall a b. m a b %1 -> m b a
forall (m :: * -> * -> *) u a b.
SymmetricMonoidal m u =>
m a b %1 -> m b a
swap (m (m c a) b %1 -> m b (m c a))
-> (m (m a b) c %1 -> m (m c a) b) -> m (m a b) c %1 -> m b (m c a)
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. m c (m a b) %1 -> m (m c a) b
forall a b c. m a (m b c) %1 -> m (m a b) c
forall (m :: * -> * -> *) u a b c.
SymmetricMonoidal m u =>
m a (m b c) %1 -> m (m a b) c
lassoc (m c (m a b) %1 -> m (m c a) b)
-> (m (m a b) c %1 -> m c (m a b)) -> m (m a b) c %1 -> m (m c a) b
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. m (m a b) c %1 -> m c (m a b)
forall a b. m a b %1 -> m b a
forall (m :: * -> * -> *) u a b.
SymmetricMonoidal m u =>
m a b %1 -> m b a
swap
  lassoc :: a `m` (b `m` c) %1 -> (a `m` b) `m` c
  lassoc = m c (m a b) %1 -> m (m a b) c
forall a b. m a b %1 -> m b a
forall (m :: * -> * -> *) u a b.
SymmetricMonoidal m u =>
m a b %1 -> m b a
swap (m c (m a b) %1 -> m (m a b) c)
-> (m a (m b c) %1 -> m c (m a b)) -> m a (m b c) %1 -> m (m a b) c
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. m (m c a) b %1 -> m c (m a b)
forall a b c. m (m a b) c %1 -> m a (m b c)
forall (m :: * -> * -> *) u a b c.
SymmetricMonoidal m u =>
m (m a b) c %1 -> m a (m b c)
rassoc (m (m c a) b %1 -> m c (m a b))
-> (m a (m b c) %1 -> m (m c a) b) -> m a (m b c) %1 -> m c (m a b)
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. m b (m c a) %1 -> m (m c a) b
forall a b. m a b %1 -> m b a
forall (m :: * -> * -> *) u a b.
SymmetricMonoidal m u =>
m a b %1 -> m b a
swap (m b (m c a) %1 -> m (m c a) b)
-> (m a (m b c) %1 -> m b (m c a)) -> m a (m b c) %1 -> m (m c a) b
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. m (m b c) a %1 -> m b (m c a)
forall a b c. m (m a b) c %1 -> m a (m b c)
forall (m :: * -> * -> *) u a b c.
SymmetricMonoidal m u =>
m (m a b) c %1 -> m a (m b c)
rassoc (m (m b c) a %1 -> m b (m c a))
-> (m a (m b c) %1 -> m (m b c) a) -> m a (m b c) %1 -> m b (m c a)
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. m a (m b c) %1 -> m (m b c) a
forall a b. m a b %1 -> m b a
forall (m :: * -> * -> *) u a b.
SymmetricMonoidal m u =>
m a b %1 -> m b a
swap
  swap :: a `m` b %1 -> b `m` a

-- XXX: should unitors be added?
-- XXX: Laws don't seem minimial

-- # Instances
-------------------------------------------------------------------------------

instance SymmetricMonoidal (,) () where
  swap :: forall a b. (a, b) %1 -> (b, a)
swap (a
x, b
y) = (b
y, a
x)
  rassoc :: forall a b c. ((a, b), c) %1 -> (a, (b, c))
rassoc ((a
x, b
y), c
z) = (a
x, (b
y, c
z))

instance SymmetricMonoidal Either Void where
  swap :: forall a b. Either a b %1 -> Either b a
swap = (a %1 -> Either b a)
-> (b %1 -> Either b a) -> Either a b %1 -> Either b a
forall a c b. (a %1 -> c) -> (b %1 -> c) -> Either a b %1 -> 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
  rassoc :: forall a b c. Either (Either a b) c %1 -> Either a (Either b c)
rassoc (Left (Left a
x)) = a -> Either a (Either b c)
forall a b. a -> Either a b
Left a
x
  rassoc (Left (Right b
x)) = (a -> Either b a
forall {a} {b}. a -> Either b a
forall a b. b -> Either a b
Right :: a %1 -> Either b a) (b -> Either b c
forall a b. a -> Either a b
Left b
x)
  rassoc (Right c
x) = (a -> Either b a
forall {a} {b}. a -> Either b a
forall a b. b -> Either a b
Right :: a %1 -> Either b a) (c -> Either b c
forall a b. b -> Either a b
Right c
x)

-- XXX: the above type signatures are necessary for certain older versions of
-- the compiler, and as such are temporary