A PDF version of this post is available on GitHub.

Dependent types, in programming, are families of types indexed by elements of an indexing type. For instance, counted vectors are families of tuples indexed by natural numbers—the lengths of the vectors.

In category theory we model dependent types as fibrations. We start with the total space , the base space , and a projection, or a display map, . The fibers of correspond to members of the type family. For instance, the total space, or the bundle, of counted vectors is the list type (a free monoid generated by ) with the projection that returns the length of a list.

Another way of looking at dependent types is as objects in the slice category . Counted vectors, for instance, are represented as objects in given by pairs . Morphisms in the slice category correspond to fibre-wise mappings between bundles.

We often require that be a locally cartesian closed category, that is a category whose slice categories are cartesian closed. In such categories, the base-change functor has both the left adjoint, the dependent sum ; and the right adjoint, the dependent product . The base-change functor is defined as a pullback:

This pullback defines a *cartesian product* in the slice category between two objects: and . In a locally cartesian closed category, this product has the right adjoint, the internal hom in .

# Dependent optics

The most general optic is given by two monoidal actions and in two categories and . It can be written as the following coend of the product of two hom-sets:

Monoidal actions are parameterized by objects in a monoidal category .

Dependent optics are a special case of general optics, where one or both categories in question are slice categories. When the monoidal action is defined in the slice category, the transformations must respect fibrations. For instance, the action in the bundle over must commute with the projection:

This is reminiscent of gauge transformations in physics, which act on fibers in bundles over spacetime. The action must respect the monoidal structure of so, for instance,

We can define a dependent (mixed) optic as:

Just like regular optics, dependent optics can be represented using Tambara modules, which are profunctors with the additional structure given by transformations:

where and are objects in the appropriate slice categories.

The optic is then given by the following end in the Tambara category:

# Dependent lens

The primordial optic, the lens, is defined by the monoidal action of a product. By analogy, we define a dependent lens by the action of the product in a slice category. The action parameterized by an object on another object is given by the pullback:

Since a pullback is the product in the slice category , it is automatically associative and unital, so it can be used to define a dependent lens:

Since is locally cartesian closed, there is an adjunction between the product and the exponential. We can use it to get:

We can then apply the Yoneda lemma to get the setter/getter form:

The internal hom in a locally cartesian closed category can be expressed using a dependent product:

where is the fibration of , is the right adjoint to the base change functor, and is the base-change functor along .

The dependent lens can be written as:

In particular, if is , this is equal to an infinite tuple of functions:

or fiber-wise pairs of setter/getter indexed by .

# Traversals

Traversals are optics whose monoidal action is generated by polynomial functors of the form:

The coefficients can be expressed as a fibration , with , the sum of the fibers. The set of powers of can be similarly written as , with the type of list of (a free monoid generated by ), and the function that assigns the length to a list. The monoidal action can then be written using a product (pullback) in the slice category :

There is an obvious forgetful functor , which can be used to express the polynomial action:

The traversal is the optic:

Eqivalently, the second factor can be rewritten as:

This, in turn, is equivalent to a single hom-set in the slice category:

where is the projection from the cartesian product.

The traversal is therefore a mixed optic:

The second factor can be transformed using the internal hom adjunction:

We can then use the ninja Yoneda lemma on the optic to “integrate” over and get:

which, in components, reads: