[Haskell-cafe] Categories (cont.)

[wren ng thornton]

On 12/20/12 6:42 AM, Christopher Howard wrote:
> code:
> --------
> instance Category Integer where
>
>    id = 1
>
>    (.) = (*)
>
> -- and
>
> instance Category [a] where
>
>    id = []
>    (.) = (++)
> -------
>
> But these lead to kind mis-matches.

As mentioned in my other email (just posted) the kind mismatch is 
because categories are actually monoid-oids[1] not monoids. That is:

     class Monoid (a :: *) where
         mempty  :: a
         mappend :: a -> a -> a

     class Category (a :: * -> * -> *) where
         id  :: a i j
         (.) :: a j k -> a i j -> a i k

Theoretically speaking, every monoid can be considered as a category 
with only one object. Since there's only one object/index, the types for 
id and (.) basically degenerate into the types for mempty and mappend. 
Notably, from this perspective, each of the elements of the carrier set 
of the monoid becomes a morphism in the category--- which some people 
find odd at first.

In order to fake this theory in Haskell we can do:

     newtype MonoidCategory a i j = MC a

     instance Monoid a => Category (MonoidCategory a) where
         id          = MC mempty
         MC f . MC g = MC (f `mappend` g)

This is a fake because technically (MonoidCategory A X Y) is a different 
type than (MonoidCategory A P Q), but since the indices are phantom 
types, we (the programmers) know they're isomorphic. From the category 
theory side of things, we have K*K many copies of the monoid where K is 
the cardinality of the kind "*". We can capture this isomorphism if we like:

     castMC :: MonoidCategory a i j -> MonoidCategory a k l
     castMC (MC a) = MC a

but Haskell won't automatically insert this coercion for us; we gotta do 
it manually. In more recent versions of GHC we can use data kinds in 
order to declare a kind like:

     MonoidCategory :: * -> () -> () -> *

which would then ensure that we can only talk about (MonoidCategory a () 
()). Unfortunately, this would mean we can't use the Control.Category 
type class, since this kind is more restrictive than (* -> * -> * -> *). 
But perhaps in the future that can be fixed by using kind polymorphism...


[1] The "-oid" part just means the indexing. We don't use the term 
"monoidoid" because it's horrific, but we do use a bunch of similar 
terms like semigroupoid, groupoid, etc.

-- 
Live well,
~wren