[Haskell-beginners] Categories in Haskell

[Robert Goss]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20130529/5b696d69/attachment.htm>