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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
