A Tenative Category Heirarchy

Categories.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Categories where

import qualified Prelude as Prelude
import Prelude hiding (id, (.), fst, snd, curry, uncurry)

import Control.Category

import Data.Void

--------------------------------------------------------------------------------
-- Monoidal Heirarchy

class (Category k) => Tensor t k where
    tensor :: a `k` c -> b `k` d -> (a `t` b) `k` (c `t` d)

class (Category k, Tensor t k) => Monoidal t i k | t -> i where
    leftUnitor :: (i `t` a) `k` a
    leftUnitorSym :: a `k` (i `t` a)
    rightUnitor :: (a `t` i) `k` a
    rightUnitorSym :: a `k` (a `t` i)
    assoc    :: (a `t` (b `t` c)) `k` ((a `t` b) `t` c)
    assocSym :: ((a `t` b) `t` c) `k` (a `t` (b `t` c))

class Monoidal t i k => SymmetricMonoidal t i k where
    swap :: (a `t` b) `k` (b `t` a)

class Monoidal t i k => MonoidalClosed t i hom k | t -> hom where
    eval :: ((a `hom` b) `t` a) `k` b
    curry :: ((a `t` b)`hom` c) `k` (a `hom` (b `hom` c))
    uncurry :: (a `hom` (b `hom` c)) `k` ((a `t` b)`hom` c)

class Monoidal t i k => MonoidalRecursive t i k where
    leftRecurse :: (a `t` r) `k` (b `t` r) -> a `k` b
    rightRecurse :: (r `t` a) `k` (r `t` b) -> a `k` b

--------------------------------------------------------------------------------
-- Cartesian

class (Category k) => HasProducts t k | k -> t where
    fst :: (a `t` b) `k` a
    snd :: (a `t` b) `k` b
    (&&&) :: (c `k` a) -> (c `k` b) -> (c `k` (a `t` b))

copy :: (HasProducts t k) => a `k` (a `t` a)
copy = id &&& id

class Category k => HasTerminal i k | k -> i where
    consume :: a `k` i

-- This _could_ be a type alias, but this leads to better type inference
class (HasTerminal i k, HasProducts t k) => Cartesian t i k | k -> t i, t -> i, i -> t

type CartesianClosed t i hom k = (Cartesian t i k, MonoidalClosed t i hom k)


--------------------------------------------------------------------------------
-- Cocartesian

class Category k => HasCoproducts t k | k -> t where
    left :: a `k` (a `t` b)
    right :: b `k` (a `t` b)
    (+++) :: (a `k` c) -> (b `k` c) -> (a `t` b) `k` c

elim :: (HasCoproducts t k) => (a `t` a) `k` a
elim = (id +++ id)

class Category k => HasInitial i k | k -> i where
    silly :: i `k` a

-- This _could_ be a type alias, but this leads to better type inference
class (HasInitial i k, HasCoproducts t k) => Cocartesian t i k | k -> t i, t -> i, i -> t

--------------------------------------------------------------------------------
-- Deriving Via

-- Every Cartesian Category is Monoidal
newtype CartesianMonoidal k a b = CartesianMonoidal { unCartesianMonoidal :: a `k` b }
    deriving newtype (Category, HasTerminal i, HasProducts t, Cartesian t i)

instance (HasProducts t k) => Tensor t (CartesianMonoidal k) where
    tensor f g = (f . fst) &&& (g . snd)

instance (Cartesian t i k) => Monoidal t i (CartesianMonoidal k) where
    leftUnitor = CartesianMonoidal snd
    leftUnitorSym = CartesianMonoidal (consume &&& id)
    rightUnitor = CartesianMonoidal fst
    rightUnitorSym = CartesianMonoidal (id &&& consume)
    assoc = CartesianMonoidal ((fst &&& (fst . snd)) &&& (snd . snd))
    assocSym = CartesianMonoidal ((fst . fst) &&& ((snd . fst) &&& snd))

instance (Cartesian t i k) => SymmetricMonoidal t i (CartesianMonoidal k) where
    swap = CartesianMonoidal (snd &&& fst)

-- Every Cocartesian Category is Monoidal
newtype CocartesianMonoidal k a b = CocartesianMonoidal { unCocartesianMonoidal :: a `k` b }
    deriving newtype (Category, HasInitial i, HasCoproducts t, Cocartesian t i)

