Various monoidal categories, monoidal functors, and monoid objects

monoidal.hs

{-# LANGUAGE
    RankNTypes,
    TypeApplications,
    TypeOperators,
    KindSignatures,
    TypeFamilies,
    TypeInType,
    MultiParamTypeClasses,
    FunctionalDependencies,
    FlexibleInstances,
    AllowAmbiguousTypes #-}

module Test where

import Prelude hiding (Monoid)
import qualified Prelude as P
import Data.Proxy
import Control.Applicative
import Data.Functor.Compose
import Data.Functor.Identity
import Control.Monad

class Set p k | p -> k where

class Set p k => Category p k | p -> k where
  type (→) :: k -> k -> *
  infixl 1 →

data (a ≅ b) p = Iso { fwd :: a `p` b, bwd :: b `p` a }
infixl 1 ≅

class Category p k => Monoidal p k | p -> k where
  type (⊗) :: k -> k -> k
  type  I  :: k

  α :: forall (a :: k) (b :: k) (c :: k). ((a ⊗ b) ⊗ c ≅ a ⊗ (b ⊗ c)) (→)
  λ :: forall (a :: k)                  . (I ⊗ a ≅ a) (→)
  ρ :: forall (a :: k)                  . (a ⊗ I ≅ a) (→)

class (Monoidal p c, Monoidal q d) => MonoidalFunctor p q (f :: c -> d) where
  ϕ  :: (f a ⊗ f b) → f (a ⊗ b)
  ϕI :: I → f I

class (Monoidal p c, Monoidal q d) => OpMonoidalFunctor p q (f :: c -> d) where
  ϕ'  :: f (a ⊗ b) → (f a ⊗ f b)
  ϕI' :: f I → I

class Monoidal p k => Monoid p (m :: k) where
  μ :: m ⊗ m → m
  η :: I → m

data Hask

instance Set Hask *

instance Category Hask * where
  type (→) = (->)

instance Monoidal Hask * where
  type (⊗) = (,)
  type  I  = ()
  α = Iso fwd bwd
    where
    fwd ((a, b), c) = (a, (b, c))
    bwd (a, (b, c)) = ((a, b), c)
  ρ = Iso fwd bwd
    where
    fwd (a, _) = a
    bwd a = (a, ())
  λ = Iso fwd bwd
    where
    fwd (_, a) = a
    bwd a = ((), a)

instance Applicative f => MonoidalFunctor Hask Hask f where
  ϕ = uncurry $ liftA2 (,)
  ϕI = pure

instance P.Monoid m => Monoid Hask m where
  μ = uncurry (<>)
  η _ = mempty

data Hask'

newtype f :~> g = Nat { runNat :: forall x. f x -> g x }
newtype (f :&: g) a = Product { runProduct :: (f a, g a) }

-- instance Set Hask' (* -> *)
--
-- instance Category Hask' (* -> *) where
--   type (→) = (:~>)

-- instance Monoidal Hask' (* -> *) where
--   type (⊗) = (:&:)
--   type  I  = (Const ())

-- instance Alternative f => Monoid Hask' f where
--   μ = Nat $ uncurry (<|>) . runProduct
--   η = Nat $ const empty

type f ∘ g = Compose f g

data HaskC

instance Set HaskC (* -> *)

instance Category HaskC (* -> *) where
  type (→) = (:~>)

instance Monoidal HaskC (* -> *) where
  type (⊗) = Compose
  type  I  = Identity

  α = Iso fwd bwd
    where
    -- fwd :: ((f ∘ g) ∘ h) :~> (f ∘ (g ∘ h))
    fwd = Nat $ _ . getCompose . getCompose
    -- bwd :: (f ∘ (g ∘ h)) :~> ((f ∘ g) ∘ h)
    bwd = Nat $ _
  ρ = Iso fwd bwd
    where
    -- fwd :: (f ∘ Identity) :~> f
    fwd = Nat $ _
    -- bwd :: f :~> (f ∘ Identity)
    bwd = Nat $ _
  λ = Iso fwd bwd
    where
    -- fwd :: (Identity ∘ f) :~> f
    fwd = Nat $ _
    -- bwd :: f :~> (Identity ∘ f)
    bwd = Nat $ _

instance Monad m => Monoid HaskC m where
  μ = Nat $ join . getCompose
  η = Nat $ return . runIdentity