Programming

Archived Posts from this Category

April 5, 2022

Teaching optics through conspiracy theories

Posted by Bartosz Milewski under Category Theory, Functional Programming, Haskell, Lens, Programming
[5] Comments

This post is based on the talk I gave at Functional Conf 2022. There is a video recording of this talk.

Disclaimers

Data types may contain secret information. Some of it can be extracted, some is hidden forever. We’re going to get to the bottom of this conspiracy.

No data types were harmed while extracting their secrets.

No coercion was used to make them talk.

We’re talking, of course, about unsafeCoerce, which should never be used.

Implementation hiding

The implementation of a function, even if it’s available for inspection by a programmer, is hidden from the program itself.

What is this function, with the suggestive name double, hiding inside?

`x`	`double x`
2	4
3	6
-1	-2

Best guess: It’s hiding 2. It’s probably implemented as:

double x = 2 * x

How would we go about extracting this hidden value? We can just call it with the unit of multiplication:

double 1
> 2

Is it possible that it’s implemented differently (assuming that we’ve already checked it for all values of the argument)? Of course! Maybe it’s adding one, multiplying by two, and then subtracting two. But whatever the actual implementation is, it must be equivalent to multiplication by two. We say that the implementaion is isomorphic to multiplying by two.

Functors

Functor is a data type that hides things of type a. Being a functor means that it’s possible to modify its contents using a function. That is, if we’re given a function a->b and a functorful of a‘s, we can create a functorful of b‘s. In Haskell we define the Functor class as a type constructor equipped with the method fmap:

class Functor f where
  fmap :: (a -> b) -> f a -> f b

A standard example of a functor is a list of a‘s. The implementation of fmap applies a function g to all its elements:

instance Functor [] where
  fmap g [] = []
  fmap g (a : as) = (g a) : fmap g as

Saying that something is a functor doesn’t guarantee that it actually “contains” values of type a. But most data structures that are functors will have some means of getting at their contents. When they do, you can verify that they change their contents after applying fmap. But there are some sneaky functors.

For instance Maybe a tells us: Maybe I have an a, maybe I don’t. But if I have it, fmap will change it to a b.

instance Functor Maybe where
  fmap g Empty = Empty
  fmap g (Just a) = Just (g a)

A function that produces values of type a is also a functor. A function e->a tells us: I’ll produce a value of type a if you ask nicely (that is call me with a value of type e). Given a producer of a‘s, you can change it to a producer of b‘s by post-composing it with a function g :: a -> b:

instance Functor ((->) e) where
  fmap g f = g . f

Then there is the trickiest of them all, the IO functor. IO a tells us: Trust me, I have an a, but there’s no way I could tell you what it is. (Unless, that is, you peek at the screen or open the file to which the output is redirected.)

Continuations

A continuation is telling us: Don’t call us, we’ll call you. Instead of providing the value of type a directly, it asks you to give it a handler, a function that consumes an a and returns the result of the type of your choice:

type Cont a = forall r. (a -> r) -> r

You’d suspect that a continuation either hides a value of type a or has the means to produce it on demand. You can actually extract this value by calling the continuation with an identity function:

runCont :: Cont a -> a
runCont k = k id

In fact Cont a is for all intents and purposes equivalent to a–it’s isomorphic to it. Indeed, given a value of type a you can produce a continuation as a closure:

mkCont :: a -> Cont a
mkCont a = \k -> k a

The two functions, runCont and mkCont are the inverse of each other thus establishing the isomorphism Cont a ~ a.

The Yoneda Lemma

Here’s a variation on the theme of continuations. Just like a continuation, this function takes a handler of a‘s, but instead of producing an x, it produces a whole functorful of x‘s:

type Yo f a = forall x. (a -> x) -> f x

Just like a continuation was secretly hiding a value of the type a, this data type is hiding a whole functorful of a‘s. We can easily retrieve this functorful by using the identity function as the handler:

runYo :: Functor f => Yo f a -> f a
runYo g = g id

Conversely, given a functorful of a‘s we can reconstruct Yo f a by defining a closure that fmap‘s the handler over it:

mkYo :: Functor f => f a -> Yo f a
mkYo fa = \g -> fmap g fa

Again, the two functions, runYo and mkYo are the inverse of each other thus establishing a very important isomorphism called the Yoneda lemma:

Yo f a ~ f a

Both continuations and the Yoneda lemma are defined as polymorphic functions. The forall x in their definition means that they use the same formula for all types (this is called parametric polymorphism). A function that works for any type cannot make any assumptions about the properties of that type. All it can do is to look at how this type is packaged: Is it passed inside a list, a function, or something else. In other words, it can use the information about the form in which the polymorphic argument is passed.

Existential Types

One cannot speak of existential types without mentioning Jean-Paul Sartre.
sartre_22
An existential data type says: There exists a type, but I’m not telling you what it is. Actually, the type has been known at the time of construction, but then all its traces have been erased. This is only possible if the data constructor is itself polymorphic. It accepts any type and then immediately forgets what it was.

Here’s an extreme example: an existential black hole. Whatever falls into it (through the constructor BH) can never escape.

data BlackHole = forall a. BH a

Even a photon can’t escape a black hole:

bh :: BlackHole
bh = BH "Photon"

We are familiar with data types whose constructors can be undone–for instance using pattern matching. In type theory we define types by providing introduction and elimination rules. These rules tell us how to construct and how to deconstruct types.

But existential types erase the type of the argument that was passed to the (polymorphic) constructor so they cannot be deconstructed. However, not all is lost. In physics, we have Hawking radiation escaping a black hole. In programming, even if we can’t peek at the existential type, we can extract some information about the structure surrounding it.

Here’s an example: We know we have a list, but of what?

data SomeList = forall a. SomeL [a]

It turns out that to undo a polymorphic constructor we can use a polymorphic function. We have at our disposal functions that act on lists of arbitrary type, for instance length:

length :: forall a. [a] -> Int

The use of a polymorphic function to “undo” a polymorphic constructor doesn’t expose the existential type:

len :: SomeList -> Int
len (SomeL as) = length as

Indeed, this works:

someL :: SomeList
someL = SomeL [1..10]
> len someL
> 10

Extracting the tail of a list is also a polymorphic function. We can use it on SomeList without exposing the type a:

trim :: SomeList -> SomeList
trim (SomeL []) = SomeL []
trim (SomeL (a: as)) = SomeL as

Here, the tail of the (non-empty) list is immediately stashed inside SomeList, thus hiding the type a.

But this will not compile, because it would expose a:

bad :: SomeList -> a
bad (SomeL as) = head as

Producer/Consumer

Existential types are often defined using producer/consumer pairs. The producer is able to produce values of the hidden type, and the consumer can consume them. The role of the client of the existential type is to activate the producer (e.g., by providing some input) and passing the result (without looking at it) directly to the consumer.

Here’s a simple example. The producer is just a value of the hidden type a, and the consumer is a function consuming this type:

data Hide b = forall a. Hide a (a -> b)

All the client can do is to match the consumer with the producer:

unHide :: Hide b -> b
unHide (Hide a f) = f a

This is how you can use this existential type. Here, Int is the visible type, and Char is hidden:

secret :: Hide Int
secret = Hide 'a' (ord)

The function ord is the consumer that turns the character into its ASCII code:

> unHide secret
> 97

Co-Yoneda Lemma

There is a duality between polymorphic types and existential types. It’s rooted in the duality between universal quantifiers (for all, $\forall$ ) and existential quantifiers (there exists, $\exists$ ).

The Yoneda lemma is a statement about polymorphic functions. Its dual, the co-Yoneda lemma, is a statement about existential types. Consider the following type that combines the producer of x‘s (a functorful of x‘s) with the consumer (a function that transforms x‘s to a‘s):

data CoYo f a = forall x. CoYo (f x) (x -> a)

What does this data type secretly encode? The only thing the client of CoYo can do is to apply the consumer to the producer. Since the producer has the form of a functor, the application proceeds through fmap:

unCoYo :: Functor f => CoYo f a -> f a
unCoYo (CoYo fx g) = fmap g fx

The result is a functorful of a‘s. Conversely, given a functorful of a‘s, we can form a CoYo by matching it with the identity function:

mkCoYo :: Functor f => f a -> CoYo f a
mkCoYo fa = CoYo fa id

This pair of unCoYo and mkCoYo, one the inverse of the other, witness the isomorphism

CoYo f a ~ f a

In other words, CoYo f a is secretly hiding a functorful of a‘s.

Contravariant Consumers

The informal terms producer and consumer, can be given more rigorous meaning. A producer is a data type that behaves like a functor. A functor is equipped with fmap, which lets you turn a producer of a‘s to a producer of b‘s using a function a->b.

Conversely, to turn a consumer of a‘s to a consumer of b‘s you need a function that goes in the opposite direction, b->a. This idea is encoded in the definition of a contravariant functor:

class Contravariant f where
  contramap :: (b -> a) -> f a -> f b

There is also a contravariant version of the co-Yoneda lemma, which reverses the roles of a producer and a consumer:

data CoYo' f a = forall x. CoYo' (f x) (a -> x)

Here, f is a contravariant functor, so f x is a consumer of x‘s. It is matched with the producer of x‘s, a function a->x.

As before, we can establish an isomorphism

CoYo' f a ~ f a

by defining a pair of functions:

unCoYo' :: Contravariant f => CoYo' f a -> f a
unCoYo' (CoYo' fx g) = contramap g fx

mkCoYo' :: Contravariant f => f a -> CoYo' f a
mkCoYo' fa = CoYo' fa id

Existential Lens

A lens abstracts a device for focusing on a part of a larger data structure. In functional programming we deal with immutable data, so in order to modify something, we have to decompose the larger structure into the focus (the part we’re modifying) and the residue (the rest). We can then recreate a modified data structure by combining the new focus with the old residue. The important observation is that we don’t care what the exact type of the residue is. This description translates directly into the following definition:

data Lens' s a =
  forall c. Lens' (s -> (c, a)) ((c, a) -> s)

Here, s is the type of the larger data structure, a is the type of the focus, and the existentially hidden c is the type of the residue. A lens is constructed from a pair of functions, the first decomposing s and the second recomposing it.
SimpleLens

Given a lens, we can construct two functions that don’t expose the type of the residue. The first is called get. It extracts the focus:

