<div dir="ltr"><br><div class="gmail_extra">Hi Friedrich,</div><div class="gmail_extra">video lectures and slides of Idris<br><a href="http://edwinb.wordpress.com/2013/03/15/idris-course-at-itu-slides-and-video/">http://edwinb.wordpress.com/2013/03/15/idris-course-at-itu-slides-and-video/</a><br>
<br></div><div class="gmail_extra">-Mukesh<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, May 30, 2013 at 12:20 PM, Friedrich Wiemer <span dir="ltr"><<a href="mailto:friedrichwiemer@gmail.com" target="_blank">friedrichwiemer@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I've heard a talk about Idris last weekend at BerlinSides. Looks very<br>
interesting - I think I'll have to take a closer look at it. The guy<br>
said it isn't stable enough for productive use but as Robert asked for<br>
some learning experiences, this should be interessting for him, too.<br>
( Btw: there should be four (?) video lectures about Idris somewhere<br>
at <a href="http://idris-lang.org/" target="_blank">http://idris-lang.org/</a> )<br></blockquote><div> </div><div><br><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
Friedrich<br>
<br>
2013/5/30 Peter Hall <<a href="mailto:peter.hall@memorphic.com">peter.hall@memorphic.com</a>>:<br>
> I haven't tried Idris yet myself, and I'm not sure how stable it is, but I<br>
> think it can do a lot that Agda can do but more suitable for actual<br>
> calculations. I would be interested to hear any experiences you have (or<br>
> have had) with it.<br>
><br>
> Peter<br>
><br>
><br>
> On 29 May 2013 23:11, Robert Goss <<a href="mailto:goss.robert@gmail.com">goss.robert@gmail.com</a>> wrote:<br>
>><br>
>><br>
>><br>
>><br>
>> On 29 May 2013 22:04, Ertugrul Söylemez <<a href="mailto:es@ertes.de">es@ertes.de</a>> wrote:<br>
>>><br>
>>><br>
>>><br>
>>> 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>
>><br>
>> I had had a look at Agda a while ago I will have to have another look. How<br>
>> possible is it to do computations in Agda? For example is it possible to<br>
>> compute the equalizer of 2 arrows (obv is a category in which equalizers<br>
>> exit)?<br>
>><br>
>> A part of this was a learning experience it seemed natural to express<br>
>> certain bits of computer algebra in terms of categories and I wanted to see<br>
>> how well these ideas could be expressed in haskell.<br>
>><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>
><br>
><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>
<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>
</blockquote></div><br></div></div>