[Haskell-cafe] Categories (cont.)

[Christopher Howard]

On 12/20/2012 03:59 AM, wren ng thornton wrote:
> On 12/20/12 6:42 AM, Christopher Howard wrote:
> 
> 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.
> 

Finally... I actually made some measurable progress, using these
"phantom types" you mentioned:

code:
--------
import Control.Category

newtype Product i j = Product Integer

  deriving (Show)

instance Category Product where

  id = Product 1

  Product a . Product b = Product (a * b)
--------

I can do composition, illustrate identity, and illustrate associativity:

code:
--------
h> Product 5 >>> Product 2
Product 10

h> Control.Category.id (Product 3)
Product 3

h> Control.Category.id <<< Product 3
Product 3
h> Product 3 <<< Control.Category.id
Product 3

h> (Product 2 <<< Product 3) <<< Product 5
Product 30
h> Product 2 <<< (Product 3 <<< Product 5)
Product 30
--------

-- 
frigidcode.com

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 553 bytes
Desc: OpenPGP digital signature
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121220/0fdfe499/attachment.pgp>