[Haskell-cafe] Categories (cont.)

[Jay Sulzberger]

On Thu, 20 Dec 2012, Christopher Howard <christopher.howard at frigidcode.com> wrote:

> 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
> --------

Thank you for this code!

What does the code for going backwards looks like?  That is,
suppose we have an instance of Category with only one object.
What is the Haskell code for the function which takes the
category instance and produces a monoid thing, like your integers
with 1 and usual integer multiplication?  Could we use a
"constraint" at the level of types, or at some other level, to
write the code?  Here by "constraint" I mean something like a
declaration that is a piece of Haskell source code, and not
something the human author of the code uses to write the code.

Maybe "Categorical Programming for Data Types with Restricted
Parametricity" by D. Orchard and Alan Mycroft

   http://www.cl.cam.ac.uk/~dao29/drafts/tfp-structures-orchard12.pdf

has something to do with this.

oo--JS.


>
> -- 
> frigidcode.com
>
>