Re: [Haskell-beginners] Categories in Haskell

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 wrote:

On 29 May 2013 22:04, Ertugrul Söylemez 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@haskell.org http://www.haskell.org/mailman/listinfo/beginners