module Data.Functor.Monoidal where

import Prelude
import Control.Applicative
import Control.Category.Tensor
import Data.Void

-- | A <https://ncatlab.org/nlab/show/monoidal+functor Monoidal Functor> is a Functor between two Monoidal Categories
-- which preserves the monoidal structure. Eg., a homomorphism of
-- monoidal categories.
--
-- = Laws
-- Associativity:
--   combine (combine fx fy) fz ⟶ combine fx (combine fy fz)
--              ↓                         ↓
--   f (x `t1` y) `t1` fz         combine fx (f (y `t1` z))
--              ↓                         ↓
--   f ((x `t1` y) `t1` z)      ⟶ (f x `t1` (y `t1` z))
--
-- Left Unitality:
--   empty `t1` f x     ⟶  f empty `t1` f x
--         ↓                        ↓
--        f x           ←  f (empty `t0` x)
--
-- Right Unitality:
--   f x `t1` empty     ⟶  f x `t1` f empty
--         ↓                        ↓
--        f x           ←  f (x `t0` empty)
class ( Tensor t1 i1 cat
      , Tensor t0 i0 cat
      , Semigroupal cat t1 t0 f
      , Unital cat i1 i0 f
      ) => Monoidal cat t1 i1 t0 i0 f

class (Associative t1 cat, Associative t0 cat) => Semigroupal cat t1 t0 f where
  combine :: (f x `t0` f x') `cat` f (x `t1` x')

class Unital cat i1 i0 f where
  introduce :: i0 `cat` f i1

-- TODO: Should we create an Apply class?
instance Applicative f => Semigroupal (->) (,) (,) f where
  combine :: (f x, f x') -> f (x, x')
  combine :: (f x, f x') -> f (x, x')
combine = (f x -> f x' -> f (x, x')) -> (f x, f x') -> f (x, x')
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((x -> x' -> (x, x')) -> f x -> f x' -> f (x, x')
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,))

instance Applicative f => Unital (->) () () f where
  introduce :: () -> f ()
  introduce :: () -> f ()
introduce = () -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance Applicative f => Monoidal (->) (,) () (,) () f

-- TODO: Should we create an Alt class?
instance Alternative f => Semigroupal (->) Either (,) f where
  combine :: (f x, f x') -> f (Either x x')
  combine :: (f x, f x') -> f (Either x x')
combine (f x
fx, f x'
fx') = (x -> Either x x') -> f x -> f (Either x x')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> Either x x'
forall a b. a -> Either a b
Left f x
fx f (Either x x') -> f (Either x x') -> f (Either x x')
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (x' -> Either x x') -> f x' -> f (Either x x')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x' -> Either x x'
forall a b. b -> Either a b
Right f x'
fx'

-- TODO: Should we create a Plus class?
instance Alternative f => Unital (->) Void () f where
  introduce :: () -> f Void
  introduce :: () -> f Void
introduce () = f Void
forall (f :: * -> *) a. Alternative f => f a
empty

instance Alternative f => Monoidal (->) Either Void (,) () f