Re: [Haskell-beginners] Categories in Haskell

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 :

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

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners