[Haskell-beginners] 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>