toGet :: Lens' s a -> (s -> a)
toGet (Lens' frm to) = snd . frm

The second, called set replaces the focus with the new value:

toSet :: Lens' s a -> (s -> a -> s)
toSet (Lens' frm to) = \s a -> to (fst (frm s), a)

Notice that access to residue not possible. The following will not compile:

bad :: Lens' s a -> (s -> c)
bad (Lens' frm to) = fst . frm

But how do we know that a pair of a getter and a setter is exactly what’s hidden in the existential definition of a lens? To show this we have to use the co-Yoneda lemma. First, we have to identify the producer and the consumer of c in our existential definition. To do that, notice that a function returning a pair (c, a) is equivalent to a pair of functions, one returning c and another returning a. We can thus rewrite the definition of a lens as a triple of functions:

data Lens' s a = 
  forall c. Lens' (s -> c) (s -> a) ((c, a) -> s)

The first function is the producer of c‘s, so the rest will define a consumer. Recall the contravariant version of the co-Yoneda lemma:

data CoYo' f s = forall c. CoYo' (f c) (s -> c)

We can define the contravariant functor that is the consumer of c‘s and use it in our definition of a lens. This functor is parameterized by two additional types s and a:

data F s a c = F (s -> a) ((c, a) -> s)

This lets us rewrite the lens using the co-Yoneda representation, with f replaced by (partially applied) F s a:

type Lens' s a = CoYo' (F s a) s

We can now use the isomorphism CoYo' f s ~ f s. Plugging in the definition of F, we get:

Lens' s a ~ CoYo' (F s a) s
CoYo' (F s a) s ~ F s a s
F s a s ~ (s -> a) ((s, a) -> s)

We recognize the two functions as the getter and the setter. Thus the existential representation of the lens is indeed isomorphic to the getter/setter pair.

Type-Changing Lens

The simple lens we’ve seen so far lets us replace the focus with a new value of the same type. But in general the new focus could be of a different type. In that case the type of the whole thing will change as well. A type-changing lens thus has the same decomposition function, but a different recomposition function:

data Lens s t a b =
forall c. Lens (s -> (c, a)) ((c, b) -> t)

As before, this lens is isomorphic to a get/set pair, where get extracts an a:

toGet :: Lens s t a b -> (s -> a)
toGet (Lens frm to) = snd . frm

and set replaces the focus with a new value of type b to produce a t:

toSet :: Lens s t a b -> (s -> b -> t)
toSet (Lens frm to) = \s b -> to (fst (frm s), b)

Other Optics

The advantage of the existential representation of lenses is that it easily generalizes to other optics. The idea is that a lens decomposes a data structure into a pair of types (c, a); and a pair is a product type, symbolically $c \times a$

data Lens s t a b =
forall c. Lens (s -> (c, a))
               ((c, b) -> t)

A prism does the same for the sum data type. A sum $c + a$ is written as Either c a in Haskell. We have:

data Prism s t a b =
forall c. Prism (s -> Either c a)
                (Either c b -> t)

We can also combine sum and product in what is called an affine type $c_1 + c_2 \times a$ . The resulting optic has two possible residues, c1 and c2:

data Affine s t a b =
forall c1 c2. Affine (s -> Either c1 (c2, a))
                     (Either c1 (c2, b) -> t)

The list of optics goes on and on.

Profunctors

A producer can be combined with a consumer in a single data structure called a profunctor. A profunctor is parameterized by two types; that is p a b is a consumer of a‘s and a producer of b‘s. We can turn a consumer of a‘s and a producer of b‘s to a consumer of s‘s and a producer of t‘s using a pair of functions, the first of which goes in the opposite direction:

class Profunctor p where
  dimap :: (s -> a) -> (b -> t) -> p a b -> p s t

The standard example of a profunctor is the function type p a b = a -> b. Indeed, we can define dimap for it by precomposing it with one function and postcomposing it with another:

instance Profunctor (->) where
  dimap in out pab = out . pab . in

Profunctor Optics

We’ve seen functions that were polymorphic in types. But polymorphism is not restricted to types. Here’s a definition of a function that is polymorphic in profunctors:

type Iso s t a b = forall p. Profunctor p =>
  p a b -> p s t

This function says: Give me any producer of b‘s that consumes a‘s and I’ll turn it into a producer of t‘s that consumes s‘s. Since it doesn’t know anything else about its argument, the only thing this function can do is to apply dimap to it. But dimap requires a pair of functions, so this profunctor-polymorphic function must be hiding such a pair:

s -> a
b -> t

Indeed, given such a pair, we can reconstruct it’s implementation:

mkIso :: (s -> a) -> (b -> t) -> Iso s t a b
mkIso g h = \p -> dimap g h p

All other optics have their corresponding implementation as profunctor-polymorphic functions. The main advantage of these representations is that they can be composed using simple function composition.

Main Takeaways

Producers and consumers correspond to covariant and contravariant functors
Existential types are dual to polymorphic types
Existential optics combine producers with consumers in one package
In such optics, producers decompose, and consumers recompose data
Functions can be polymorphic with respect to types, functors, or profunctors

December 28, 2021

Co-Presheaf Optics

Posted by Bartosz Milewski under Category Theory, Lens, Programming
Leave a Comment

A PDF version of this post is available on github.

Abstract

Co-presheaf optic is a new kind of optic that generalizes the polynomial lens. Its distinguishing feature is that it’s not based on the action of a monoidal category. Instead the action is parameterized by functors between different co-presheaves. The composition of these actions corresponds to composition of functors rather than the more traditional tensor product. These functors and their composition have a representation in terms of profunctors.

Motivation

A lot of optics can be defined using the existential, or coend, representation:

$\mathcal{O}\langle a, b\rangle \langle s, t \rangle = \int^{m \colon \mathcal M} \mathcal C (s, m \bullet a) \times \mathcal D ( m \bullet b, t)$

Here $\mathcal M$ is a monoidal category with an action on objects of two categories $\mathcal C$ and $\mathcal D$ (I’ll use the same notation for both actions). The actions are composed using the tensor product in $\mathcal M$ :

$n \bullet (m \bullet a) = (n \otimes m) \bullet a$

The idea of this optic is that we have a pair of morphisms, one decomposing the source $s$ into the action of some $m$ on $a$ , and the other recomposing the target $t$ from the action of the same $m$ on $b$ . In most applications we pick $\mathcal D$ to be the same category as $\mathcal C$ .

Recently, there has been renewed interest in polynomial functors. Morphisms between polynomial functors form a new kind of optic that doesn’t neatly fit this mold. They do, however, admit an existential representation or the form:

$\int^{c_{k i}} \prod_{k \in K} \mathbf{Set} \left(s_k, \sum_{n \in N} a_n \times c_{n k} \right) \times \prod_{i \in K} \mathbf{Set} \left(\sum_{m \in N} b_m \times c_{m i}, t_i \right)$

Here the sets $s_k$ and $t_i$ can be treated as fibers over the set $K$ , while the sets $a_n$ and $b_m$ are fibers over a different set $N$ .

Alternatively, we can treat these fibrations as functors from discrete categories to $\mathbf{Set}$ , that is co-presheaves. For instance $a_n$ is the result of a co-presheaf $a$ acting on an object $n$ of a discrete category $\mathcal N$ . The products over $K$ can be interpreted as ends that define natural transformations between co-presheaves. The interesting part is that the matrices $c_{n k}$ are fibrated over two different sets. I have previously interpreted them as profunctors:

$c \colon \mathcal N^{op} \times \mathcal K \to \mathbf{Set}$

In this post I will elaborate on this interpretation.

Co-presheaves

A co-presheaf category $[\mathcal C, Set ]$ behaves, in many respects, like a vector space. For instance, it has a “basis” consisting of representable functors $\mathcal C (r, -)$ ; in the sense that any co-presheaf is as a colimit of representables. Moreover, colimit-preserving functors between co-presheaf categories are very similar to linear transformations between vector spaces. Of particular interest are functors that are left adjoint to some other functors, since left adjoints preserve colimits.

The polynomial lens formula has a form suggestive of vector-space interpretation. We have one vector space with vectors $\vec{s}$ and $\vec{t}$ and another with $\vec{a}$ and $\vec{b}$ . Rectangular matrices $c_{n k}$ can be seen as components of a linear transformation between these two vector spaces. We can, for instance, write:

$\sum_{n \in N} a_n \times c_{n k} = c^T a$

where $c^T$ is the transposed matrix. Transposition here serves as an analog of adjunction.

We can now re-cast the polynomial lens formula in terms of co-presheaves. We no longer intepret $\mathcal N$ and $\mathcal K$ as discrete categories. We have:

$a, b \colon [\mathcal N, \mathbf{Set}]$

$s, t \colon [\mathcal K, \mathbf{Set}]$

In this interpretation $c$ is a functor between categories of co-presheaves:

$c \colon [\mathcal N, \mathbf{Set}] \to [\mathcal K, \mathbf{Set}]$

We’ll write the action of this functor on a presheaf $a$ as $c \bullet a$ .

We assume that this functor has a right adjoint and therefore preserves colimits.

$[\mathcal K, \mathbf{Set}] (c \bullet a, t) \cong [\mathcal N, \mathbf{Set}] (a, c^{\dagger} \bullet t)$

where:

$c^{\dagger} \colon [\mathcal K, \mathbf{Set}] \to [\mathcal N, \mathbf{Set}]$

We can now generalize the polynomial optic formula to:

$\mathcal{O}\langle a, b\rangle \langle s, t \rangle = \int^{c} [\mathcal K, \mathbf{Set}] \left(s, c \bullet a \right) \times [\mathcal K, \mathbf{Set}] \left(c \bullet b, t \right)$

The coend is taken over all functors that have a right adjoint. Fortunately there is a better representation for such functors. It turns out that colimit preserving functors:

$c \colon [\mathcal N, \mathbf{Set}] \to [\mathcal K, \mathbf{Set}]$

are equivalent to profunctors (see the Appendix for the proof). Such a profunctor:

$p \colon \mathcal N^{op} \times \mathcal K \to \mathbf{Set}$

is given by the formula:

$p \langle n, k \rangle = c ( \mathcal N(n, -)) k$

where $\mathcal N(n, -)$ is a representable co-presheaf.

The action of $c$ can be expressed as a coend:

$(c \bullet a) k = \int^{n} a(n) \times p \langle n, k \rangle$

The co-presheaf optic is then a coend over all profunctors $p \colon \mathcal N^{op} \times \mathcal K \to \mathbf{Set}$ :

$\int^{p} [\mathcal K, \mathbf{Set}] \left(s, \int^{n} a(n) \times p \langle n, - \rangle \right) \times [\mathcal K, \mathbf{Set}] \left(\int^{n'} b(n') \times p \langle n', - \rangle, t \right)$

Composition

We have defined the action $c \bullet a$ as the action of a functor on a co-presheaf. Given two composable functors:

$c \colon [\mathcal N, \mathbf{Set}] \to [\mathcal K, \mathbf{Set}]$

and:

$c' \colon [\mathcal K, \mathbf{Set}] \to [\mathcal M, \mathbf{Set}]$

we automatically get the associativity law:

$c' \bullet (c \bullet a) = (c' \circ c) a$

The composition of functors between co-presheaves translates directly to profunctor composition. Indeed, the profunctor $p' \diamond p$ corresponding to $c' \circ c$ is given by:

$(p' \diamond p) \langle n, m \rangle = (c' \circ c) ( \mathcal N(n, -)) m$

and can be evaluated to:

$(c' ( c ( \mathcal N(n, -))) m \cong \int^{k} c ( \mathcal N(n, -)) k \times p' \langle k, m \rangle$

$\cong \int^{k} p \langle n, k \rangle \times p' \langle k, m \rangle$

which is the standard definition of profunctor composition.

Consider two composable co-presheaf optics, $\mathcal{O}\langle a, b\rangle \langle s, t \rangle$ and $\mathcal{O}\langle a', b' \rangle \langle a, b \rangle$ . The first one tells us that there exists a $c$ and a pair of natural transformations:

$l_c (s, a ) = [\mathcal K, \mathbf{Set}] \left(s, c \bullet a \right)$

$r_c (b, t) = [\mathcal K, \mathbf{Set}] \left(c \bullet b, t \right)$

The second tells us that there exists a $c'$ and a pair:

$l'_{c'} (a, a' ) = [\mathcal K, \mathbf{Set}] \left(a, c' \bullet a' \right)$

$r'_{c'} (b', b) = [\mathcal K, \mathbf{Set}] \left(c' \bullet b', b \right)$

The composition of the two should be an optic of the type $\mathcal{O}\langle a', b'\rangle \langle s, t \rangle$ . Indeed, we can construct such an optic using the composition $c' \circ c$ and a pair of natural transformations:

$s \xrightarrow{l_c (s, a )} c \bullet a \xrightarrow{c \,\circ \, l'_{c'} (a, a')} c \bullet (c' \bullet a') \xrightarrow{assoc} (c \circ c') \bullet a'$

$(c \circ c') \bullet b' \xrightarrow{assoc^{-1}} c \bullet (c' \bullet b') \xrightarrow{c \, \circ \, r'_{c'} (b', b)} c \bullet b \xrightarrow{r_c (b, t)} t$

Generalizations

By duality, there is a corresponding optic based on presheaves. Also, (co-) presheaves can be naturally generalized to enriched categories, where the correspondence between left adjoint functors and enriched profunctors holds as well.

Appendix

I will show that a functor between two co-presheaves that has a right adjoint and therefore preserves colimits:

$c \colon [\mathcal N, \mathbf{Set}] \to [\mathcal K, \mathbf{Set}]$

is equivalent to a profunctor:

$p \colon \mathcal N^{op} \times \mathcal K \to \mathbf{Set}$

The profunctor is given by:

$p \langle n, k \rangle = c ( \mathcal N(n, -)) k$

and the functor $c$ can be recovered using the formula:

$c (a) k = \int^{n'} a (n') \times p \langle n', k \rangle$

where:

$a \colon [\mathcal N, \mathbf{Set}]$

I’ll show that these formulas are the inverse of each other. First, inserting the formula for $c$ into the definition of $p$ should gives us $p$ back:

$\int^{n'} \mathcal N(n, -) (n') \times p\langle n', k \rangle \cong p \langle n, k \rangle$

which follows from the co-Yoneda lemma.

Second, inserting the formula for $p$ into the definition of $c$ should give us $c$ back:

$\int^{n'} a n' \times c(\mathcal N(n', -)) k \cong c (a) k$

Since $c$ preserves all colimits, and any co-presheaf is a colimit of representables, it’s enough that we prove this identity for a representable:

$a (n) = \mathcal N (r, n)$

We have to show that:

$\int^{n'} \mathcal N (r, n') \times c(\mathcal N(n', -)) k \cong c ( \mathcal N (r, -) ) k$

and this follows from the co-Yoneda lemma.

December 10, 2021

Profunctor Representation of a Polynomial Lens

Posted by Bartosz Milewski under Category Theory, Lens, Programming
Leave a Comment

A PDF of this post is available on github.

Motivation

In this post I’ll be looking at a subcategory of $\mathbf{Poly}$ that consists of polynomial functors in which the fibration is done over one fixed set $N$ :

$P(y) = \sum_{n \in N} s_n \times \mathbf{Set}(t_n, y)$

The reason for this restriction is that morphisms between such functors, which are called polynomial lenses, can be understood in terms of monoidal actions. Optics that have this property automatically have profunctor representation. Profunctor representation has the advantage that it lets us compose optics using regular function composition.

Previously I’ve explored the representations of polynomial lenses as optics in terms on functors and profunctors on discrete categories. With just a few modifications, we can make these categories non-discrete. The trick is to replace sums with coends and products with ends; and, when appropriate, interpret ends as natural transformations.

Monoidal Action

Here’s the existential representation of a lens between polynomials in which all fibrations are over the same set $N$ :

$\mathbf{Pl}\langle s, t\rangle \langle a, b\rangle \cong$

$\int^{c_{k i}} \prod_{k \in N} \mathbf{Set} \left(s_k, \sum_{n \in N} a_n \times c_{n k} \right) \times \prod_{i \in N} \mathbf{Set} \left(\sum_{m \in N} b_m \times c_{m i}, t_i \right)$

This makes the matrices $c_{n k}$ “square.” Such matrices can be multiplied using a version of matrix multiplication.

Interestingly, this idea generalizes naturally to a setting in which $N$ is replaced by a non-discrete category $\mathcal{N}$ . In this setting, we’ll write the residues $c_{m n}$ as profunctors:

$c \langle m, n \rangle \colon \mathcal{N}^{op} \times \mathcal{N} \to \mathbf{Set}$

They are objects in the monoidal category in which the tensor product is given by profunctor composition:

$(c \diamond c') \langle m, n \rangle = \int^{k \colon \mathcal{N}} c \langle m, k \rangle \times c' \langle k, n \rangle$

and the unit is the hom-functor $\mathcal{N}(m, n)$ . (Incidentally, a monoid in this category is called a promonad.)

In the case of $\mathcal{N}$ a discrete category, these definitions decay to standard matrix multiplication:

$\sum_k c_{m k} \times c'_{k n}$

and the Kronecker delta $\delta_{m n}$ .

We define the monoidal action of the profunctor $c$ acting on a co-presheaf $a$ as:

$(c \bullet a) (m) = \int^{n \colon \mathcal{N}} a(n) \times c \langle n, m \rangle$

This is reminiscent of a vector being multiplied by a matrix. Such an action of a monoidal category equips the co-presheaf category with the structure of an actegory.

A product of hom-sets in the definition of the existential optic turns into a set of natural transformations in the functor category $[\mathcal{N}, \mathbf{Set}]$ .

$\mathbf{Pl}\langle s, t\rangle \langle a, b\rangle \cong \int^{c \colon [\mathcal{N}^{op} \times \mathcal{N}, Set]} [\mathcal{N}, \mathbf{Set}] \left(s, c \bullet a\right) \times [\mathcal{N}, \mathbf{Set}] \left(c \bullet b, t\right)$

Or, using the end notation for natural transformations:

$\int^{c} \left( \int_m \mathbf{Set}\left(s(m), (c \bullet a)(m)\right) \times \int_n \mathbf{Set} \left((c \bullet b)(n), t(n)\right) \right)$

As before, we can eliminate the coend if we can isolate $c$ in the second hom-set using a series of isomorphisms:

$\int_n \mathbf{Set} \left(\int^k b(k) \times c\langle k, n \rangle , t(n) \right)$

$\cong \int_n \int_k \mathbf{Set}\left( b(k) \times c\langle k, n \rangle , t (n)\right)$

$\cong \int_{n, k} \mathbf{Set}\left(c\langle k, n \rangle , [b(k), t (n)]\right)$

I used the fact that a mapping out of a coend is an end. The result, after applying the Yoneda lemma to eliminate the end over $k$ , is:

$\mathbf{Pl}\langle s, t\rangle \langle a, b\rangle \cong \int_m \mathbf{Set}\left(s(m), \int^j a(j) \times [b(j), t(m)] \right)$

or, with some abuse of notation:

$[\mathcal{N}, \mathbf{Set}] ( s, [b, t] \bullet a)$

When $\mathcal{N}$ is discrete, this formula decays to the one for polynomial lens.

Profunctor Representation

Since this poly-lens is a special case of a general optic, it automatically has a profunctor representation. The trick is to define a generalized Tambara module, that is a category $\mathcal{T}$ of profunctors of the type:

$P \colon [\mathcal{N}, \mathbf{Set}]^{op} \times [\mathcal{N}, \mathbf{Set}] \to \mathbf{Set}$

with additional structure given by the following family of transformations, in components:

$\alpha_{c, s, t} \colon P\langle s, t \rangle \to P \left \langle c \bullet s, c \bullet t \right \rangle$

The profunctor representation of the polynomial lens is then given by an end over all profunctors in this Tambara category:

$\mathbf{Pl}\langle s, t\rangle \langle a, b\rangle \cong \int_{P \colon \mathcal{T}} \mathbf{Set}\left ( (U P)\langle a, b \rangle, (U P) \langle s, t \rangle \right)$

Where $U$ is the obvious forgetful functor from $\mathcal{T}$ to the underlying profunctor category$.

December 9, 2021

Polynomial Lens in Idris

Posted by Bartosz Milewski under Category Theory, Idris, Lens, Programming
[2] Comments

Lenses and, more general, optics are an example of hard-core category theory that has immediate application in programming. While working on polynomial lenses, I had a vague idea how they could be implemented in a programming language. I thought up an example of a polynomial lens that would focus on all the leaves of a tree at once. It could retrieve or modify them in a single operation. There already is a Haskell optic called traversal that could do it. It can safely retrieve a list of leaves from a tree. But there is a slight problem when it comes to replacing them: the size of the input list has to match the number of leaves in the tree. If it doesn’t, the traversal doesn’t work.

A polynomial lens adds an additional layer of safety by keeping track of the sizes of both the trees and the lists. The problem is that its implementation requires dependent types. Haskell has some support for dependent types, so I tried to work with it, but I quickly got bogged down. So I decided to bite the bullet and quickly learn Idris. This was actually easier than I expected and this post is the result.

Counted Vectors and Trees

I started with the “Hello World!” of dependent types: counted vectors. Notice that, in Idris, type signatures use a single colon rather than the Haskell’s double colon. You can quickly get used to it after the compiler slaps you a few times.

data Vect : Type -> Nat -> Type where
  VNil : Vect a Z
  VCons : (x: a) -> (xs : Vect a n) -> Vect a (S n)

If you know Haskell GADTs, you can easily read this definition. In Haskell, we usually think of Nat as a “kind”, but in Idris types and values live in the same space. Nat is just an implementation of Peano artithmetics, with Z standing for zero, and (S n) for the successor of n. Here, VNil is the constructor of an empty vector of size Z, and VCons prepends a value of type a to the tail of size n resulting in a new vector of size (S n). Notice that Idris is much more explicit about types than Haskell.

The power of dependent types is in very strict type checking of both the implementation and of usage of functions. For instance, when mapping a function over a vector, we can make sure that the result is the same size as the argument:

mapV : (a -> b) -> Vect a n -> Vect b n
mapV f VNil = VNil
mapV f (VCons a v) = VCons (f a) (mapV f v)

When concatenating two vectors, the length of the result must be the sum of the two lengths, (plus m n):

concatV : Vect a m -> Vect a n -> Vect a (plus m n)
concatV VNil v = v
concatV (VCons a w) v = VCons a (concatV w v)

Similarly, when splitting a vector in two, the lengths must match, too:

splitV : (n : Nat) -> Vect a (plus n m) -> (Vect a n, Vect a m)
splitV Z v = (VNil, v)
splitV (S k) (VCons a v') = let (v1, v2) = splitV k v'
                            in (VCons a v1, v2)

Here’s a more complex piece of code that implements insertion sort:

sortV : Ord a => Vect a n -> Vect a n
sortV VNil = VNil
sortV (VCons x xs) = let xsrt = sortV xs 
                     in (ins x xsrt)
  where
    ins : Ord a => (x : a) -> (xsrt : Vect a n) -> Vect a (S n)
    ins x VNil = VCons x VNil
    ins x (VCons y xs) = if x < y then VCons x (VCons y xs)
                                  else VCons y (ins x xs)

In preparation for the polynomial lens example, let’s implement a node-counted binary tree. Notice that we are counting nodes, not leaves. That’s why the node count for Node is the sum of the node counts of the children plus one:

data Tree : Type -> Nat -> Type where
  Empty : Tree a Z
  Leaf  : a -> Tree a (S Z)
  Node  : Tree a n -> Tree a m -> Tree a (S (plus m  n))

All this is not much different from what you’d see in a Haskell library.

Existential Types

So far we’ve been dealing with function that return vectors whose lengths can be easily calculated from the inputs and verified at compile time. This is not always possible, though. In particular, we are interested in retrieving a vector of leaves from a tree that’s parameterized by the number of nodes. We don’t know up front how many leaves a given tree might have. Enter existential types.

An existential type hides part of its implementation. An existential vector, for instance, hides its size. The receiver of an existential vector knows that the size “exists”, but its value is inaccessible. You might wonder then: What can be done with such a mystery vector? The only way for the client to deal with it is to provide a function that is insensitive to the size of the hidden vector. A function that is polymorphic in the size of its argument. Our sortV is an example of such a function.

Here’s the definition of an existential vector:

data SomeVect : Type -> Type where
  HideV : {n : Nat} -> Vect a n -> SomeVect a

SomeVect is a type constructor that depends on the type a—the payload of the vector. The data constructor HideV takes two arguments, but the first one is surrounded by a pair of braces. This is called an implicit argument. The compiler will figure out its value from the type of the second argument, which is Vect a n. Here’s how you construct an existential:

secretV : SomeVect Int
secretV = HideV (VCons 42 VNil)

In this case, the compiler will deduce n to be equal to one, but the recipient of secretV will have no way of figuring this out.

Since we’ll be using types parameterized by Nat a lot, let’s define a type synonym:

Nt : Type
Nt = Nat -> Type

Both Vect a and Tree a are examples of this type.

We can also define a generic existential for stashing such types:

data Some : Nt -> Type where
  Hide : {n : Nat} -> nt n -> Some nt

and some handy type synonyms:

SomeVect : Type -> Type
SomeVect a = Some (Vect a)

SomeTree : Type -> Type
SomeTree a = Some (Tree a)

Polynomial Lens

We want to translate the following categorical definition of a polynomial lens:

$\mathbf{PolyLens}\langle s, t\rangle \langle a, b\rangle = \prod_{k} \mathbf{Set}\left(s_k, \sum_{n} a_n \times [b_n, t_k] \right)$

We’ll do it step by step. First of all, we’ll assume, for simplicity, that the indices $k$ and $n$ are natural numbers. Therefore the four arguments to PolyLens are types parameterized by Nat, for which we have a type alias:

PolyLens : Nt -> Nt -> Nt -> Nt -> Type

The definition starts with a big product over all $k$ ‘s. Such a product corresponds, in programming, to a polymorphic function. In Haskell we would write it as forall k. In Idris, we’ll accomplish the same using an implicit argument {k : Nat}.

The hom-set notation $\mathbf{Set}(a, b)$ stands for a set of functions from $a$ to $b$ , or the type a -> b. So does the notation $[a, b]$ (the internal hom is the same as the external hom in $\mathbf{Set}$ ). The product $a \times b$ is the type of pairs (a, b).

The only tricky part is the sum over $n$ . A sum corresponds exactly to an existential type. Our SomeVect, for instance, can be considered a sum over n of all vector types Vect a n.

Here’s the intuition: Consider that to construct a sum type like Either a b it’s enough to provide a value of either type a or type b. Once the Either is constructed, the information about which one was used is lost. If you want to use an Either, you have to provide two functions, one for each of the two branches of the case statement. Similarly, to construct SomeVect its enough to provide a vector of some particular lenght n. Instead of having two possibilities of Either, we have infinitely many possibilities corresponding to different n‘s. The information about what n was used is then promptly lost.

The sum in the definition of the polynomial lens:

$\sum_{n} a_n \times [b_n, t_k]$

can be encoded in this existential type:

data SomePair : Nt -> Nt -> Nt -> Type where
  HidePair : {n : Nat} -> 
             (k : Nat) -> a n -> (b n -> t k) -> SomePair a b t

Notice that we are hiding n, but not k.

Taking it all together, we end up with the following type definition:

PolyLens : Nt -> Nt -> Nt -> Nt -> Type
PolyLens s t a b = {k : Nat} -> s k -> SomePair a b t

The way we read this definition is that PolyLens is a function polymorphic in k. Given a value of the type s k it produces and existential pair SomePair a b t. This pair contains a value of the type a n and a function b n -> t k. The important part is that the value of n is hidden from the caller inside the existential type.

Using the Lens

Because of the existential type, it’s not immediately obvious how one can use the polynomial lens. For instance, we would like to be able to extract the foci a n, but we don’t know what the value of n is. The trick is to hide n inside an existential Some. Here is the “getter” for this lens:

getLens :  PolyLens sn tn an bn -> sn n -> Some an
getLens lens t =
  let  HidePair k v _ = lens t
  in Hide v

We call lens with the argument t, pattern match on the constructor HidePair and immediately hide the contents back using the constructor Hide. The compiler is smart enough to know that the existential value of n hasn’t been leaked.

The second component of SomePair, the “setter”, is trickier to use because, without knowing the value of n, we don’t know what argument to pass to it. The trick is to take advantage of the match between the producer and the consumer that are the two components of the existential pair. Without disclosing the value of n we can take the a‘s and use a polymorphic function to transform them into b‘s.

transLens : PolyLens sn tn an bn -> ({n : Nat} -> an n -> bn n)
        -> sn n -> Some tn
transLens lens f t =
  let  HidePair k v vt = lens t
  in  Hide (vt (f v))

The polymorphic function here is encoded as ({n : Nat} -> an n -> bn n). (An example of such a function is sortV.) Again, the value of n that’s hidden inside SomePair is never leaked.

Example

Let’s get back to our example: a polynomial lens that focuses on the leaves of a tree. The type signature of such a lens is:

treeLens : PolyLens (Tree a) (Tree b) (Vect a) (Vect b)

Using this lens we should be able to retrieve a vector of leaves Vect a n from a node-counted tree Tree a k and replace it with a new vector Vect b n to get a tree Tree b k. We should be able to do it without ever disclosing the number of leaves n.

To implement this lens, we have to write a function that takes a tree of a and produces a pair consisting of a vector of a‘s and a function that takes a vector of b‘s and produces a tree of b‘s. The type b is fixed in the signature of the lens. In fact we can pass this type to the function we are implementing. This is how it’s done:

treeLens : PolyLens (Tree a) (Tree b) (Vect a) (Vect b)
treeLens {b} t = replace b t

First, we bring b into the scope of the implementation as an implicit parameter {b}. Then we pass it as a regular type argument to replace. This is the signature of replace:

replace : (b : Type) -> Tree a n -> SomePair (Vect a) (Vect b) (Tree b)

We’ll implement it by pattern-matching on the tree.

The first case is easy:

replace b Empty = HidePair 0 VNil (\v => Empty)

For an empty tree, we return an empty vector and a function that takes and empty vector and recreates and empty tree.

The leaf case is also pretty straightforward, because we know that a leaf contains just one value:

replace b (Leaf x) = HidePair 1 (VCons x VNil) 
                                (\(VCons y VNil) => Leaf y)

The node case is more tricky, because we have to recurse into the subtrees and then combine the results.

replace b (Node t1 t2) =
  let (HidePair k1 v1 f1) = replace b t1
      (HidePair k2 v2 f2) = replace b t2
      v3 = concatV v1 v2
      f3 = compose f1 f2
  in HidePair (S (plus k2 k1)) v3 f3

Combining the two vectors is easy: we just concatenate them. Combining the two functions requires some thinking. First, let’s write the type signature of compose:

compose : (Vect b n -> Tree b k) -> (Vect b m -> Tree b j) ->
       (Vect b (plus n m)) -> Tree b (S (plus j k))

The input is a pair of functions that turn vectors into trees. The result is a function that takes a larger vector whose size is the sume of the two sizes, and produces a tree that combines the two subtrees. Since it adds a new node, its node count is the sum of the node counts plus one.

Once we know the signature, the implementation is straightforward: we have to split the larger vector and pass the two subvectors to the two functions:

compose {n} f1 f2 v =
  let (v1, v2) = splitV n v
  in Node (f1 v1) (f2 v2)

The split is done by looking at the type of the first argument (Vect b n -> Tree b k). We know that we have to split at n, so we bring {n} into the scope of the implementation as an implicit parameter.

Besides the type-changing lens (that changes a to b), we can also implement a simple lens:

treeSimpleLens : PolyLens (Tree a) (Tree a) (Vect a) (Vect a)
treeSimpleLens {a} t = replace a t

We’ll need it later for testing.

Testing

To give it a try, let’s create a small tree with five nodes and three leaves:

t3 : Tree Char 5
t3 = (Node (Leaf 'z') (Node (Leaf 'a') (Leaf 'b')))

We can extract the leaves using our lens:

getLeaves : Tree a n -> SomeVect a
getLeaves t = getLens treeSimpleLens t

As expected, we get a vector containing 'z', 'a', and 'b'.

We can also transform the leaves using our lens and the polymorphic sort function:

trLeaves : ({n : Nat} -> Vect a n -> Vect b n) -> Tree a n -> SomeTree b
trLeaves f t = transLens treeLens f t

trLeaves sortV

The result is a new tree: ('a',('b','z'))

Complete code is available on github.

September 4, 2021

Dependent Optics

Posted by Bartosz Milewski under Category Theory, Functional Programming, Lens, Programming
Leave a Comment

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 $E$ , the base space $B$ , and a projection, or a display map, $p \colon E \to B$ . The fibers of $p$ correspond to members of the type family. For instance, the total space, or the bundle, of counted vectors is the list type $\mathit{List} (A)$ (a free monoid generated by $A$ ) with the projection $\mathit{len} \colon \mathit{List} (A) \to \mathbb{N}$ that returns the length of a list.

Another way of looking at dependent types is as objects in the slice category $\mathcal{C}/B$ . Counted vectors, for instance, are represented as objects in $\mathcal{C}/\mathbb{N}$ given by pairs $\langle \mathit{List} (A), \mathit{len} \rangle$ . Morphisms in the slice category correspond to fibre-wise mappings between bundles.

We often require that $\mathcal{C}$ be a locally cartesian closed category, that is a category whose slice categories are cartesian closed. In such categories, the base-change functor $f^*$ has both the left adjoint, the dependent sum $\Sigma_f$ ; and the right adjoint, the dependent product $\Pi_f$ . The base-change functor is defined as a pullback:

basechange

This pullback defines a cartesian product in the slice category $\mathcal{C}/B$ between two objects: $\langle B', f \rangle$ and $\langle E, p \rangle$ . In a locally cartesian closed category, this product has the right adjoint, the internal hom in $\mathcal{C}/B$ .

Dependent optics

The most general optic is given by two monoidal actions $L_m$ and $R_m$ in two categories $\mathcal{C}$ and $\mathcal{D}$ . It can be written as the following coend of the product of two hom-sets:

$O(A, A'; S, S') = \int^{m \colon \mathcal{M}} \mathcal{C}( S, L_m A) \times \mathcal{D}(R_m A', S')$

Monoidal actions are parameterized by objects in a monoidal category $(\mathcal{M}, \otimes, 1)$ .

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 $\langle E, p \rangle$ over $B$ must commute with the projection:

$p \circ L_m = p$

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

$L_{m \otimes n} \cong L_m \circ L_n$

$L_1 \cong \mathit{Id}$

We can define a dependent (mixed) optic as:

$\int^{m : \mathcal{M}} (\mathcal{C}/B)( S, L_m A) \times (\mathcal{D}/B')(R_m A', S')$

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

$\alpha_{m, \langle A, A' \rangle} \colon P \langle A, A' \rangle \to P\langle L_m A, R_m A' \rangle$

where $A$ and $A'$ are objects in the appropriate slice categories.
The optic is then given by the following end in the Tambara category:

$O(A, A'; S, S') = \int_{p : \mathbf{Tam}} \mathbf{Set}(P \langle A, A' \rangle, P \langle S, S' \rangle)$

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 $\langle C, q \rangle$ on another object $\langle A, p \rangle$ is given by the pullback:

$M_C A = C \times_B A$

Since a pullback is the product in the slice category $\mathcal{C}/B$ , it is automatically associative and unital, so it can be used to define a dependent lens:

$\mathit{DLens}(A, A'; S, S') = \int^{\langle C, p \rangle : \mathcal{C}/B} (\mathcal{C}/B)( S, C \times_B A) \times (\mathcal{C}/B)(C \times_B A', S')$

Since $\mathcal{C}$ is locally cartesian closed, there is an adjunction between the product and the exponential. We can use it to get:

$\cong \int^{\langle C, p \rangle : \mathcal{C}/B} (\mathcal{C}/B)( S, C \times_B A) \times (\mathcal{C}/B)(C , [A', S']_B)$

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

$(\mathcal{C}/B)( S, [A', S']_B \times_B A)$

The internal hom $[A', S']_B$ in a locally cartesian closed category can be expressed using a dependent product:

$\left [\left \langle A' \atop p \right \rangle, \left \langle S' \atop q \right \rangle \right ] \cong \Pi_p \left(p^* \left \langle S' \atop q \right \rangle \right)$

where $p \colon A' \to B$ is the fibration of $A'$ , $\Pi_p$ is the right adjoint to the base change functor, and $p^*$ is the base-change functor along $p$ .

The dependent lens can be written as:

$(\mathcal{C} / B) \left( \left \langle S \atop r \right \rangle, \Pi_p \left(p^* \left \langle S' \atop q \right \rangle \right) \times \left \langle A \atop r' \right \rangle \right)$

In particular, if $B$ is $\mathbb{N}$ , this is equal to an infinite tuple of functions:

$O(A, B; S, T) \cong \prod_n \left( s_n \to \left((b_n \to t_n) \times a_n \right) \right)$

or fiber-wise pairs of setter/getter $\langle s_n \to b_n \to t_n, s_n \to a_n \rangle$ indexed by $n$ .

Traversals

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

$M_{c} a = \sum_{n \colon \mathbb{N}} c_n \times a^n$

The coefficients $c_n$ can be expressed as a fibration $\langle C, p \colon C \to \mathbb{N} \rangle$ , with $C = \sum_n c_n$ , the sum of the fibers. The set of powers of $a$ can be similarly written as $\langle L(a), \mathit{len} \rangle$ , with $L(a)$ the type of list of $a$ (a free monoid generated by $a$ ), and $\mathit{len}$ the function that assigns the length to a list. The monoidal action can then be written using a product (pullback) in the slice category $\mathbf{Set}/\mathbb{N}$ :

$\left \langle {C \atop p} \right \rangle \times \left \langle {L(a) \atop \mathit{len}} \right \rangle$

There is an obvious forgetful functor $U \colon \mathbf{Set}/\mathbb{N} \to \mathbf{Set}$ , which can be used to express the polynomial action:

$M_c a = U\left( \left \langle {C \atop p} \right \rangle \times \left \langle {L(a) \atop \mathit{len}} \right \rangle \right)$

The traversal is the optic:

$\int^{\langle C, p \rangle : \mathbf{Set}/\mathbb{N}} \mathbf{Set} \left(s, M_c a \right) \times \mathbf{Set}(M_c b, t)$

Eqivalently, the second factor can be rewritten as:

$\mathbf{Set}\left( \sum_{n \colon \mathbb{N}} c_n \times b^n, t\right) \cong \prod_{n \colon \mathbb{N}} \mathbf{Set}(c_n \times b^n, t)$

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

$\cong (\mathbf{Set}/\mathbb{N})\left(\left \langle {C \atop p} \right \rangle \times \left \langle {L(b) \atop \mathit{len}} \right \rangle, \left \langle {\mathbb{N} \times t \atop \pi_1} \right \rangle \right)$

where $\pi_1$ is the projection from the cartesian product.

The traversal is therefore a mixed optic:

$\int^{\langle C, p \rangle : \mathbf{Set}/\mathbb{N}} \mathbf{Set} \left(s, M_c a \right) \times (\mathbf{Set}/\mathbb{N})\left( \left \langle {C \atop p} \right \rangle \times \left \langle {L(b) \atop \mathit{len}} \right \rangle, \left \langle {\mathbb{N} \times t \atop \pi_1} \right \rangle \right)$

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

$(\mathbf{Set}/\mathbb{N})\left(\left \langle {C \atop p} \right \rangle, \left[ \left \langle {L(b) \atop \mathit{len}} \right \rangle, \left \langle {\mathbb{N} \times t \atop \pi_1} \right \rangle \right] \right)$

We can then use the ninja Yoneda lemma on the optic to “integrate” over $\langle C, p \rangle$ and get:

$O(a, b; s, t) \cong \mathbf{Set} \left( s, U\left( \left[ \left \langle {L(b) \atop \mathit{len}} \right \rangle, \left \langle {\mathbb{N} \times t \atop \pi_1} \right \rangle \right] \times \left \langle {L(a) \atop \mathit{len}} \right \rangle \right) \right)$

which, in components, reads:

$s \to \sum_n \left( (b^n \to t) \times a^n \right)$

April 1, 2021

Traversals 3: Existential and Profunctor representations of Traversals

Posted by Bartosz Milewski under Programming | Tags: Category Theory, Lens, Polynomial Functors, Profunctors, Tambara Modules, Traversal |
Leave a Comment

Previously: Profunctors.

Traversals

A traversal is a kind of optic that can focus on zero or more items at a time. Naively, we would expect to have a getter that returns a list of values, and a setter that replaces a list of values. Think of a tree with $N$ leaves: a traversal would return a list of leaves, and it would allow you to replace them with a new list. The problem is that the size of the list you pass to the setter cannot be arbitrary—it must match the number of leaves in the particular tree. This is why, in Haskell, the setter and the getter are usually combined in a single function:

s -> ([b] -> t, [a])

Still, Haskell is not able to force the sizes of both lists to be equal.

Since a list type can be represented as an infinite sum of tuples, I knew that the categorical version of this formula must involve a power series, or a polynomial functor:

$\mathbf{Set} \big(s, \sum_{n} \mathbf{Set}(b^n, t) \times a^n\big)$

but was unable to come up with an existential form for it.

Pickering, Gibbons, and Wu came up with a representation for traversals using profunctors that were cartesian, cocartesian, and monoidal at the same time, but the monoidal constraint didn’t fit neatly into the Tambara scheme:

class Profunctor p => Monoidal p where
  par   :: p a b -> p c d -> p (a, c) (b, d)
  empty :: p () ()

We’ve been struggling with this problem, when one of my students, Mario Román came up with the ingenious idea to make $n$ existential.

The idea is that a coend in the existential representation of optics acts like a sum (or like an integral—hence the notation). A sum over natural numbers is equivalent to the coend over the category of natural numbers.

At the root of all optics there is a monoidal action. For lenses, this action is given by “scaling”

$a \to a \times c$

For prisms, it’s the “translation”

$a \to a + c$

For grates it’s the exponentiation

$a \to a^c$

The composition of a prism and a lens is an affine transformation

$a \to c_0 + a \times c_1$

A traversal is similarly generated by a polynomial functor, or a power series functor:

$a \to \sum_n c_n \times a^n$

The key observation here is that there is a different object $c_n$ for every power of $a$ , which can only be expressed using dependent types in programming. For every multiplicity of foci, the residue is of a different type.

In category theory, we can express the whole infinite sequence of residues as a functor from the monoidal category $\mathbb{N}$ of natural numbers to $\mathbf{Set}$ . (The sum is really a coend over $\mathbb{N}$ .)

The existential version of a traversal is thus given by:

$\int^{c \colon [\mathbb{N}, \mathbf{Set}]} \mathbf{Set}\big(s, \sum_n c_n \times a^n\big) \times \mathbf{Set}\big( \sum_m c_m \times b^m, t\big)$

We can now use the continuity of the hom-set to replace the mapping out of a sum with a product of mappings:

$\int^{c \colon [\mathbb{N}, \mathbf{Set}]} \mathbf{Set}\big(s, \sum_n c_n \times a^n\big) \times \prod_m \mathbf{Set}\big( c_m \times b^m, t\big)$

and use the currying adjunction

$\int^{c \colon [\mathbb{N}, \mathbf{Set}]} \mathbf{Set}\big(s, \sum_n c_n \times a^n\big) \times \prod_m \mathbf{Set}\big( c_m, \mathbf{Set}( b^m, t)\big)$

The product of hom-sets is really an end over $\mathbb{N}$ , or a set of natural transformations in $[\mathbb{N}, \mathbf{Set}]$

$\int^{c \colon [\mathbb{N}, \mathbf{Set}]} \mathbf{Set}\big(s, \sum_n c_n \times a^n\big) \times [\mathbb{N}, \mathbf{Set}]\big( c_-, \mathbf{Set}( b^-, t)\big)$

and we can apply the Yoneda lemma to “integrate” over $c$ to get:

$\mathbf{Set}(s, \sum_n (\mathbf{Set}(b^n, t) \times a^n)\big)$

which is exactly the formula for traversals.

Once we understood the existential representation of traversals, the profunctor representation followed. The equivalent of Tambara modules for traversals is a category of profunctors equipped with the monoidal action parameterized by objects in $[\mathbb{N}, \mathbf{Set}]$ :

$\alpha_{c, \langle a, b \rangle} \colon p \langle a, b \rangle \to p\langle \sum_n c_n \times a^n, \sum_m c_m \times b^m \rangle$

The double Yoneda trick works for these profunctors as well, proving the equivalence with the existential representation.

Generalizations

As hinted in my blog post and formalized by Mitchell Riley, Tambara modules can be generalized to an arbitrary monoidal action. We have also realized that we can combine actions in two different categories. We could take an arbitrary monoidal category $\mathcal{M}$ , define its action on two categories, $\mathcal{C}$ and $\mathcal{D}$ using strong monoidal functors:

$F \colon \mathcal{M} \to [\mathcal{C}, \mathcal{C}]$

$G \colon \mathcal{M} \to [\mathcal{D}, \mathcal{D}]$

These actions define the most general existential optic:

$\mathbf{Optic} \langle s, t \rangle \langle a, b \rangle = \int^{m \colon \mathcal{M}} \mathcal{C}(s, F_m a) \times \mathcal{D}(G_m b, t)$

Notice that the pairs of arguments are heterogenous—e.g., in $\langle a, b \rangle$ , $a$ is from $\mathcal{C}$ , and $b$ is from $\mathcal{D}$ .

We have also generalized Tambara modules:

$\alpha_{m, \langle a, b \rangle} \colon p \langle a, b \rangle \to p \langle F_m a, G_m b\rangle$

and the Pastro Street derivation of the promonad. That lead us to a more general proof of isomorphism between the profunctor formulation and the existential formulation of optics. Just to be general enough, we did it for enriched categories, replacing $\mathbf{Set}$ with an arbitrary monoidal category.

Finally, we described some new interesting optics like algebraic and monadic lenses.

The Physicist’s Explanation

The traversal result confirmed my initial intuition from general relativity that the most general optics are generated by the analog of diffeomorphisms. These are the smooth coordinate transformations under which Einstein’s theory is covariant.

Physicists have long been using symmetry groups to build theories. Laws of physics are symmetric with respect to translations, time shifts, rotations, etc.; leading to laws of conservation of momentum, energy, angular momentum, etc. There is an uncanny resemblance of these transformations to some of the monoidal actions in optics. The prism is related to translations, the lens to rotations or scaling, etc.

There are many global symmetries in physics, but the real power comes from local symmetries: gauge symmetries and diffeomorphisms. These give rise to the Standard Model and to Einstein’s theory of gravity.

A general monoidal action seen in optics is highly reminiscent of a diffeomorphism, and the symmetry behind a traversal looks like it’s generated by an analytical function.

In my opinion, these similarities are a reflection of a deeper principle of compositionality. There is only a limited set of ways we can decompose complex problems, and sooner or later they all end up in category theory.

The main difference between physics and category theory is that category theory is more interested in one-way mappings, whereas physics deals with invertible transformations. For instance, in category theory, monoids are more fundamental than groups.

Here’s how categorical optics might be seen by a physicist.

In physics we would start with a group of transformations. Its representations would be used, for instance, to classify elementary particles. In optics we start with a monoidal category $\mathcal{M}$ and define its action in the target category $\mathcal{C}$ . (Notice the use of a monoid rather than a group.)

$F \colon \mathcal{M} \to [\mathcal{C}, \mathcal{C}]$

In physics we would represent the group using matrices, here we use endofunctors.

A profunctor is like a path that connects the initial state to the final state. It describes all the ways in which $a$ can evolve into $b$ .

If we use mixed optics, final states come from a different category $\mathcal{D}$ , but their transformations are parameterized by the same monoidal category:

$G \colon \mathcal{M} \to [\mathcal{D}, \mathcal{D}]$

A path may be arbitrarily extended, at both ends, by a pair of morphisms. Given a morphism in $\mathcal{C}$ :

$f \colon a' \to a$

and another one in $\mathcal{D}$

$g \colon b \to b'$

the profunctor uses them to extend the path:

$p \langle a, b \rangle \to p \langle a', b' \rangle$

A (generalized) Tambara module is like the space of paths that can be extended by transforming their endpoints.

$\alpha_{m, \langle a, b \rangle} \colon p \langle a, b \rangle \to p \langle F_m a, G_m b\rangle$

If we have a path that can evolve $a$ into $b$ , then the same path can be used to evolve $F_m a$ into $G_m b$ . In physics, we would say that the paths are “invariant” under the transformation, but in category theory we are fine with a one-way mapping.

The profunctor representation is like a path integral:

$\int_{p \colon \mathbf{Tam}} \mathbf{Set}( p \langle a, b \rangle, p \langle s, t \rangle)$

We fix the end-states but we vary the paths. We integrate over all paths that have the “invariance” or extensibility property that defines the Tambara module.

For every such path, we have a mapping that takes the evolution from $a$ to $b$ and produces the evolution (along the same path) from $s$ to $t$ .

The main theorem of profunctor optics states that if, for a given collection of states, $\langle a, b \rangle, \langle s, t \rangle$ , such a mapping exists, then these states are related. There exists a transformation and a pair of morphisms that are secretly used in the path integral to extend the original path.

$\int^{m \colon \mathcal{M}} \mathcal{C}(s, F_m a) \times \mathcal{D}(G_m b, t)$

Again, the mappings are one-way rather than both ways. They let us get from $s$ to $F_m a$ and from $G_m b$ to $t$ .

This pair of morphisms is enough to extend any path $p \langle a, b \rangle$ to $p \langle s, t \rangle$ by first applying $\alpha_m$ and then lifting the two morphisms. The converse is also true: if every path can be extended then such a pair of morphisms must exist.

What seems unique to optics is the interplay between transformations and decompositions: The way $m$ can be interpreted both as parameterizing a monoidal action and the residue left over after removing the focus.

Conclusion

For all the details and a list of references you can look at our paper “Profunctor optics, a categorical update.” It’s the result of our work at the Adjoint School of Applied Category Theory in Oxford in 2019. It’s avaliable on arXiv.

I’d like to thank Mario Román for reading the draft and providing valuable feedback.

April 1, 2021

Traversals 2: Profunctors and Tambara Modules

Posted by Bartosz Milewski under Programming | Tags: Category Theory, Lens, Optics, Profunctors, Tambara Modules |
[4] Comments

Previously: Existentials.

Double Yoneda

If you squint hard enough, the Yoneda lemma:

$\int_{x} \mathbf{Set}\big(\mathcal{C}(a, x), f x\big) \cong f a$

could be interpreted as the representable functor $\mathcal{C}(a, -)$ acting as the unit with respect to taking the end. It takes an $f$ and returns an $f$ . Let’s keep this in mind.

We are going to need an identity that involves higher-order natural transformations between two higher-order functors. These are actually the functors $R_a$ that we’ve encountered before. They are parameterized by objects in $\mathcal{C}$ , and their action on functors (co-presheaves) is to apply those functors to objects. They are the “give me a functor and I’ll apply it to my favorite object” kind of functors.

We need a natural transformation between two such functors, and we can express it as an end:

$\int_f \mathbf{Set}( R_a f, R_s f) = \int_f \mathbf{Set}( f a, f s)$

Here’s the trick: replace these functors with their Yoneda equivalents:

$\int_f \mathbf{Set}( f a, f s) \cong \int_f \mathbf{Set}\Big(\int_{x} \mathbf{Set}\big(\mathcal{C}(a, x), fx), \int_{y} \mathbf{Set}\big(\mathcal{C}(s, y), f y\big)\Big)$

Notice that this is now a mapping between two hom-sets in the functor category, the first one being:

$\int_{x} \mathbf{Set}\big(\mathcal{C}(a, x), fx\big) = [\mathcal{C}, \mathbf{Set}]\big(\mathcal{C}(a, -), f\big)$

We can now use the corollary of the Yoneda lemma to replace the set of natural transformation between these two hom-functors with the hom-set:

$[\mathcal{C}, \mathbf{Set}]\big(\mathcal{C}(s, -), \mathcal{C}(a, -) \big)$

But this is again a natural transformation between two hom-functors, so it can be further reduced to $\mathcal{C}(a, s)$ . The result is:

$\int_f \mathbf{Set}( f a, f s) \cong \mathcal{C}(a, s)$

We’ve used the Yoneda lemma twice, so this trick is called the double-Yoneda.

Profunctors

It turns out that the prism also has a functor-polymorphic representation, but it uses profunctors in place of regular functors. A profunctor is a functor of two arguments, but its action on arrows has a twist. Here’s the Haskell definition:

class Profunctor p where
  dimap :: (a' -> a) -> (b -> b') -> (p a b -> p a' b')

It lifts a pair of functions, where the first one goes in the opposite direction.

In category theory, the “twist” is encoded by using the opposite category $\mathcal{C}^{op}$ , so a profunctor is defined a functor from $\mathcal{C}^{op} \times \mathcal{C}$ to $\mathbf{Set}$ .

The prime example of a profunctor is the hom-functor which, on objects, assigns the set $\mathcal{C}(a, b)$ to every pair $\langle a, b \rangle$ .

Before we talk about the profunctor representation of prisms and lenses, there is a simple optic called Iso. It’s defined by a pair of functions:

from :: s -> a
to   :: b -> t

The key observation here is that such a pair of arrows is an element of the hom set in the category $\mathcal{C}^{op} \times \mathcal{C}$ between the pair $\langle a, b \rangle$ and the pair $\langle s, t \rangle$ :

$(\mathcal{C}^{op} \times \mathcal{C})( \langle a, b \rangle, \langle s, t \rangle)$

The “twist” of using $\mathcal{C}^{op}$ reverses the direction of the first arrow.

Iso has a simple profunctor representation:

type Iso s t a b = forall p. Profunctor p => p a b -> p s t

This formula can be translated to category theory as an end in the profunctor category:

$\int_p \mathbf{Set}(p \langle a, b \rangle, p \langle s, t \rangle)$

Profunctor category is a category of co-presheaves $[\mathcal{C}^{op} \times \mathcal{C}, \mathbf{Set}]$ . We can immediately apply the double Yoneda identity to it to get:

$\int_p \mathbf{Set}(p \langle a, b \rangle, p \langle s, t \rangle) \cong (\mathcal{C}^{op} \times \mathcal{C})( \langle a, b \rangle, \langle s, t \rangle)$

which shows the equivalence of the two representations.

Tambara Modules

Here’s the profunctor representation of a prism:

type Prism s t a b = forall p. Choice p => p a b -> p s t

It looks almost the same as Iso, except that the quantification goes over a smaller class of profunctors called Choice (or cocartesian). This class is defined as:

class Profunctor p => Choice where
  left'  :: p a b -> p (Either a c) (Either b c)
  right' :: p a b -> p (Either c a) (Either c b)

Lenses can also be defined in a similar way, using the class of profunctors called Strong (or cartesian).

class Profunctor p => Strong where
  first'  :: p a b -> p (a, c) (b, c)
  second' :: p a b -> p (c, a) (c, b)

Profunctor categories with these structures are called Tambara modules. Tambara formulated them in the context of monoidal categories, for a more general tensor product. Sum (Either) and product (,) are just two special cases.

A Tambara module is an object in a profunctor category with additional structure defined by a family of morphisms:

$\alpha_{c, \langle a, b \rangle} \colon p \langle a, b \rangle \to p\langle c \otimes a, c \otimes b \rangle$

with some naturality and coherence conditions.

Lenses and prisms can thus be defined as ends in the appropriate Tambara modules

$\int_{p \colon \mathbf{Tam}} \mathbf{Set}(p \langle a, b \rangle, p \langle s, t \rangle)$

We can now use the double Yoneda trick to get the usual representation.

The problem is, we don’t know in what category the result should be. We know the objects are pairs $\langle a, b \rangle$ , but what are the morphisms between them? It turns out this problem was solved in a paper by Pastro and Street. The category in question is the Kleisli category for a particular promonad. This category is now better known as $\mathbf{Optic}$ . Let me explain.

Double Yoneda with Adjunctions

The double Yoneda trick worked for an unconstrained category of functors. We need to generalize it to a category with some additional structure (for instance, a Tambara module).

Let’s say we start with a functor category $[\mathcal{C}, \mathbf{Set}]$ and endow it with some structure, resulting in another functor category $\mathcal{T}$ . It means that there is a (higher-order) forgetful functor $U \colon \mathcal{T} \to [\mathcal{C}, \mathbf{Set}]$ that forgets this additional structure. We’ll also assume that there is the right adjoint functor $F$ that freely generates the structure.

We will re-start the derivation of double Yoneda using the forgetful functor

$\int_{f \colon \mathcal{T}} \mathbf{Set}( (U f) a, (U f) s)$

Here, $a$ and $s$ are objects in $\mathcal{C}$ and $(U f)$ is a functor in $[\mathcal{C}, \mathbf{Set}]$ .

We perform the Yoneda trick the same way as before to get:

$\int_{f \colon \mathcal{T}} \mathbf{Set}\Big(\int_{x \colon C} \mathbf{Set}\big(\mathcal{C}(a, x),(U f) x), \int_{y \colon C} \mathbf{Set}\big(\mathcal{C}(s, y),(U f) y\big)\Big)$

Again, we have two sets of natural transformations, the first one being:

$\int_{x \colon C} \mathbf{Set}\big(\mathcal{C}(a, x), (U f) x\big) = [\mathcal{C}, \mathbf{Set}]\big(\mathcal{C}(a, -), U f\big)$

The adjunction tells us that

$[\mathcal{C}, \mathbf{Set}]\big(\mathcal{C}(a, -), U f\big) \cong \mathcal{T}\Big(F\big(\mathcal{C}(a, -)\big), f\Big)$

The right-hand side is a hom-set in the functor category $\mathcal{T}$ . Plugging this back into the original formula, we get

$\int_{f \colon \mathcal{T}} \mathbf{Set}\Big(\mathcal{T}\Big(F\big(\mathcal{C}(a, -)\big), f\Big), \mathcal{T}\Big(F\big(\mathcal{C}(s, -)\big), f\Big) \Big)$

This is the set of natural transformations between two hom-functors, so we can use the corollary of the Yoneda lemma to replace it with:

$\mathcal{T}\Big( F\big(\mathcal{C}(s, -)\big), F\big(\mathcal{C}(a, -)\big) \Big)$

We can then use the adjunction again, in the opposite direction, to get:

$[\mathcal{C}, \mathbf{Set}] \Big( \mathcal{C}(s, -), (U \circ F)\big(\mathcal{C}(a, -)\big) \Big)$

or, using the end notation:

$\int_{c \colon C} \mathbf{Set} \Big(\mathcal{C}(s, c), (U \circ F)\big(\mathcal{C}(a, -)\big) c \Big)$

Finally, we use the Yoneda lemma again to get:

$(U \circ F) \big( \mathcal{C}(a, -) \big) s$

This is the action of the higher-order functor $(U \circ F)$ on the hom-functor $\mathcal{C}(a, -)$ , the result of which is applied to $s$ .

The composition of two functors that form an adjunction is a monad $\Phi$ . This is a monad in the functor category $[\mathcal{C}, \mathbf{Set}]$ . Altogether, we get:

$\int_{f \colon \mathcal{T}} \mathbf{Set}( (U f) a, (U f) s) \cong \Phi \big( \mathcal{C}(a, -) \big) s$

Profunctor Representation of Lenses and Prisms

The previous formula can be immediately applied to the category of Tambara modules. The forgetful functor takes a Tambara module and maps it to a regular profunctor $p$ , an object in the functor category $[\mathcal{C}^{op} \times \mathcal{C}, \mathbf{Set}]$ . We replace $a$ and $s$ with pairs of objects. We get:

$\int_{p \colon \mathbf{Tam}} \mathbf{Set}(p \langle a, b \rangle, p \langle s, t \rangle) \cong \Phi \big( (\mathcal{C}^{op} \times \mathcal{C})(\langle a, b \rangle, -) \big) \langle s, t \rangle$

The only missing piece is the higher order monad $\Phi$ —a monad operating on profunctors.

The key observation by Pastro and Street was that Tambara modules are higher-order coalgebras. The mappings:

$\alpha \colon p \langle a, b \rangle \to p\langle c \otimes a, c \otimes b \rangle$

can be thought of as components of a natural transformation

$\int_{\langle a, b \rangle, c} \mathbf{Set} \big( p \langle a, b \rangle, p\langle c \otimes a, c \otimes b \rangle \big)$

By continuity of hom-sets, we can move the end over $c$ to the right:

$\int_{\langle a, b \rangle} \mathbf{Set} \Big( p \langle a, b \rangle, \int_c p\langle c \otimes a, c \otimes b \rangle \Big)$

We can use this to define a higher order functor that acts on profunctors:

$(\Theta p)\langle a, b \rangle = \int_c p\langle c \otimes a, c \otimes b \rangle$

so that the family of Tambara mappings can be written as a set of natural transformations $p \to (\Theta p)$ :

$\int_{\langle a, b \rangle} \mathbf{Set} \big( p \langle a, b \rangle, (\Theta p)\langle a, b \rangle \big)$

Natural transformations are morphisms in the category of profunctors, and such a morphism $p \to (\Theta p)$ is, by definition, a coalgebra for the functor $\Theta$ .

Pastro and Street go on showing that $\Theta$ is more than a functor, it’s a comonad, and the Tambara structure is not just a coalgebra, it’s a comonad coalgebra.

What’s more, there is a monad that is adjoint to this comonad:

$(\Phi p) \langle s, t \rangle = \int^{\langle x, y \rangle, c} (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes x, c \otimes y \rangle, \langle s, t \rangle \big) \times p \langle x, y \rangle$

When a monad is adjoint to a comonad, the comonad coalgebras are isomorphic to monad algebras—in this case, Tambara modules. Indeed, the algebras $(\Phi p) \to p$ are given by natural transformations:

$\int_{\langle s, t \rangle} \mathbf{Set}\Big( (\Phi p) \langle s, t \rangle, p\langle s, t \rangle \Big)$

Substituting the formula for $\Phi$ ,

$\int_{\langle s, t \rangle} \mathbf{Set}\Big( \int^{\langle x, y \rangle, c} (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes x, c \otimes y \rangle, \langle s, t \rangle \big) \times p \langle x, y \rangle, p\langle s, t \rangle \Big)$

by continuity of the hom-set (with the coend in the negative position turning into an end),

$\int_{\langle s, t \rangle} \int_{\langle x, y \rangle, c}\mathbf{Set}\Big( (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes x, c \otimes y \rangle, \langle s, t \rangle \big) \times p \langle x, y \rangle, p\langle s, t \rangle \Big)$

using the currying adjunction,

$\int_{\langle s, t \rangle, \langle x, y \rangle, c}\mathbf{Set}\Big( (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes x, c \otimes y \rangle, \langle s, t \rangle \big), \mathbf{Set}\big( p \langle x, y \rangle, p\langle s, t \rangle \big) \Big)$

and the Yoneda lemma, we get

$\int_{\langle x, y \rangle, c} \mathbf{Set}\big( p \langle x, y \rangle, p\langle c \otimes x, c \otimes y \rangle \big)$

which is the Tambara structure $\alpha$ .

$\Phi$ is exactly the monad that appears on the right-hand side of the double-Yoneda with adjunctions. This is because every monad can be decomposed into a pair of adjoint functors. The decomposition we’re interested in is the one that involves the Kleisli category of free algebras for $\Phi$ . And now we know that these algebras are Tambara modules.

All that remains is to evaluate the action of $\Phi$ on the represesentable functor:

$\Phi \big( (\mathcal{C}^{op} \times \mathcal{C})(\langle a, b \rangle, -) \big) \langle s, t \rangle$

It’s a matter of simple substitution:

$\int^{\langle x, y \rangle, c} (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes x, c \otimes y \rangle, \langle s, t \rangle \big) \times (\mathcal{C}^{op} \times \mathcal{C})(\langle a, b \rangle, \langle x, y \rangle)$

and using the Yoneda lemma to replace $\langle x, y \rangle$ with $\langle a, b \rangle$ . The result is:

$\int^c (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes a, c \otimes b \rangle, \langle s, t \rangle \big)$

This is exactly the existential represenation of the lens and the prism:

$\int^c \mathcal{C}(s, c \otimes a) \times \mathcal{C}(c \otimes b, t)$

This was an encouraging result, and I was able to derive a few other optics using the same approach.

The idea was that Tambara modules were just one example of a monoidal action, and it could be easily generalized to other types of optics, like Grate, where the action $c \otimes a$ is replaced by the (contravariant in $c$ ) action $a^c$ (or c->a, in Haskell).

There was just one optic that resisted that treatment, the Traversal. The breakthrough came when I was joined by a group of talented students at the Applied Category Theory School in Oxford.

Next: Traversals.

April 1, 2021

Traversals 1: van Laarhoven and Existentials

Posted by Bartosz Milewski under Programming | Tags: Category Theory, Lens, Optics |
[3] Comments

Note: A PDF version of this series is available on github.

My gateway drug to category theory was the Haskell lens library. What first piqued my attention was the van Laarhoven representation, which used functions that are functor-polymorphic. The following function type:

type Lens s t a b = 
  forall f. Functor f => (a -> f b) -> (s -> f t)

is isomorphic to the getter/setter pair that traditionally defines a lens:

get :: s -> a
set :: s -> b -> t

My intuition was that the Yoneda lemma must be somehow involved. I remember sharing this idea excitedly with Edward Kmett, who was the only expert on category theory I knew back then. The reasoning was that a polymorphic function in Haskell is equivalent to a natural transformation in category theory. The Yoneda lemma relates natural transformations to functor values. Let me explain.

In Haskell, the Yoneda lemma says that, for any functor f, this polymorphic function:

forall x. (a -> x) -> f x

is isomorphic to (f a).
In category theory, one way of writing it is:

$\int_{x} \mathbf{Set}\big(\mathcal{C}(a, x), f x\big) \cong f a$

If this looks a little intimidating, let me go through the notation:

The functor $f$ goes from some category $\mathcal{C}$ to the category of sets, which is called $\mathbf{Set}$ . Such functor is called a co-presheaf.
$\mathcal{C}(a, x)$ stands for the set of arrows from $a$ to $x$ in $\mathcal{C}$ , so it corresponds to the Haskell type a->x. In category theory it’s called a hom-set. The notation for hom-sets is: the name of the category followed by names of two objects in parentheses.
$\mathbf{Set}\big(\mathcal{C}(a, x), f x\big)$ stands for a set of functions from $\mathcal{C}(a, x)$ to $f x$ or, in Haskell (a -> x)-> f x. It’s a hom-set in $\mathbf{Set}$ .
Think of the integral sign as the forall quantifier. In category theory it’s called an end. Natural transformations between two functors $f$ and $g$ can be expressed using the end notation:
$\int_x \mathbf{Set}(f x, g x)$

As you can see, the translation is pretty straightforward. The van Laarhoven representation in this notation reads:

$\int_f \mathbf{Set}\big( \mathcal{C}(a, f b), \mathcal{C}(s, f t) \big)$

If you vary $x$ in $\mathcal{C}(b, x)$ , it becomes a functor, which is called a representable functor—the object $b$ “representing” the whole functor. In Haskell, we call it the reader functor:

newtype Reader b x = Reader (b -> x)

You can plug a representable functor for $f$ in the Yoneda lemma to get the following very important corollary:

$\int_x \mathbf{Set}\big(\mathcal{C}(a, x), \mathcal{C}(b, x)\big) \cong \mathcal{C}(b, a)$

The set of natural transformation between two representable functors is isomorphic to a hom-set between the representing objects. (Notice that the objects are swapped on the right-hand side.)

The van Laarhoven representation

There is just one little problem: the forall quantifier in the van Laarhoven formula goes over functors, not types.

This is okay, though, because category theory works at many levels. Functors themselves form a category, and the Yoneda lemma works in that category too.

For instance, the category of functors from $\mathcal{C}$ to $\mathbf{Set}$ is called $[\mathcal{C},\mathbf{Set}]$ . A hom-set in that category is a set of natural transformations between two functors which, as we’ve seen, can be expressed as an end:

$[\mathcal{C},\mathbf{Set}](f, g) \cong \int_x \mathbf{Set}(f x, g x)$

Remember, it’s the name of the category, here $[\mathcal{C},\mathbf{Set}]$ , followed by names of two objects (here, functors $f$ and $g$ ) in parentheses.

So the corollary to the Yoneda lemma in the functor category, after a few renamings, reads:

$\int_f \mathbf{Set}\big( [\mathcal{C},\mathbf{Set}](g, f), [\mathcal{C},\mathbf{Set}](h, f)\big) \cong [\mathcal{C},\mathbf{Set}](h, g)$

This is getting closer to the van Laarhoven formula because we have the end over functors, which is equivalent to

forall f. Functor f => ...

In fact, a judicious choice of $g$ and $h$ is all we need to finish the proof.

But sometimes it’s easier to define a functor indirectly, as an adjoint to another functor. Adjunctions actually allow us to switch categories. A functor $L$ defined by a mapping-out in one category can be adjoint to another functor $R$ defined by its mapping-in in another category.

$\mathcal{C}(L a, b) \cong \mathcal{D}(a, R b)$

A useful example is the currying adjunction in $\mathbf{Set}$ :

$\mathbf{Set}(c \times a, y) \cong \mathbf{Set}(c, y^a) \cong \mathbf{Set}\big(c, \mathbf{Set}(a, y)\big)$

where $y^a$ corresponds to the function type a->y and, in $\mathbf{Set}$ , is isomorphic to the hom-set $\mathbf{Set}(a, y)$ . This is just saying that a function of two arguments is equivalent to a function returning a function.

Here’s the clever trick: let’s replace $g$ and $h$ in the functorial Yoneda lemma with $L_b a$ and $L_t s$ , where $L_b$ and $L_t$ are some higher-order functors from $\mathcal{C}$ to $[\mathcal{C},\mathbf{Set}]$ (as you will see, this notation anticipates the final substitution). We get:

$\int_f \mathbf{Set}\big( [\mathcal{C},\mathbf{Set}](L_b a, f), [\mathcal{C},\mathbf{Set}](L_t s, f)\big) \cong [\mathcal{C},\mathbf{Set}](L_t s, L_b a)$

Now suppose that these functors are left adjoint to some other functors: $R_b$ and $R_t$ that go in the opposite direction from $[\mathcal{C},\mathbf{Set}]$ to $\mathcal{C}$ . We can then replace all mappings-out in $[\mathcal{C},\mathbf{Set}]$ with the corresponding mappings-in in $\mathcal{C}$ :

$\int_f \mathbf{Set}\big( \mathcal{C}(a, R_b f), \mathcal{C}(s, R_t f)\big) \cong \mathcal{C}\big(s, R_t (L_b a)\big)$

We are almost there! The last step is to realize that, in order to get the van Laarhoven formula, we need:

$R_b f = f b$

$R_t f = f t$

So these are just functors that apply $f$ to some fixed objects: $b$ and $t$ , respectively. The left-hand side becomes:

$\int_f \mathbf{Set}\big( \mathcal{C}(a, f b), \mathcal{C}(s, f t) \big)$

which is exactly the van Laarhoven representation.

Now let’s look at the right-hand side:

$\mathcal{C}\big(s, R_t (L_b a)\big) = \mathcal{C}\big( s, (L_b a) t \big)$

We know what $R_b$ is, but what’s its left adjoint $L_b$ ? It must satisfy the adjunction:

$[\mathcal{C},\mathbf{Set}](L_b a, f) \cong \mathcal{C}(a, R_b f) = \mathcal{C}(a, f b)$

or, using the end notation:

$\int_x \mathbf{Set}\big((L_b a) x, f x\big) \cong \mathcal{C}(a, f b)$

This identity has a simple solution when $\mathcal{C}$ is $\mathbf{Set}$ , so we’ll just temporarily switch to $\mathbf{Set}$ . We have:

$(L_b a) x = \mathbf{Set}(b, x) \times a$

which is known as the IStore comonad in Haskell. We can check the identity by first applying the currying adjunction to eliminate the product:

$\int_x \mathbf{Set}\big(\mathbf{Set}(b, x) \times a, f x\big) \cong \int_x \mathbf{Set}\big(\mathbf{Set}(b, x), \mathbf{Set}(a, f x )\big)$

and then using the Yoneda lemma to “integrate” over $x$ , which replaces $x$ with $b$ ,

$\int_x \mathbf{Set}\big(\mathbf{Set}(b, x), \mathbf{Set}(a, f x )\big) \cong \mathbf{Set}(a, f b)$

So the right hand side of the original identity (after replacing $\mathcal{C}$ with $\mathbf{Set}$ ) becomes:

$\mathbf{Set}\big(s, R_t (L_b a)\big) \cong \mathbf{Set}\big( s, (L_b a) t \big) \cong \mathbf{Set}\big(s, \mathbf{Set}(b, t) \times a) \big)$

which can be translated to Haskell as:

(s -> b -> t, s -> a)

or a pair of set and get.

I was very proud of myself for finding the right chain of substitutions, so I was pretty surprised when I learned from Mauro Jaskelioff and Russell O’Connor that they had a paper ready for publication with exactly the same proof. (They added a reference to my blog in their publication, which was probably a first.)

The Existentials

But there’s more: there are other optics for which this trick doesn’t work. The simplest one was the prism defined by a pair of functions:

match :: s -> Either t a
build :: b -> t

In this form it’s hard to see a commonality between a lens and a prism. There is, however, a way to unify them using existential types.

Here’s the idea: A lens can be applied to types that, at least conceptually, can be decomposed into two parts: the focus and the residue. It lets us extract the focus using get, and replace it with a new value using set, leaving the residue unchanged.

The important property of the residue is that it’s opaque: we don’t know how to retrieve it, and we don’t know how to modify it. All we know about it is that it exists and that it can be combined with the focus. This property can be expressed using existential types.

Symbolically, we would want to write something like this:

type Lens s t a b = exists c . (s -> (c, a), (c, b) -> t)

where c is the residue. We have here a pair of functions: The first decomposes the source s into the product of the residue c and the focus a . The second recombines the residue with the new focus b resulting in the target t.

Existential types can be encoded in Haskell using GADTs:

data Lens s t a b where
  Lens :: (s -> (c, a), (c, b) -> t) -> Lens s t a b

They can also be encoded in category theory using coends. So the lens can be written as:

$\int^c \mathcal{C}(s, c \times a) \times \mathcal{C}(c \times b, t)$

The integral sign with the argument at the top is called a coend. You can read it as “there exists a $c$ ”.

There is a version of the Yoneda lemma for coends as well:

$\int^c f c \times \mathcal{C}(c, a) \cong f a$

The intuition here is that, given a functorful of $c$ ‘s and a function c->a, we can fmap the latter over the former to obtain f a. We can do it even if we have no idea what the type c is.

We can use the currying adjunction and the Yoneda lemma to transform the new definition of the lens to the old one:

$\int^c \mathcal{C}(s, c \times a) \times \mathcal{C}(c \times b, t) \cong \int^c \mathcal{C}(s, c \times a) \times \mathcal{C}(c, t^b) \cong \mathcal{C}(s, t^b \times a)$

The exponential $t^b$ translates to the function type b->t, so this this is really the set/get pair that defines the lens.

The beauty of this representation is that it can be immediately applied to the prism, just by replacing the product with the sum (coproduct). This is the existential representation of a prism:

$\int^c \mathcal{C}(s, c + a) \times \mathcal{C}(c + b, t)$

To recover the standard encoding, we use the mapping-out property of the sum:

$\mathcal{C}(c + b, t) \cong \mathcal{C}(c, t) \times \mathcal{C}(b, t)$

This is simply saying that a function from the sum type is equivalent to a pair of functions—what we call case analysis in programming.

We get:

$\int^c \mathcal{C}(s, c + a) \times \mathcal{C}(c + b, t) \cong \int^c \mathcal{C}(s, c + a) \times \mathcal{C}(c, t) \times \mathcal{C}(b, t)$

This has the form suitable for the use of the Yoneda lemma, namely:

$\int^c f c \times \mathcal{C}(c, t)$

with the functor

$f c = \mathcal{C}(s, c + a) \times \mathcal{C}(b, t)$

The result of the Yoneda is replacing $c$ with $t$ , so the result is:

$\mathcal{C}(s, t + a) \times \mathcal{C}(b, t)$

which is exactly the match/build pair (in Haskell, the sum is translated to Either).

It turns out that every optic has an existential form.

Next: Profunctors.

February 16, 2021

Functorio

Posted by Bartosz Milewski under Programming
[17] Comments

You might have heard people say that functional programming is more academic, and real engineering is done in imperative style. I’m going to show you that real engineering is functional, and I’m going to illustrate it using a computer game that is designed by engineers for engineers. It’s a simulation game called Factorio, in which you are given resources that you have to explore, build factories that process them, create more and more complex systems, until you are finally able to launch a spaceship that may take you away from an inhospitable planet. If this is not engineering at its purest then I don’t know what is. And yet almost all you do when playing this game has its functional programming counterparts and it can be used to teach basic concepts of not only programming but also, to some extent, category theory. So, without further ado, let’s jump in.

Functions

The building blocks of every programming language are functions. A function takes input and produces output. In Factorio they are called assembling machines, or assemblers. Here’s an assembler that produces copper wire.

If you bring up the info about the assembler you’ll see the recipe that it’s using. This one takes one copper plate and produces a pair of coils of copper wire.

This recipe is really a function signature in a strongly typed system. We see two types: copper plate and copper wire, and an arrow between them. Also, for every copper plate the assembler produces a pair of copper wires. In Haskell we would declare this function as

makeCopperWire :: CopperPlate -> (CopperWire, CopperWire)

Not only do we have types for different components, but we can combine types into tuples–here it’s a homogenous pair (CopperWire, CopperWire). If you’re not familiar with Haskell notation, here’s what it might look like in C++:

std::pair<CopperWire, CopperWire> makeCopperWire(CopperPlate);

Here’s another function signature in the form of an assembler recipe:

It takes a pair of iron plates and produces an iron gear wheel. We could write it as

makeGear :: (IronPlate, IronPlate) -> Gear

or, in C++,

Gear makeGear(IronPlate, IronPlate);

Many recipes require a combination of differently typed ingredients, like the one for producing red science packs

We would declare this function as:

makeRedScience :: (CopperPlate, Gear) -> RedScience

Pairs are examples of product types. Factorio recipes use the plus sign to denote tuples; I guess this is because we often read a sum as “this and this”, and “and” introduces a product type. The assembler requires both inputs to produce the output, so it accepts a product type. If it required either one, we’d call it a sum type.

We can also tuple more than two ingredients, as in this recipe for producing electronic circuits (or green circuits, as they are commonly called)

makeGreenCircuit :: 
  (CopperWire, CopperWire, CopperWire, IronPlate) -> GreenCircuit

Now suppose that you have at your disposal the raw ingeredients: iron plates and copper plates. How would you go about producing red science or green circuits? This is where function composition kicks in. You can pass the output of the copper wire assembler as the input to the green circuit assembler. (You will still have to tuple it with an iron plate.)

Similarly, you can compose the gear assembler with the red science assembler.

The result is a new function with the following signature

makeRedScienceFrom :: 
    (CopperPlate, IronPlate, IronPlate) -> RedScience

And this is the implementation:

makeRedScienceFrom (cu, fe1, fe2) = 
    makeRedScience (cu, makeGear (fe1, fe2))

You start with one copper plate and two iron plates. You feed the iron plates to the gear assembler. You pair the resulting gear with the copper plate and pass it to the red science assembler.

Most assemblers in Factorio take more than one argument, so I couldn’t come up with a simpler example of composition, one that wouldn’t require untupling and retupling. In Haskell we usually use functions in their curried form (we’ll come back to this later), so composition is easy there.

Composition is also a feature of a category, so we should ask the question if we can treat assemblers as arrows in a category. Their composition is obviously associative. But do we have an equivalent of an identity arrow? It is something that takes input of some type and returns it back unchanged. And indeed we have things called inserters that do exactly that. Here’s an inserter between two assemblers.

In fact, in Factorio, you have to use an inserter for direct composition of assemblers, but that’s an implementation detail (technically, inserting an identity function doesn’t change anything).

An inserter is actually a polymorphic function, just like the identity function in Haskell

inserter :: a -> a
inserter x = x

It works for any type a.

But the Factorio category has more structure. As we have seen, it supports finite products (tuples) of arbitrary types. Such a category is called cartesian. (We’ll talk about the unit of this product later.)

Notice that we have identified multiple Factorio subsystem as functions: assemblers, inserters, compositions of assemblers, etc. In a programming language they would all be just functions. If we were to design a language based on Factorio (we could call it Functorio), we would enclose the composition of assemblers into an assembler, or even make an assembler that takes two assemblers and produces their composition. That would be a higher-order assembler.

Higher order functions

The defining feature of functional languages is the ability to make functions first-class objects. That means the ability to pass a function as an argument to another function, and to return a function as a result of another function. For instance, we should have a recipe for producing assemblers. And, indeed, there is such recipe. All it needs is green circuits, some gear wheels, and a few iron plates:

If Factorio were a strongly typed language all the way, there would be separate recipes for producing different assemblers (that is assemblers with different recipes). For instance, we could have:

makeRedScienceAssembler :: 
   (GreenCircuit, Gear, IronPlate) -> RedScienceAssembler

Instead, the recipe produces a generic assembler, and it lets the player manually set the recipe in it. In a way, the player provides one last ingredient, an element of the enumeration of all possible recipes. This enumeration is displayed as a menu of choices:

After all, Factorio is an interactive game.

Since we have identified the inserter as the identity function, we should have a recipe for producing it as well. And indeed there is one:

Do we also have functions that take functions as arguments? In other words, recipes that use assemblers as input? Indeed we do:

Again, this recipe accepts a generic assembler that hasn’t been assigned its own recipe yet.

This shows that Factorio supports higher-order functions and is indeed a functional language. What we have here is a way of treating functions (assemblers) not only as arrows between objects, but also as objects that can be produced and consumed by functions. In category theory, such objectified arrow types are called exponential objects. A category in which arrow types are represented as objects is called closed, so we can view Factorio as a cartesian closed category.

In a strongly typed Factorio, we could say that the object RedScienceAssembler

is equivalent to its recipe

type RedScienceAssembler = 
    (CopperPlate, Gear) -> RedScience

We could then write a higher-order recipe that produces this particular assembler as:

makeRedScienceAssembler :: 
     (GreenCircuit, Gear, IronPlate) 
  -> ((CopperPlate, Gear) -> RedScience)

Similarly, in a strongly typed Factorio we would replace this higher-order recipe

with the following signature

makeGreenScience :: ((a -> a), Belt) -> GreenScience

assuming that the inserter is a polymorphic function a -> a.

Linear types

There is one important aspect of functional programming that seems to be broken in Factorio. Functions are supposed to be pure: mutation is a no-no. And in Factorio we keep talking about assemblers consuming resources. A pure function doesn’t consume its arguments–you may pass the same item to many functions and it will still be there. Dealing with resources is a real problem in programming in general, including purely functional languages. Fortunately there are clever ways of dealing with it. In C++, for instance, we can use unique pointers and move semantics, in Rust we have ownership types, and Haskell recently introduced linear types. What Factorio does is very similar to Haskell’s linear types. A linear function is a function that is guaranteed to consume its argument. Functorio assemblers are linear functions.

Factorio is all about consuming and transforming resources. The resources originate as various ores and coal in mines. There are also trees that can be chopped to yield wood, and liquids like water or crude oil. These external resources are then consumed, linearly, by your industry. In Haskell, we would implement it by passing a linear function called a continuation to the resource producer. A linear function guarantees to consume the resource completely (no resource leaks) and not to make multiple copies of the same resource. These are the guarantees that the Factorio industrial complex provides automatically.

Currying

Of course Factorio was not designed to be a programming language, so we can’t expect it to implement every aspect of programming. It is fun though to imagine how we would translate some more advanced programming features into Factorio. For instance, how would currying work? To support currying we would first need partial application. The idea is pretty simple. We have already seen that assemblers can be treated as first class objects. Now imagine that you could produce assemblers with a set recipe (strongly typed assemblers). For instance this one:

It’s a two-input assembler. Now give it a single copper plate, which in programmer speak is called partial application. It’s partial because we haven’t supplied it with an iron gear. We can think of the result of partial application as a new single-input assembler that expects an iron gear and is able to produce one beaker of red science. By partially applying the function makeRedScience

makeRedScience :: (CopperPlate, Gear) -> RedScience

we have created a new function of the type

Gear -> RedScience

In fact we have just designed a process that gave us a (higher-order) function that takes a copper plate and creates a “primed” assembler that only needs an iron gear to produce red science:

makeGearToRedScience :: CopperPlate -> (Gear -> RedScience)

In Haskell, we would implement this function using a lambda expression

makeGearToRedScience cu = \gear -> makeRedScience (cu, gear)

Now we would like to automate this process. We want to have something that takes a two-input assembler, for instance makeRedScience, and returns a single input assembler that produces another “primed” single-input assembler. The type signature of this beast would be:

curryRedScienceAssembler ::
     ((CopperPlate, Gear) -> RedScience)  -- RedScienceAssembler
  -> (CopperPlate -> (Gear -> RedScience))

We would implement it as a double lambda:

curryRedScienceAssembler rsAssembler = 
  \cu -> (\gear -> rsAssembler (cu, gear))

Notice that it really doesn’t matter what the concrete types are. What’s important is that we can turn a function that takes a pair of arguments into a function that returns a function. We can make it fully polymorphic:

curry :: ((a, b) -> c) 
       -> (a -> (b -> c))

Here, the type variables a, b and c can be replaced with any types (in particular, CopperPlate, Gear, and RedScience).
This is a Haskell implementation:

curry f = \a -> \b -> f (a, b)

Functors

So far we haven’t talked about how arguments (items) are delivered to functions (assemblers). We can manually drop items into assemblers, but that very quickly becomes boring. We need to automate the delivery systems. One way of doing it is by using some kind of containers: chests, train wagons, barrels, or conveyor belts. In programming we call these functors. Strictly speaking a functor can hold only one type of items at a time, so a chest of iron plates should be a different type than a chest of gears. Factorio doesn’t enforce this but, in practice, we rarely mix different types of items in one container.

The important property of a functor is that you can apply a function to its contents. This is best illustrated with conveyor belts. Here we take the recipe that turns a copper plate into copper wire and apply it to a whole conveyor belt of copper (coming from the right) to produce a conveyor belt of copper wire (going to the left).

The fact that a belt can carry any type of items can be expressed as a type constructor–a data type parameterized by an arbitrary type a

data Belt a

You can apply it to any type to get a belt of specific items, as in

Belt CopperPlate

We will model belts as Haskell lists.

data Belt a = MakeBelt [a]

The fact that it’s a functor is expressed by implementing a polymorphic function mapBelt

mapBelt :: (a -> b) -> (Belt a -> Belt b)

This function takes a function a->b and produces a function that transforms a belt of as to a belt of bs. So to create a belt of (pairs of) copper wire we’ll map the assembler that implements makeCoperWire over a belt of CopperPlate

makeBeltOfWire :: (Belt CopperPlate) -> (Belt (CopperWire, CopperWire))
makeBeltOfWire = mapBelt makeCopperWire

You may think of a belt as corresponding to a list of elements, or an infinite stream, depending on the way you use it.

In general, a type constructor F is called a functor if it supports the mapping of a function over its contents:

map :: (a -> b) -> (F a -> F b)

Sum types

Uranium ore processing is interesting. It is done in a centrifuge, which accepts uranium ore and produces two isotopes of Uranium.

The new thing here is that the output is probabilistic. Most of the time (on average, 99.3% of the time) you’ll get Uranium 238, and only occasionally (0.7% of the time) Uranium 235 (the glowy one). Here the plus sign is used to actually encode a sum type. In Haskell we would use the Either type constructor, which generates a sum type:

makeUranium :: UraniumOre -> Either U235 U238

In other languages you might see it called a tagged union.

The two alternatives in the output type of the centrifuge require different actions: U235 can be turned into fuel cells, whereas U238 requires reprocessing. In Haskell, we would do it by pattern matching. We would apply one function to deal with U235 and another to deal with U238. In Factorio this is accomplished using filter inserters (a.k.a., purple inserters). A filter inserter corresponds to a function that picks one of the alternatives, for instance:

filterInserterU235 :: Either U235 U238 -> Maybe U235

The Maybe data type (or Optional in some languages) is used to accommodate the possibility of failure: you can’t get U235 if the union contained U238.

Each filter inserter is programmed for a particular type. Below you see two purple inserters used to split the output of the centrifuge into two different chests:

Incidentally, a mixed conveyor belt may be seen as carrying a sum type. The items on the belt may be, for instance, either copper wire or steel plates, which can be written as Either CopperWire SteelPlate. You don’t even need to use purple inserters to separate them, as any inserter becomes selective when connected to the input of an assembler. It will only pick up the items that are the inputs of the recipe for the given assembler.

Monoidal functors

Every conveyor belt has two sides, so it’s natural to use it to transport pairs. In particular, it’s possible to merge a pair of belts into one belt of pairs.

We don’t use an assembler to do it, just some belt mechanics, but we can still think of it as a function. In this case, we would write it as

(Belt CopperPlate, Belt Gear) -> Belt (CopperPlate, Gear)

In the example above, we map the red science function over it

streamRedScience :: Belt (CopperPlate, Gear) -> Belt RedScience
streamRedScience beltOfPairs = mapBelt makeRedScience beltOfPairs

Since makeRedScience has the signature

makeRedScience :: (CopperPlate, Gear) -> RedScience

it all type checks.

Since we can apply belt merging to any type, we can write it as a polymorphic function

mergeBelts :: (Belt a, Belt b) -> Belt (a, b)
mergeBelts (MakeBelt as, MakeBelt bs) = MakeBelt (zip as bs)

(In our Haskell model, we have to zip two lists together to get a list of pairs.)

Belt is a functor. In general, a functor that has this kind of merging ability is called a monoidal functor, because it preserves the monoidal structure of the category. Here, the monoidal structure of the Factorio category is given by the product (pairing). Any monoidal functor F must preserve the product:

(F a, F b) -> F (a, b)

There is one more aspect to monoidal structure: the unit. The unit, when paired with anything, does nothing to it. More precisely, a pair (Unit, a) is, for all intents and purposes, equivalent to a. The best way to understand the unit in Factorio is to ask the question: The belt of what, when merged with the belt of a, will produce a belt of a? The answer is: the belt of nothing. Merging an empty belt with any other belt, makes no difference.

So emptiness is the monoidal unit, and we have, for instance:

(Belt CopperPlate, Belt Nothing) -> Belt CopperPlate

The ability to merge two belts, together with the ability to create an empty belt, makes Belt a monoidal functor. In general, besides preserving the product, the condition for the functor F to be monoidal is the ability to produce

F Nothing

Most functors, at least in Factorio, are not monoidal. For instance, chests cannot store pairs.

Applicative functors

As I mentioned before, most assembler recipes take multiple arguments, which we modeled as tuples (products). We also talked about partial application which, essentially, takes an assembler and one of the ingredients and produces a “primed” assembler whose recipe requires one less ingredient. Now imagine that you have a whole belt of a single ingredient, and you map an assembler over it. In current Factorio, this assembler will accept one item and then get stuck waiting for the rest. But in our extended version of Factorio, which we call Functorio, mapping a multi-input assembler over a belt of single ingredient should produce a belt of “primed” assemblers. For instance, the red science assembler has the signature

(CopperPlate, Gear) -> RedScience

When mapped over a belt of CopperPlate it should produce a belt of partially applied assemblers, each with the recipe:

Gear -> RedScience

Now suppose that you have a belt of gears ready. You should be able to produce a belt of red science. If there only were a way to apply the first belt over the second belt. Something like this:

(Belt (Gear -> RedScience), Belt Gear) -> Belt RedScience

Here we have a belt of primed assemblers and a belt of gears and the output is a belt of red science.

A functor that supports this kind of merging is called an applicative functor. Belt is an applicative functor. In fact, we can tell that it’s applicative because we’ve established that it’s monoidal. Indeed, monoidality lets us merge the two belts to get a belt of pairs

Belt (Gear -> RedScience, Gear)

We know that there is a way of applying the Gear->RedScience assembler to a Gear resulting in RedScience. That’s just how assemblers work. But for the purpose of this argument, let’s give this application an explicit name: eval.

eval :: (Gear -> RedScience, Gear) -> RedScience
eval (gtor, gr) = gtor gr

(gtor gr is just Haskell syntax for applying the function gtor to the argument gr). We are abstracting the basic property of an assembler that it can be applied to an item.

Now, since Belt is a functor, we can map eval over our belt of pairs and get a belt of RedScience.

apBelt :: (Belt (Gear -> RedScience), Belt Gear) -> Belt RedScience
apBelt (gtors, gear) = mapBelt eval (mergeBelts (gtors, gears))

Going back to our original problem: given a belt of copper plate and a belt of gear, this is how we produce a belt of red science:

redScienceFromBelts :: (Belt CopperPlate, Belt Gear) -> Belt RedScience
redScienceFromBelts (beltCu, beltGear) = 
  apBelt (mapBelt (curry makeRedScience) beltCu, beltGear)

We curry the two-argument function makeRedScience and map it over the belt of copper plates. We get a beltful of primed assemblers. We then use apBelt to apply these assemblers to a belt of gears.

To get a general definition of an applicative functor, it’s enough to replace Belt with generic functor F, CopperPlate with a, and Gear with b. A functor F is applicative if there is a polymorphic function:

(F (a -> b), F a) -> F b

or, in curried form,

F (a -> b) -> F a -> F b

To complete the picture, we also need the equivalent of the monoidal unit law. A function called pure plays this role:

pure :: a -> F a

This just tell you that there is a way to create a belt with a single item on it.

Monads

In Factorio, the nesting of functors is drastically limited. It’s possible to produce belts, and you can put them on belts, so you can have a beltful of belts, Belt Belt. Similarly you can store chests inside chests. But you can’t have belts of loaded belts. You can’t pick a belt filled with copper plates and put it on another belt. In other words, you cannot transport beltfuls of stuff. Realistically, that wouldn’t make much sense in real world, but in Functorio, this is exactly what we need to implement monads. So imagine that you have a belt carrying a bunch of belts that are carrying copper plates. If belts were monadic, you could turn this whole thing into a single belt of copper plates. This functionality is called join (in some languages, “flatten”):

join :: Belt (Belt CopperPlate) -> Belt CopperPlate

This function just gathers all the copper plates from all the belts and puts them on a single belt. You can thing of it as concatenating all the subbelts into one.

Similarly, if chests were monadic (and there’s no reason they shouldn’t be) we would have:

join :: Chest (Chest Gear) -> Chest Gear

A monad must also support the applicative pure (in Haskell it’s called return) and, in fact, every monad is automatically applicative.

Conclusion

There are many other aspects of Factorio that lead to interesting topics in programming. For instance, the train system requires dealing with concurrency. If two trains try to enter the same crossing, we’ll have a data race which, in Functorio, is called a train crash. In programming, we avoid data races using locks. In Factorio, they are called train signals. And, of course, locks lead to deadlocks, which are very hard to debug in Factorio.

In functional programming we might use STM (Software Transactional Memory) to deal with concurrency. A train approaching a crossing would start a crossing transaction. It would temporarily ignore all other trains and happily make the crossing. Then it would attempt to commit the crossing. The system would then check if, in the meanwhile, another train has successfully commited the same crossing. If so, it would say “oops! try again!”.

August 11, 2020

Benign Data Races Considered Harmful

Posted by Bartosz Milewski under Atomics, C++, Concurrency, Memory Model, Multicore, Multithreading, Programming
[4] Comments

The series of posts about so called benign data races stirred a lot of controversy and led to numerous discussions at the startup I was working at called Corensic. Two bastions formed, one claiming that no data race was benign, and the other claiming that data races were essential for performance. Then it turned out that we couldn’t even agree on the definition of a data race. In particular, the C++11 definition seemed to deviate from the established notions.

What Is a Data Race Anyway?

First of all, let’s make sure we know what we’re talking about. In current usage a data race is synonymous with a low-level data race, as opposed to a high-level race that involves either multiple memory locations, or multiple accesses per thread. Everybody agrees on the meaning of data conflict, which is multiple threads accessing the same memory location, at least one of them through a write. But a data conflict is not necessarily a data race. In order for it to become a race, one more condition must be true: the access has to be “simultaneous.”

Unfortunately, simultaneity is not a well defined term in concurrent systems. Leslie Lamport was the first to observe that a distributed system follows the rules of Special Relativity, with no independent notion of simultaneity, rather than those of Galilean Mechanics, with its absolute time. So, really, what defines a data race is up to your notion of simultaneity.

Maybe it’s easier to define what isn’t, rather than what is, simultaneous? Indeed, if we can tell which event happened before another event, we can be sure that they weren’t simultaneous. Hence the use of the famous “happened before” relationship in defining data races. In Special Relativity this kind of relationship is established by the exchange of messages, which can travel no faster than the speed of light. The act of sending a message always happens before the act of receiving the same message. In concurrent programming this kind of connection is made using synchronizing actions. Hence an alternative definition of a data race: A memory conflict without intervening synchronization.

The simplest examples of synchronizing actions are the taking and the releasing of a lock. Imagine two threads executing this code:

  mutex.lock();
  x = x + 1;
  mutex.unlock();

In any actual execution, accesses to the shared variable x from the two threads will be separated by a synchronization. The happens-before (HB) arrow will always go from one thread releasing the lock to the other thread acquiring it. For instance in:

#	Thread 1	Thread 2
1		mutex.lock();
2		x = x + 1;
3		mutex.unlock();
4	mutex.lock();
5	x = x + 1;
6	mutex.unlock();

the HB arrow goes from 3 to 4, clearly separating the conflicting accesses in 2 and 5.

Notice the careful choice of words: “actual execution.” The following execution that contains a race can never happen, provided the mutex indeed guarantees mutual exclusion:

#	Thread 1	Thread 2
1		mutex.lock();
2	mutex.lock();
3	x = x + 1;	x = x + 1;
4		mutex.unlock();
5	mutex.unlock();

It turns out that the selection of possible executions plays an important role in the definition of a data race. In every memory model I know of, only sequentially consistent executions are tried in testing for data races. Notice that non-sequentially-consistent executions may actually happen, but they do not enter the data-race test.

In fact, most languages try to provide the so called DRF (Data Race Free) guarantee, which states that all executions of data-race-free programs are sequentially consistent. Don’t be alarmed by the apparent circularity of the argument: you start with sequentially consistent executions to prove data-race freedom and, if you don’t find any data races, you conclude that all executions are sequentially consistent. But if you do find a data race this way, then you know that non-sequentially-consistent executions are also possible.

DRF guarantee. If there are no data races for sequentially consistent executions, there are no non-sequentially consistent executions. But if there are data races for sequentially consistent executions, the non-sequentially consistent executions are possible.

As you can see, in order to define a data race you have to precisely define what you mean by “simultaneous,” or by “synchronization,” and you have to specify to which executions your definition may be applied.

The Java Memory Model

In Java, besides traditional mutexes that are accessed through “synchronized” methods, there is another synchronization device called a volatile variable. Any access to a volatile variable is considered a synchronization action. You can draw happens-before arrows not only between consecutive unlocks and locks of the same object, but also between consecutive accesses to a volatile variable. With this extension in mind, Java offers the the traditional DRF guarantee. The semantics of data-race free programs is well defined in terms of sequential consistency thus making every Java programmer happy.

But Java didn’t stop there, it also attempted to provide at least some modicum of semantics for programs with data races. The idea is noble–as long as programmers are human, they will write buggy programs. It’s easy to proclaim that any program with data races exhibits undefined behavior, but if this undefined behavior results in serious security loopholes, people get really nervous. So what the Java memory model guarantees on top of DRF is that the undefined behavior resulting from data races cannot lead to out-of-thin-air values appearing in your program (for instance, security credentials for an intruder).

It is now widely recognized that this attempt to define the semantics of data races has failed, and the Java memory model is broken (I’m citing Hans Boehm here).

The C++ Memory Model

Why is it so important to have a good definition of a data race? Is it because of the DRF guarantee? That seems to be the motivation behind the Java memory model. The absence of data races defines a subset of programs that are sequentially consistent and therefore have well-defined semantics. But these two properties: being sequentially consistent and having well-defined semantics are not necessarily the same. After all, Java tried (albeit unsuccessfully) to define semantics for non sequentially consistent programs.

So C++ chose a slightly different approach. The C++ memory model is based on partitioning all programs into three categories:

Sequentially consistent,
Non-sequentially consistent, but with defined semantics, and
Incorrect programs with undefined semantics

The first category is very similar to race-free Java programs. The place of Java volatile is taken by C++11 default atomic. The word “default” is crucial here, as we’ll see in a moment. Just like in Java, the DRF guarantee holds for those programs.

It’s the second category that’s causing all the controversy. It was introduced not so much for security as for performance reasons. Sequential consistency is expensive on most multiprocessors. This is why many C++ programmers currently resort to “benign” data races, even at the risk of undefined behavior. Hans Boehm’s paper, How to miscompile programs with “benign” data races, delivered a death blow to such approaches. He showed, example by example, how legitimate compiler optimizations may wreak havoc on programs with “benign” data races.

Fortunately, C++11 lets you relax sequential consistency in a controlled way, which combines high performance with the safety of well-defined (if complex) semantics. So the second category of C++ programs use atomic variables with relaxed memory ordering semantics. Here’s some typical syntax taken from my previous blog post:

std::atomic<int> owner = 0
...
owner.load(memory_order_relaxed);

And here’s the controversial part: According to the C++ memory model, relaxed memory operations, like the above load, don’t contribute to data races, even though they are not considered synchronization actions. Remember one of the versions of the definition of a data race: Conflicting actions without intervening synchronization? That definition doesn’t work any more.

The C++ Standard decided that only conflicts for which there is no defined semantics are called data races.

Notice that some forms of relaxed atomics may introduce synchronization. For instance, a write access with memory_order_release “happens before” another access with memory_order_acquire, if the latter follows the former in a particular execution (but not if they are reversed!).

Conclusion

What does it all mean for the C++11 programmer? It means that there no longer is an excuse for data races. If you need benign data races for performance, rewrite your code using weak atomics. Weak atomics give you the same kind of performance as benign data races but they have well defined semantics. Traditional “benign” races are likely to be broken by optimizing compilers or on tricky architectures. But if you use weak atomics, the compiler will apply whatever means necessary to enforce the correct semantics, and your program will always execute correctly. It will even naturally align atomic variables to avoid torn reads and writes.

What’s more, since C++11 has well defined memory semantics, compiler writers are no longer forced to be conservative with their optimizations. If the programmer doesn’t specifically mark shared variables as atomic, the compiler is free to optimize code as if it were single-threaded. So all those clever tricks with benign data races are no longer guaranteed to work, even on relatively simple architectures, like the x86. For instance, compiler is free to use your lossy counter or a binary flag for its own temporary storage, as long as it restores it back later. If other threads access those variables through racy code, they might see arbitrary values as part of the “undefined behavior.” You have been warned!
Follow @BartoszMilewski

Programming

Disclaimers

Implementation hiding

Functors

Continuations

The Yoneda Lemma

Existential Types

Producer/Consumer

Co-Yoneda Lemma

Contravariant Consumers

Existential Lens

Type-Changing Lens

Other Optics

Profunctors

Profunctor Optics

Main Takeaways

Abstract

Motivation

Co-presheaves

Composition

Generalizations

Appendix

Motivation

Monoidal Action

Profunctor Representation

Counted Vectors and Trees

Existential Types

Polynomial Lens

Using the Lens

Example

Testing

Dependent optics

Dependent lens

Traversals

Traversals

Generalizations

The Physicist’s Explanation

Conclusion

Double Yoneda

Profunctors

Tambara Modules

Double Yoneda with Adjunctions

Profunctor Representation of Lenses and Prisms

The van Laarhoven representation

The Existentials

Functions

Higher order functions

Linear types

Currying

Functors

Sum types

Monoidal functors

Applicative functors

Monads

Conclusion

What Is a Data Race Anyway?

The Java Memory Model

The C++ Memory Model

Conclusion

Top Posts

License

Blogroll

Follow Me

Archives