<div dir="ltr">I haven&#39;t tried Idris yet myself, and I&#39;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.<div>

<br></div><div style>Peter</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On 29 May 2013 23:11, Robert Goss <span dir="ltr">&lt;<a href="mailto:goss.robert@gmail.com" target="_blank">goss.robert@gmail.com</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="im"><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>
<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><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>
<br>_______________________________________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org">Beginners@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/beginners" target="_blank">http://www.haskell.org/mailman/listinfo/beginners</a><br>
<br></blockquote></div><br></div>