[Haskell-beginners] Categories in Haskell
goss.robert at gmail.com
Thu May 30 00:11:29 CEST 2013
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
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Beginners