MonoidalCategory.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TupleSections #-}
import Prelude hiding (fst, snd, curry, uncurry, (.))

import Control.Category
import Data.Void
import Control.Arrow (Kleisli(..), arr)

class Category cat => MonoidalCategory cat p u | p -> u where
  fromRight  :: cat (p u a) a                    -- rho
  fromLeft   :: cat (p a u) a                    -- lambda
  toRight    :: cat a (p u a)
  toLeft     :: cat a (p a u)

  assoc      :: cat (p (p a b) c) (p a (p b c))  -- alpha
  assoc'     :: cat (p a (p b c)) (p (p a b) c)

  first      :: cat a b -> cat (p a c) (p b c)
  second     :: cat a b -> cat (p c a) (p c b)

instance MonoidalCategory (->) (,) () where
  fromRight (_, x)  = x
  fromLeft (x, _)   = x

  toRight           = ((),)
  toLeft            = (,())

  assoc ((a,b),c)   = (a,(b,c))
  assoc' (a,(b,c))  = ((a,b),c)

  first f (a,b)     = (f a, b)
  second f (a,b)    = (a, f b)

instance Monad m => MonoidalCategory (Kleisli m) (,) () where
  fromRight  = arr fromRight
  fromLeft   = arr fromLeft

  toRight    = arr toRight
  toLeft     = arr toLeft

  assoc      = arr assoc
  assoc'     = arr assoc'
  first      =  arr first
  second     = arr second

instance MonoidalCategory (->) Either Void where
  fromRight (Right r)  = r
  fromLeft  (Left l)   = l

  toRight  = Right
  toLeft   = Left

  assoc (Left (Left x))     = Left x
  assoc (Left (Right x))    = Right (Left x)
  assoc (Right x)           = Right (Right x)

  assoc' (Left x)           = Left (Left x)
  assoc' (Right (Left x))   = Left (Right x)
  assoc' (Right (Right x))  = Right x

  first f (Left x)    = Left (f x)
  first f (Right x)   = Right x

  second f (Left x)   = Left x
  second f (Right x)  = Right (f x)

instance Monad m => MonoidalCategory (Kleisli m) Either Void where
  fromRight  = arr fromRight
  fromLeft   = arr fromLeft

  toRight    = arr toRight
  toLeft     = arr toLeft

  assoc      = arr assoc
  assoc'     = arr assoc'
  first      =  arr first
  second     = arr second


class MonoidalCategory cat p u => SymmetricalMonoidalCategory cat p u where
  swap :: cat (p a b) (p b a)

instance SymmetricalMonoidalCategory (->) (,) () where
  swap (a,b) = (b, a)

instance Monad m => SymmetricalMonoidalCategory (Kleisli m) (,) () where
  swap = arr swap

instance SymmetricalMonoidalCategory (->) Either Void  where
  swap (Left x)   = Right x
  swap (Right x)  = Left x

instance Monad m => SymmetricalMonoidalCategory (Kleisli m) Either Void where
  swap = arr swap


class SymmetricalMonoidalCategory cat p u => ClosedMonoidalCategory cat p u where
  fst :: cat (p a b) a
  snd :: cat (p a b) b
  snd = fst . swap

instance ClosedMonoidalCategory (->) (,) () where
  fst (x,_)  = x

instance Monad m => ClosedMonoidalCategory (Kleisli m) (,) () where
  fst = arr fst


-- A^B ≅ A ~> B
class ClosedMonoidalCategory cat p u => CCC cat p u where
  eval     :: cat (p (cat a b) a) b
  uncurry  :: cat a (cat b c) -> cat (p a b) c
  curry    :: cat (p a b)  c -> cat a (cat b c)

instance CCC (->) (,) () where
  eval           = uncurry ($)
  uncurry f      = \(a,b) -> f a b
  curry f        = \a b -> f (a,b)

instance Monad m => CCC (Kleisli m) (,) () where
  eval     = Kleisli (uncurry runKleisli)
  uncurry  = arr uncurry
  curry    = arr curry