Categories in Haskell

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Categories in Haskell

Robert Goss
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.

class Category m where
  id :: m a a
  comp :: m a b -> m b c -> m a c

The main issue is that the objects of the category (represented by the id
morphism) are in bijection to some set of haskell types.

The problem (I think) this leads too is that

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.
2. This requires representing (for example) all groups as types. In general
I have found while possible it leads to pretty horrendous types.

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.

For a (toy) example take trying to model the category of CyclicGroups

--Cyclic n is the object representing the cyclic group Z_n
newtype Cyclic = Cyclic Int
--CyclicMor n m p is represents a group morphism from Z_n to Z_m taking 1
-> p
newtype CyclicMor = CyclicMor Int Int Int

This now gives the definition of

id :: Cyclic -> CyclicMor
id (Cyclic n) = CyclicMor n n 1

comp :: CyclicMor -> CyclicMor -> Maybe CyclicMor
comp (CyclicMor n m p) (CyclicMor n' m' p')
  | m==n' = Just (CyclicMor n m' (p+p'))
  | otherwise = Nothing

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 :

class OrdinaryCategory m where
  id :: a -> m a a
  comp :: m a b -> m b c -> Maybe (m a c)

I haven't seen a similar construction in haskell libraries does anyone know
if this is because
1. It is already there and I just haven't come across it.
2. It solves a problems that no-one else has had.
3. My idea is fundamentally broken / useless in some key way.

Thanks for any comments anyone has.

Robert
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20130529/d268eeca/attachment.htm>

Reply | Threaded
Open this post in threaded view
|

Categories in Haskell

Ertugrul Söylemez
Robert Goss <goss.robert at gmail.com> wrote:

> The main issue is that the objects of the category (represented by
> the id morphism) are in bijection to some set of haskell types.
>
> [...]
>
> 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.

Perhaps what you need is not a programming language like Haskell, but a
proof assistant like Agda, where you can express arbitrary categories.
A limited form of this is possible in Haskell as well, but the lack of
dependent types would force you through a lot of boilerplate and heavy
value/type/kind lifting.


Greets,
Ertugrul

--
Not to be or to be and (not to be or to be and (not to be or to be and
(not to be or to be and ... that is the list monad.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/beginners/attachments/20130529/7c9ac314/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Categories in Haskell

Robert Goss
On 29 May 2013 22:04, Ertugrul S?ylemez <es at ertes.de> wrote:

>
>
> Perhaps what you need is not a programming language like Haskell, but a
> proof assistant like Agda, where you can express arbitrary categories.
> A limited form of this is possible in Haskell as well, but the lack of
> dependent types would force you through a lot of boilerplate and heavy
> value/type/kind lifting.
>
>
I had had a look at Agda a while ago I will have to have another look. How
possible is it to do computations in Agda? For example is it possible to
compute the equalizer of 2 arrows (obv is a category in which equalizers
exit)?

A part of this was a learning experience it seemed natural to express
certain bits of computer algebra in terms of categories and I wanted to see
how well these ideas could be expressed in haskell.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20130529/5b696d69/attachment.htm>

Reply | Threaded
Open this post in threaded view
|

Categories in Haskell

Peter Hall
I haven't tried Idris yet myself, and I'm not sure how stable it is, but I
think it can do a lot that Agda can do but more suitable for actual
calculations. I would be interested to hear any experiences you have (or
have had) with it.

Peter


On 29 May 2013 23:11, Robert Goss <goss.robert at gmail.com> wrote:

>
>
>
> On 29 May 2013 22:04, Ertugrul S?ylemez <es at ertes.de> wrote:
>
>>
>>
>> Perhaps what you need is not a programming language like Haskell, but a
>> proof assistant like Agda, where you can express arbitrary categories.
>> A limited form of this is possible in Haskell as well, but the lack of
>> dependent types would force you through a lot of boilerplate and heavy
>> value/type/kind lifting.
>>
>>
> I had had a look at Agda a while ago I will have to have another look. How
> possible is it to do computations in Agda? For example is it possible to
> compute the equalizer of 2 arrows (obv is a category in which equalizers
> exit)?
>
> A part of this was a learning experience it seemed natural to express
> certain bits of computer algebra in terms of categories and I wanted to see
> how well these ideas could be expressed in haskell.
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20130530/440b65f8/attachment.htm>

Reply | Threaded
Open this post in threaded view
|

Categories in Haskell

Friedrich Wiemer
I've heard a talk about Idris last weekend at BerlinSides. Looks very
interesting - I think I'll have to take a closer look at it. The guy
said it isn't stable enough for productive use but as Robert asked for
some learning experiences, this should be interessting for him, too.
( Btw: there should be four (?) video lectures about Idris somewhere
at http://idris-lang.org/ )

Friedrich

2013/5/30 Peter Hall <peter.hall at memorphic.com>:

> I haven't tried Idris yet myself, and I'm not sure how stable it is, but I
> think it can do a lot that Agda can do but more suitable for actual
> calculations. I would be interested to hear any experiences you have (or
> have had) with it.
>
> Peter
>
>
> On 29 May 2013 23:11, Robert Goss <goss.robert at gmail.com> wrote:
>>
>>
>>
>>
>> On 29 May 2013 22:04, Ertugrul S?ylemez <es at ertes.de> wrote:
>>>
>>>
>>>
>>> Perhaps what you need is not a programming language like Haskell, but a
>>> proof assistant like Agda, where you can express arbitrary categories.
>>> A limited form of this is possible in Haskell as well, but the lack of
>>> dependent types would force you through a lot of boilerplate and heavy
>>> value/type/kind lifting.
>>>
>>
>> I had had a look at Agda a while ago I will have to have another look. How
>> possible is it to do computations in Agda? For example is it possible to
>> compute the equalizer of 2 arrows (obv is a category in which equalizers
>> exit)?
>>
>> A part of this was a learning experience it seemed natural to express
>> certain bits of computer algebra in terms of categories and I wanted to see
>> how well these ideas could be expressed in haskell.
>>
>> _______________________________________________
>> Beginners mailing list
>> Beginners at haskell.org
>> http://www.haskell.org/mailman/listinfo/beginners
>>
>
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
>


Reply | Threaded
Open this post in threaded view
|

Categories in Haskell

mukesh tiwari
Hi Friedrich,
video lectures and slides of Idris
http://edwinb.wordpress.com/2013/03/15/idris-course-at-itu-slides-and-video/

-Mukesh

On Thu, May 30, 2013 at 12:20 PM, Friedrich Wiemer <
friedrichwiemer at gmail.com> wrote:

> I've heard a talk about Idris last weekend at BerlinSides. Looks very
> interesting - I think I'll have to take a closer look at it. The guy
> said it isn't stable enough for productive use but as Robert asked for
> some learning experiences, this should be interessting for him, too.
> ( Btw: there should be four (?) video lectures about Idris somewhere
> at http://idris-lang.org/ )
>




> Friedrich
>
> 2013/5/30 Peter Hall <peter.hall at memorphic.com>:
> > I haven't tried Idris yet myself, and I'm not sure how stable it is, but
> I
> > think it can do a lot that Agda can do but more suitable for actual
> > calculations. I would be interested to hear any experiences you have (or
> > have had) with it.
> >
> > Peter
> >
> >
> > On 29 May 2013 23:11, Robert Goss <goss.robert at gmail.com> wrote:
> >>
> >>
> >>
> >>
> >> On 29 May 2013 22:04, Ertugrul S?ylemez <es at ertes.de> wrote:
> >>>
> >>>
> >>>
> >>> Perhaps what you need is not a programming language like Haskell, but a
> >>> proof assistant like Agda, where you can express arbitrary categories.
> >>> A limited form of this is possible in Haskell as well, but the lack of
> >>> dependent types would force you through a lot of boilerplate and heavy
> >>> value/type/kind lifting.
> >>>
> >>
> >> I had had a look at Agda a while ago I will have to have another look.
> How
> >> possible is it to do computations in Agda? For example is it possible to
> >> compute the equalizer of 2 arrows (obv is a category in which equalizers
> >> exit)?
> >>
> >> A part of this was a learning experience it seemed natural to express
> >> certain bits of computer algebra in terms of categories and I wanted to
> see
> >> how well these ideas could be expressed in haskell.
> >>
> >> _______________________________________________
> >> Beginners mailing list
> >> Beginners at haskell.org
> >> http://www.haskell.org/mailman/listinfo/beginners
> >>
> >
> >
> > _______________________________________________
> > Beginners mailing list
> > Beginners at haskell.org
> > http://www.haskell.org/mailman/listinfo/beginners
> >
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20130530/3de7a676/attachment.htm>