{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
-------------------------------------------------------------------------------------------
-- |
-- Module    : Control.Category.Monoidal
-- Copyright : 2008,2012 Edward Kmett
-- License   : BSD
--
-- Maintainer : Edward Kmett <ekmett@gmail.com>
-- Stability  : experimental
-- Portability: non-portable (class-associated types)
--
-- A 'Monoidal' category is a category with an associated biendofunctor that has an identity,
-- which satisfies Mac Lane''s pentagonal and triangular coherence conditions
-- Technically we usually say that category is 'Monoidal', but since
-- most interesting categories in our world have multiple candidate bifunctors that you can
-- use to enrich their structure, we choose here to think of the bifunctor as being
-- monoidal. This lets us reuse the same 'Bifunctor' over different categories without
-- painful newtype wrapping.

-------------------------------------------------------------------------------------------

module Control.Category.Monoidal
  ( Monoidal(..)
  ) where

import Control.Category.Associative
import Data.Void

-- | Denotes that we have some reasonable notion of 'Identity' for a particular 'Bifunctor' in this 'Category'. This
-- notion is currently used by both 'Monoidal' and 'Comonoidal'

{- | A monoidal category. 'idl' and 'idr' are traditionally denoted lambda and rho
 the triangle identities hold:

> first idr = second idl . associate
> second idl = first idr . associate
> first idr = disassociate . second idl
> second idl = disassociate . first idr
> idr . coidr = id
> idl . coidl = id
> coidl . idl = id
> coidr . idr = id

-}

class Associative k p => Monoidal (k :: * -> * -> *) (p :: * -> * -> *) where
  type Id (k :: * -> * -> *) (p :: * -> * -> *) :: *
  idl   :: k (p (Id k p) a) a
  idr   :: k (p a (Id k p)) a
  coidl :: k a (p (Id k p) a)
  coidr :: k a (p a (Id k p))

instance Monoidal (->) (,) where
  type Id (->) (,) = ()
  idl :: forall a. (Id (->) (,), a) -> a
idl = (Id (->) (,), a) -> a
forall a b. (a, b) -> b
snd
  idr :: forall a. (a, Id (->) (,)) -> a
idr = (a, Id (->) (,)) -> a
forall a b. (a, b) -> a
fst
  coidl :: forall a. a -> (Id (->) (,), a)
coidl a
a = ((),a
a)
  coidr :: forall a. a -> (a, Id (->) (,))
coidr a
a = (a
a,())

instance Monoidal (->) Either where
  type Id (->) Either = Void
  idl :: forall a. Either (Id (->) Either) a -> a
idl = (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 a. a -> a
id
  idr :: forall a. Either a (Id (->) Either) -> a
idr = (a -> a) -> (Void -> a) -> Either a Void -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
id Void -> a
forall a. Void -> a
absurd
  coidl :: forall a. a -> Either (Id (->) Either) a
coidl = a -> Either (Id (->) Either) a
forall a b. b -> Either a b
Right
  coidr :: forall a. a -> Either a (Id (->) Either)
coidr = a -> Either a (Id (->) Either)
forall a b. a -> Either a b
Left

{-- RULES
-- "bimap id idl/associate"   second idl . associate = first idr
-- "bimap idr id/associate"   first idr . associate = second idl
-- "disassociate/bimap id idl"  disassociate . second idl = first idr
-- "disassociate/bimap idr id"  disassociate . first idr = second idl
"idr/coidr" idr . coidr = id
"idl/coidl"  idl . coidl = id
"coidl/idl"  coidl . idl = id
"coidr/idr"  coidr . idr = id
"idr/braid" idr . braid = idl
"idl/braid" idl . braid = idr
"braid/coidr" braid . coidr = coidl
"braid/coidl" braid . coidl = coidr
 --}