<div dir="ltr"><div><div><div><div><div><div><div><div><div>I am interested in trying to use category to perform some mathematical computations. It seems natural to want to talk about categories of mathematical objects e.g. Groups,Rings,Algebras ... etc. But I have found some difficulty doing this with Haskell's standard Category libraries. <br>
<br></div><div>class Category m where<br></div><div> id :: m a a<br></div><div> comp :: m a b -> m b c -> m a c<br></div><div><br></div>The main issue is that the objects of the category (represented by the id morphism) are in bijection to some set of haskell types. <br>
<br></div>The problem (I think) this leads too is that<br><br>1. All the objects that may appear in a program must be known to the compiler. Which leads to problems (for me at least) as the application I want to study I don't know all the (Groups,Rings,... etc) that I will need.<br>
</div>2. This requires representing (for example) all groups as types. In general I have found while possible it leads to pretty horrendous types.<br><br></div>Now this all makes sense Haskell's categories are for reasoning about programs while I want to use it more for pure maths. Has anyone else had a similar problem with categories in haskell? Or am I missing a way of implementing such structures within the standard Category framework for haskell.<br>
<br></div><div>For a (toy) example take trying to model the category of CyclicGroups<br><br></div><div>--Cyclic n is the object representing the cyclic group Z_n<br></div><div>newtype Cyclic = Cyclic Int<br></div><div>--CyclicMor n m p is represents a group morphism from Z_n to Z_m taking 1 -> p<br>
</div><div>newtype CyclicMor = CyclicMor Int Int Int<br><br></div><div>This now gives the definition of <br><br></div><div>id :: Cyclic -> CyclicMor<br></div><div>id (Cyclic n) = CyclicMor n n 1<br><br></div><div>comp :: CyclicMor -> CyclicMor -> Maybe CyclicMor<br>
</div><div>comp (CyclicMor n m p) (CyclicMor n' m' p') <br></div><div> | m==n' = Just (CyclicMor n m' (p+p'))<br></div><div> | otherwise = Nothing<br></div><div><br></div><div>The main loss in this approach is compiler can no longer determine if morphisms are compatible. In my project I use a slightly more generic variant :<br>
</div><br></div>class OrdinaryCategory m where<br></div> id :: a -> m a a<br></div> comp :: m a b -> m b c -> Maybe (m a c)<br><br></div><div>I haven't seen a similar construction in haskell libraries does anyone know if this is because<br>
</div><div>1. It is already there and I just haven't come across it.<br></div><div>2. It solves a problems that no-one else has had.<br></div><div>3. My idea is fundamentally broken / useless in some key way.<br><br>Thanks for any comments anyone has.<br>
<br></div><div>Robert<br></div><div><br></div><br></div>