Tool/app for learning category theory?

Question

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.

Answer 1

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).

Answer 2

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.

Answer 3

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.