{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
-------------------------------------------------------------------------------------------
-- |
-- Module	 : Control.Category.Monoidal
-- Copyright : 2008 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.

-- The use of class associated types here makes Control.Category.Cartesian FAR more palatable
-------------------------------------------------------------------------------------------

module Control.Category.Monoidal 
	( Id
	, Monoidal(..)
	, Comonoidal(..)
	) 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'
type family Id k p :: *

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

> first idr = second idl . associate 
> second idl = first idr . associate
-}

class Associative k p => Monoidal k p where
  idl :: k (p (Id k p) a) a
  idr :: k (p a (Id k p)) a

{- | A comonoidal category satisfies the dual form of the triangle identities

> first idr = disassociate . second idl
> second idl = disassociate . first idr

This type class is also (ab)used for the inverse operations needed for a strict (co)monoidal category.
A strict (co)monoidal category is one that is both 'Monoidal' and 'Comonoidal' and satisfies the following laws:

> idr . coidr = id 
> idl . coidl = id 
> coidl . idl = id 
> coidr . idr = id 

-}
class Disassociative k p => Comonoidal k p where
  coidl :: k a (p (Id k p) a)
  coidr :: k a (p a (Id k p))

{-- 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
 --}

type instance Id (->) (,) = ()
type instance Id (->) Either = Void

instance Monoidal (->) (,) where
  idl = snd
  idr = fst

instance Monoidal (->) Either where
  idl = either absurd id
  idr = either id absurd

instance Comonoidal (->) (,) where
  coidl a = ((),a)
  coidr a = (a,())

instance Comonoidal (->) Either where
  coidl = Right
  coidr = Left