N_P3Ch06c_MonoidalCats

Markdown of literate Haskell program. Program source: /src/CTNotes/P3Ch06c_MonoidalCats.lhs

Notes on monoidal categories in Haskell. Mostly because I will need them later. Very much work-in-progress

Refs:: category-extras, categories packages

 {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, PolyKinds#-}
 {-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}
 {-# LANGUAGE AllowAmbiguousTypes #-} -- needed for NonHaskMonoidal nhassociator
 module CTNotes.P3Ch06c_MonoidalCats where
 import CTNotes.P1Ch08c_BiFunctorNonHask
 import Data.Void
 import Data.Kind (Type)

category-extras, categories define Monoidal in terms of more general type classes: Associative Bifunctor, HasIdentity This bundles the concept into one and uses less generic approach.
i plays the role of identity object, bi is the tensor product.

 class CBifunctor bi cat cat => Monoidal cat bi i | cat bi -> i where
   associator :: cat (bi (bi a b) c) (bi a (bi b c))
   lunitor :: cat (bi i a) a
   runitor :: cat (bi a i) a

Using book notation, these correspond to

α_{a b c} :: (a ⊗ b) ⊗ c -> a ⊗ (b ⊗ c)
λ_a :: i ⊗ a -> a
ρ_a :: a ⊗ i -> a

ghci> :k Monoidal
Monoidal :: (k -> k -> *) -> (k -> k -> k) -> k -> Constraint

Coherence conditions:

TODO

in Haskell:

TODO

Instances

Famously (in pseudo-Haskell)

instance Monoidal Endo Composition Identity

(N_P1Ch07_Functors_Composition) where Endo is category of Endofunctors on Hask, Composition is functor composition, and Identity is identity functor.

TODO category-extras, uses Void as Id for Product. This does not seem right.

 instance Monoidal (->) (,) () where
      associator = undefined
      lunitor = snd
      runitor = fst

Non-Hask generalization

This is conceptual code and I have hard time implementing instances but it conveys the message (more implementable version in N_P3Ch12a_EnrichedPreorder)

 class NonHaskMonoidal (cat :: k -> k -> Type) where
    type (a :: k) :*: (b :: k) :: k
    type IdT :: k
    nhbimap :: cat a c -> cat b d -> cat ( a :*: b) (c :*: d)
    nhassociator :: cat (( a :*: b) :*: c) ( a :*: ( b :*: c))
    nhlunitor :: cat (IdT :*: a) a
    nhrunitor :: cat (a :*: IdT) a

(N_P3Ch12a_EnrichedPreorder notes provide more examples).