[Haskell-beginners] Categories in Haskell

[Ertugrul Söylemez]

Robert Goss <goss.robert at gmail.com> wrote:

> The main issue is that the objects of the category (represented by
> the id morphism) are in bijection to some set of haskell types.
>
> [...]
>
> Now this all makes sense Haskell's categories are for reasoning about
> programs while I want to use it more for pure maths. Has anyone else
> had a similar problem with categories in haskell? Or am I missing a
> way of implementing such structures within the standard Category
> framework for haskell.

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.


Greets,
Ertugrul

-- 
Not to be or to be and (not to be or to be and (not to be or to be and
(not to be or to be and ... that is the list monad.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/beginners/attachments/20130529/7c9ac314/attachment.pgp>