[Haskell-beginners] Categories in Haskell

[mukesh tiwari]

Hi Friedrich,
video lectures and slides of Idris
http://edwinb.wordpress.com/2013/03/15/idris-course-at-itu-slides-and-video/

-Mukesh

On Thu, May 30, 2013 at 12:20 PM, Friedrich Wiemer <
friedrichwiemer at gmail.com> wrote:

> 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
> >
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20130530/3de7a676/attachment.htm>