constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A Categorical Manifesto is an article written by Joseph Goguen, encouraging the use of category theory in computer science.
To quote from his introduction:
This paper tries to explain why category theory is useful in computing science. The basic answer is that computing science is a young field that is growing rapidly, is poorly organised, and needs all the help it can get, and that category theory can provide help with at least the following:
Formulating definitions and theories. In computing science, it is often more difficult to formulate concepts and results than to give a proof. The seven guidelines of this paper can help with formulation; the guidelines can also be used to measure the elegance and coherence of existing formulations.
Carrying out proofs. Once basic concepts have been correctly formulated in a categorical language, it often seems that proofs “just happen”: at each step, there is a “natural” thing to try, and it works. Diagram chasing provides many examples of this. It could almost be said that the purpose of category theory is to reduce all proofs to such simple calculations.
Discovering and exploiting relations with other fields. Sufficiently abstract formulations can reveal surprising connections. For example, an analogy between Petri nets and the -calculus might suggest looking for a closed category structure on the category of Petri nets.
Dealing with abstraction and representation independence. In computing science, more abstract viewpoints are often more useful, because of the need to achieve independence from the often overwhelmingly complex details of how things are represented or implemented. A corollary of the first guideline is that two objects are “abstractly the same” if they are isomorphic. Moreover, universal constructions (i.e., adjoints) define their results uniquely up to isomorphism, i.e., “abstractly” in just this sense.
Formulating conjectures and research directions. Connections with other fields can suggest new questions in your own field. Also the seven guidelines can help to guide research. For example, if you have found an interesting functor, then you might be well advised to investigate its adjoints.
Unification. Computing science is very fragmented, with many different sub-disciplines having many different schools within them. Hence, we badly need the kind of conceptual unification that category theory can provide.
This paper tries to explain why and how category theory is useful in computing science, by giving guidelines for applying seven basic categorical concepts: category, functor, natural transformation, limit, adjoint, colimit and comma category. Some examples, intuition, and references are given for each concept, but completeness is not attempted. Some additional categorical concepts and some suggestions for further research are also mentioned. The paper concludes with some philosophical discussion.
Last revised on November 10, 2020 at 06:23:50. See the history of this page for a list of all contributions to it.