[Haskell-beginners] Categories in Haskell

[Friedrich Wiemer]

I've heard a talk about Idris last weekend at BerlinSides. Looks very
interesting - I think I'll have to take a closer look at it. The guy
said it isn't stable enough for productive use but as Robert asked for
some learning experiences, this should be interessting for him, too.
( Btw: there should be four (?) video lectures about Idris somewhere
at http://idris-lang.org/ )

Friedrich

2013/5/30 Peter Hall <peter.hall at memorphic.com>:
> I haven't tried Idris yet myself, and I'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.
>
> Peter
>
>
> On 29 May 2013 23:11, Robert Goss <goss.robert at gmail.com> wrote:
>>
>>
>>
>>
>> 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.
>>
>> _______________________________________________
>> Beginners mailing list
>> Beginners at haskell.org
>> http://www.haskell.org/mailman/listinfo/beginners
>>
>
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
>