[Haskell-beginners] Categories in Haskell

Peter Hall peter.hall at memorphic.com
Thu May 30 01:15:31 CEST 2013

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.


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>

More information about the Beginners mailing list