Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Being a programmer I appreciate the errors given by a compiler for a programming language and come to rely on the compiler's error as a safety net.

In learning category theory I would like to have some tool that also acted as a safety net letting me experiment with diagrams and pointing out my mistakes when I make one. Does such a tool/app exist?

I know this is more of a math question, but I am asking here because I am looking for an answer from those with and understanding for computer science.

share|cite|improve this question
up vote 6 down vote accepted

There are at least three encodings of (aspects of) Category Theory in Coq. Approaches using a proof assistant guarantee correctness by design, though I don't know whether they will enhance understand. You'll then have both the proof assistant and Category Theory to learn.

If you want a reasonably introductory, computer science-oriented book, it's hard to beat Categories and Computer Science by R. F. C. Walters. His examples are mostly about data types and automata, rather than programming languages and lambdas. Conceptual Mathematics by Lawvere and Schanuel is also quite digestable.

One approach combining these two is to use this Coq formalisation with Steve Awodey’s Book. The formalisation covers closely what is in the book. There's also a blog post about it.

That said, Category Theory is tough and its relationship with programming quickly becomes quite distant, and so one needs to rely on one's mathematical background (which is now getting on to be 20 years old).

share|cite|improve this answer

Please have a look at this blog:

Introduction to Category Theory in Scala

It uses Scalaz libray for category theory. There are some in Haskell.

share|cite|improve this answer

If you are looking for a tutorial application :

The Introduction to Graphical Database for Category Theory (GDCT) is a research project at Mount Allison University. It allows for the creation, editing, and storage of finitely presented categories.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.