On 29 May 2013 22:04, Ertugrul Söylemez <es@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.