Category theory

Category theory is an approach to mathematics which unifies computation, logic, and topology. It was originally created to study wikipedia:algebraic topology and define wikipedia:naturality. Instead of studying individual objects, category theory studies relationships and transformations between objects. Categories can be seen as generalizations of sets, groups, and other common mathematical gadgets.

Several facets of programming-language design can be simplified using category theory. Type theory is interpreted using categories. Kan extensions describe optimizations which use intermediate representations. Infamously, monads represent effects, and less famously, comonads represent contexts.

Introduction

A category can also be thought of as—but is not equivalent to—a labeled digraph: a set of nodes containing values with directed edges mapping nodes to other nodes. In the more general way of thought, a category is a class of "objects"—which can be any type of arbitrary thing—with "arrows" (also called "morphisms") between them mapping one to another. An arrow represents some sort of transformation between a "domain" (the object from which the arrow originates) and the "codomain" (the destination object).

Categories also have some sort of operation for composing arrows, written f ∘ g. This leads to the property that, if there is are two arrows f : A → B and g : B → C, then there is another arrow f ∘ g : A → C. This should be reminiscent of function composition in other areas of mathematics, but represents a more general concept. Note that it is required that ∘ is associative—that is, (f ∘ g) ∘ h ≡ f ∘ (g ∘ h).

The final requirement for a category is that every object A has an "identity morphism" idA. For every morphism f : A → B, The identity object has the property that f ∘ idA ≡ f, and for every morphism g : B → A, idA ∘ g ≡ g

Higher Categories

In certain contexts, such as topology, it is natural to define 2-morphisms, things similar to morphisms whose domains and codomains are themselves morphisms. These can be composed in more varied ways, and lead to a generalization of associativity known as a coherence law. There is a hierarchy of k-morphisms parameterized by natural numbers, which may or may not be directed. The study of categories with such higher k-morphisms is known as Higher Category Theory, and is discussed in detail on The nLab.

Automatic Language Generation

Given a category, we can follow a recipe to generate the semantics for a language which studies that category. If facts about the original category are computable, then the resulting language is computable too.

Native Type Theory

Conversely, given a language, we can generate a type theory and associated category. The resulting type theory is called the native type theory. Even dynamically-typed languages often have useful native type theories.

Codensity Monads

The (right) Kan extension of a functor along itself always generates a monad, known as the wikipedia:codensity monad. Common advice from category theorists, e.g. in [1], is:

Whenever you meet a functor, ask what its codensity monad is.

As explained in "Kan Extensions for Program Optimization", continuation monads arise as special cases of codensity monads. Continuation monads are known as "mothers of all monads" in the sense that all effect monads factor through them. In "Colored Functions and Monadic Effects", the concept of colored functions is explained in terms of continuation monads.