instance (HasCoproducts t k) => Tensor t (CocartesianMonoidal k) where
    tensor f g = (left . f) +++ (right . g)

instance (Cocartesian t i k) => Monoidal t i (CocartesianMonoidal k) where
    leftUnitor = CocartesianMonoidal (silly +++ id)
    leftUnitorSym = CocartesianMonoidal right
    rightUnitor = CocartesianMonoidal (id +++ silly)
    rightUnitorSym = CocartesianMonoidal left
    assoc = CocartesianMonoidal ((left . left) +++ ((left . right) +++ right))
    assocSym = CocartesianMonoidal ((left +++ (right . left)) +++ (right . right))

instance (Cocartesian t i k) => SymmetricMonoidal t i (CocartesianMonoidal k) where
    swap = CocartesianMonoidal (right +++ left)

--------------------------------------------------------------------------------
-- Deriving via Duality

newtype Dual k a b = Dual { getDual :: b `k` a }

instance Category k => Category (Dual k) where
    id = Dual id
    (Dual f) . (Dual g) = Dual (g . f)

instance (HasTerminal t k) => HasInitial t (Dual k) where
    silly = Dual consume

instance (HasInitial t k) => HasTerminal t (Dual k) where
    consume = Dual silly

instance (HasProducts t k) => HasCoproducts t (Dual k) where
    left = Dual fst
    right = Dual snd
    (Dual f) +++ (Dual g) = Dual (f &&& g)

instance (HasCoproducts t k) => HasProducts t (Dual k) where
    fst = Dual left
    snd = Dual right
    (Dual f) &&& (Dual g) = Dual (f +++ g)

instance (Cartesian t i k) => Cocartesian t i (Dual k)
instance (Cocartesian t i k) => Cartesian t i (Dual k)

instance (Tensor t k) => Tensor t (Dual k) where
    tensor (Dual f) (Dual g) = Dual (tensor f g)

instance (Monoidal t i k) => Monoidal t i (Dual k) where
    leftUnitor = Dual leftUnitorSym
    leftUnitorSym = Dual leftUnitor
    rightUnitor = Dual rightUnitorSym
    rightUnitorSym = Dual rightUnitor
    assoc = Dual assocSym
    assocSym = Dual assoc

instance (SymmetricMonoidal t i k) => SymmetricMonoidal t i (Dual k) where
    swap = Dual swap

instance (MonoidalRecursive t i k) => MonoidalRecursive t i (Dual k) where
    leftRecurse (Dual f) = Dual (leftRecurse f)
    rightRecurse (Dual f) = Dual (rightRecurse f)


--------------------------------------------------------------------------------
-- Categories enriched in some structure

class (Category k) => SemigroupEnriched k where
    (<+>) :: k a b -> k a b -> k a b

class (SemigroupEnriched k) => MonoidEnriched k where
    zero :: k a b

-- Deriving Via helper for zero objects.
-- If a category has an object that is both terminal and initial, we can build maps between any 2 objects
type HasZero i k = (HasTerminal i k, HasInitial i k)

newtype ZeroObject k a b = ZeroObject { unZeroObject :: k a b }
    deriving newtype (Category, SemigroupEnriched)

instance (SemigroupEnriched k, HasTerminal i k, HasInitial i k) => MonoidEnriched k where
    zero = silly . consume

--------------------------------------------------------------------------------
-- Examples:

instance HasTerminal () (->) where
    consume _ = ()

instance HasProducts (,) (->) where
    fst = Prelude.fst
    snd = Prelude.snd
    f &&& g = \x -> (f x , g x)

instance Cartesian (,) () (->)

instance HasInitial Void (->) where
    silly = absurd

instance HasCoproducts Either (->) where
    left = Left
    right = Right
    (+++) = either

instance Cocartesian Either Void (->)

deriving via (CartesianMonoidal (->)) instance Tensor (,) (->)
deriving via (CartesianMonoidal (->)) instance Monoidal (,) () (->)
deriving via (CartesianMonoidal (->)) instance SymmetricMonoidal (,) () (->)
deriving via (CocartesianMonoidal (->)) instance Tensor (Either) (->)
deriving via (CocartesianMonoidal (->)) instance Monoidal Either Void (->)
deriving via (CocartesianMonoidal (->)) instance SymmetricMonoidal Either Void (->)

instance MonoidalClosed (,) () (->) (->) where
    eval (f, a) = f a
    curry = Prelude.curry
    uncurry = Prelude.uncurry