<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On 29 May 2013 22:04, Ertugrul Söylemez <span dir="ltr">&lt;<a href="mailto:es@ertes.de" target="_blank">es@ertes.de</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br><div class="im">
<br>
</div>Perhaps what you need is not a programming language like Haskell, but a<br>
proof assistant like Agda, where you can express arbitrary categories.<br>
A limited form of this is possible in Haskell as well, but the lack of<br>
dependent types would force you through a lot of boilerplate and heavy<br>
value/type/kind lifting.<br>
<br></blockquote></div><br></div><div class="gmail_extra">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)?<br>
<br></div><div class="gmail_extra">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.<br>
</div></div>