Professor at the University of Edinburgh, contributed to the design of Haskell, Java, and XQuery.

Category theory for the working hacker

We explain why category theory is of interest for developers. The principle of Propositions as Types describes a correspondence between propositions and proofs in logic, on the one hand, and types and programs in computing, on the other. Category theory constitutes a third leg of this correspondence, a doctrine that Robert Harper has christened 'computational trinitarianism'.