[Haskell-cafe] The meaning of categories constructed from HASK

[David Feuer]

It's generally quite hard or impossible to express commutative diagrams as
Haskell types since it's (currently) impossible to talk about term equality
at the type level. I imagine someone who actually knows category theory can
describe some ways they use such concepts to design or analyse Haskell
code, though.

On Sep 22, 2016 7:26 PM, "Dimitri DeFigueiredo" <defigueiredo at ucdavis.edu>
wrote:

> In category theory, there are many ways one can make new categories out
> of an old one.
>
> In particular, given a category C one can construct:
>
> 1. The arrows category of C:
>         arrows in C become objects and
>         commutative squares in C become arrows
> 2. The slice category of C given an object A:
>         arrows into a distinguished object A become objects in the slice
>         commutative triangles become arrows
>
> There are also functors going from C to these new categories (and back).
>
> Are these constructed categories useful when C = `Hask` (the category of
> haskell types and functions)?
> What do they represent in programming terms?
>
> In other words, is there intuition for what the arrows category of Hask is?
> What about the slice category of Hask over a specific type?
> Do the functors between these match some programming abstractions?
>
> Any pointers are much appreciated.
>
> Thanks,
>
> Dimitri
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160923/ed2a92d0/attachment.html>