The Curry–Howard isomorphism

Category theory may seem vary abstract and intimidating, but in fact it is extremely easy to understand. In category theory we look at concrete objects from far away without any regard for the internal structure. This is similar with Bohr's position on physics: physics is about what we can say about nature, and not decide what nature is. Surprisingly, a lot of information about the objects in category theory is derivable from the behavior of the objects and this is where I am ultimately heading with this series on category theory.

Last time I mentioned the origin of category theory as the formalism to clarify when two homology theories are equivalent. But category theory can be started from two other directions as well, and those alternative viewpoints help provide the intuition needed to navigate the abstractions of category theory. One thread of discussion starts with the idea of computability and the work of Alonzo Church and Alan Turing. Turing was Church's student and each started an essential line of research: lambda calculus and universal Turing machines.  Those later grew into one hand functional languages like Java script, and the other hand into object oriented languages like C++. What one can do with lambda calculus can be achieved with universal Turing machines, and the other way around. The essential idea of computer programming is to build complex structures out of simpler building blocks. Object oriented programming starts from the idea of packaging together actions and states. An object is a "black box" containing actions (functions performing computations) and information (the internal state of the object). Functional programming on the other hand lacks the concept of an internal state and you deal only with functions which take an input, crunch the numbers, and then produce an output. The typical example is FORTRAN: FORmula TRANslation (from higher level human understandable syntax into zeroes and ones understandable by a machine).

The second direction one can start category theory is intuitionistic logic and the foundation of set theory. The problem of naive set theory is that one can create paradoxes like Russel's paradox: the set of all sets which are not members of themselves. The solution Russel proposed was type theory. Types introduce structure to set theory preventing self-referential constructions. In computer programming, types are semantic rules which tell us how to understand various sequences of zeros and ones from computer memory as integers, boolean variables, etc.

In intuitionistic logic statements are not true by simply disproving their falsehood, but they are true by providing an explicit construction. Truth must be computed and the parallel with computer programming is obvious. There is a name for this relationship, the Curry-Howard isomorphism. The mathematical formalism needed to rigorously spell out this correspondence is category theory. At high level:

• proofs are programs
• propositions are types

More important is that we can attach logical and programming meaning to category theory constructions which helps dramatically reduce the difficulty of category theory to that of elementary linear algebra. 

There are two additional key points I want to make. First category theory ignores the structure of the objects: they can be sets, topological spaces, posets, even physical systems. As such uniqueness is relaxed in category theory and things are unique up to isomorphisms. Second, we are strengthening uniqueness by seeking universal properties. This gives category theory its abstract flavour: the generalization of standard mathematical concepts in category theory involve diagrams which must commute. The typical definition is something like: "if there is an "impostor" which claims to have the same properties as the concept being defined, then there exist a so and so isomorphism such that a certain diagram commutes which guarantees that the impostor is nothing but a restatement of the same concept up to isomorphism". Next time I will talk about the first key definition we need from category theory, that of a product, and by flipping the arrows that of a coproduct.