Summary and further reading#
In this first chapter, we set the stage for category theory by introducing one of the simplest interesting sorts of example: preorders. From this seemingly simple structure, a bunch of further structure emerges: monotone maps, meets, joins, and more. In terms of modeling real world phenomena, we thought of preorders as the states of a system, and monotone maps as describing a way to use one system to observe another. From this point of view, generative effects occur when observations of the whole cannot be deduced by combining observations of the parts.
In the final section we introduced Galois connections. A Galois connection, or adjunction, is a pair of maps that are like inverses, but allowed to be more โrelaxedโ by getting the orders involved. Perhaps surprisingly, it turns out adjunctions are closely related to joins and meets: if a preorder \(๐\) has all joins, then a monotone map out of \(๐\) is a left adjoint if and only if it preserves joins; similarly for meets and right adjoints.
The next two chapters build significantly on this material, but in two different directions. Chapter 2 adds a new operation on the underlying set: it introduces the idea of a monoidal structure on preorders. This allows us to construct an element \(๐ โ ๐\) of a preorder \(๐\) from any elements \(๐,๐ โ ๐\), in a way that respects the order. On the other hand, Chapter 3 adds new structure on the order itself: it introduces the idea of a morphism, which describes not only whether \(๐ โค ๐\), but gives a name \(๐\) for how \(๐\) relates to \(๐\). This structure is known as a category. These generalizations are both fundamental to the story of compositionality, and in Chapter 4 weโll see them meet in the concept of a monoidal category. The lessons we have learned in this chapter will illuminate the more highly-structured generalizations in the chapters to come. Indeed, it is a useful principle in studying category theory to try to understand concepts first in the setting of preordersโwhere often much of the complexity is stripped away and one can develop some intuitionโbefore considering the general case.
But perhaps you might be interested in exploring some ideas in this chapter in other directions. While we wonโt return to them in this book, we learned about generative effects from Elie Adamโs thesis (Systems, generativity and interactional effects), and a much richer treatment of generative effect can be found there. In particular, he discusses abelian categories and cohomology, providing a way to detect generative effects in quite a general setting.
Another important application of preorders, monotone maps, and Galois connections is to the analysis of programming languages. In this setting, preorders describe the possible states of a computer, and monotone maps describe the action of programs, or relationships between different ways of modeling computation states. Galois connections are useful for showing how different models may be closely related, and for transporting program analysis from one framework to another. For more detail on this, see Chapter 4 of the textbook [NNH99].