[Haskell-beginners] Categories in Haskell
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
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Beginners