| > The overlap of mathematicians who care about category theory [...] and mathematicians who program [...] is pretty much zero. You probably won't find your algebraic topology professor programming Well, unless perhaps s/he has some involvement in a project like this one http://comptop.stanford.edu/ ("The overall goal of this project is to develop flexible topological methods which will allow the analysis of data which is difficult to analyze using classical linear methods"; first named person in left sidebar is an algebraic topologist). Or this one http://www.esf.org/index.php?id=8764 ("Applied and Computational Algebraic Topology"; first named person on steering committee is an algebraic topologist). Or this one http://munkres.us.es:8080/groups/catam/ ("Computational Applied Topology and Applied Mathematics"; directory is an algebraic topologist). Or, turning away from algebraic topology as such to mathematics inspired by algebraic topology and involving both category theory and programming: http://homotopytypetheory.org/ ("... new program for a comprehensive, computational foundation for mathematics based on the homotopical interpretation of type theory. [...] currently being implemented with the help of the automated proof assistant Coq"; note that in practice doing nontrivial things in Coq is a matter of functional programming). For sure there are plenty of mathematicians (in algebraic topology and elsewhere) who don't program, but I think the intersection between people interested in categories and people interesting in programming is bigger than you suggest. I don't know how many of them are using Haskell, though. |
If you go to your average mathematics department and ask a few professors there that work in logic, algtop or alggeom, I doubt you'll find any that do any programming for their research. You probably won't find that many logicians that use proof-assistants either, although those are probably the least niche category of the things listed (and they are fairly popular with the CS folks)