<p>This library is not especially useful for category-theoretic proofs, since Haskell's typechecking is not sufficient to verify that the constructions satisfy the required properties. Surprisingly enough ;), it's actually intended to be used for writing Haskell programs. You are best off asking on the <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe">Haskell-cafe mailing list</a> for examples. </p>

CC BY-SA 3.0
2012-05-23T14:32:31.233Z
2012-05-23T14:32:31.233Z
Neel Krishnaswami
<p>See <a href="http://hackage.haskell.org/package/category-extras" rel="nofollow">here</a>. Has anyone attempted to use this to verify category theoretic proofs? Given the relationship between categories and <a href="http://ncatlab.org/nlab/show/quiver" rel="nofollow">graphs</a>, are there some applications with respect to graph algorithms? What other possible uses are there for this package and those associated with it?</p>

<p>I realize this is a broad, open-ended question, which may not be entirely appropriate for Stack Exchange. A better place to post this question could also be a helpful answer.</p>

CC BY-SA 3.0
2012-05-22T23:06:18.627Z
I'm not sure that that package could be used for that but it seems like this paper might help you verify category theoretic proofs http://www.nuprl.org/documents/Kreitz/06ijcar-categories.pdf
Joshua Herman
<pl.programming-languages><functional-programming><ct.category-theory>
What can the Haskell package category-extras be used for?
Cameron Smith
# What can the Haskell package category-extras be used for?

(Asked by: username_0 on 2012-05-22)

See [here](http://hackage.haskell.org/package/category-extras). Has anyone attempted to use this to verify category theoretic proofs? Given the relationship between categories and [graphs](http://ncatlab.org/nlab/show/quiver), are there some applications with respect to graph algorithms? What other possible uses are there for this package and those associated with it?

I realize this is a broad, open-ended question, which may not be entirely appropriate for Stack Exchange. A better place to post this question could also be a helpful answer.

**Tags:** pl.programming-languages, functional-programming, ct.category-theory
> **Comments:**
> **username_1**: I'm not sure that that package could be used for that but it seems like this paper might help you verify category theoretic proofs http://www.nuprl.org/documents/Kreitz/06ijcar-categories.pdf  

---

## 1 answers

### Answer by username_2 on 2012-05-23. Score: 5 | Accepted answer

This library is not especially useful for category-theoretic proofs, since Haskell's typechecking is not sufficient to verify that the constructions satisfy the required properties. Surprisingly enough ;), it's actually intended to be used for writing Haskell programs. You are best off asking on the [Haskell-cafe mailing list](http://www.haskell.org/mailman/listinfo/haskell-cafe) for examples.


---

