
On 12/20/12 7:07 PM, Christopher Howard wrote:
On 12/20/2012 03:59 AM, wren ng thornton wrote:
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...
Finally... I actually made some measurable progress, using these "phantom types" you mentioned:
Yep, everything should work fine with the phantom types. The only problem is, as I mentioned, that you're not really getting the category associated with the underlying monoid, you're getting a whole bunch of copies of that monoid (one copy for each instantiation of the phantom types). -- Live well, ~wren