Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Various monoidal categories, monoidal functors, and monoid objects
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment