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

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

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


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