Bartosz Milewski's Programming Cafe

You may think of Tannakian Reconstruction as an example of redundant encoding. It lets you replace a simple hom-set with a much more complex end that is taken over an entire functor category.

Why would anyone want to do it? The answer is simple: composition! Morphisms on the left compose according to the rules of the category , which can be arbitrarily complex. By contrast, the right hand side lives in , and its elements are functions with very simple composition rules. So any time you want to internalize a non-trivial category in a programming language like Haskell, the Tannakian representation becomes a valuable tool. One such example is the category of optics.

Optics

A simple category of optics over a single category has objects that are pairs of objects . The morphisms are defined using the action of a monoidal category (thus making an actegory):

In what follows, we’ll be using the fact that an element of a coend can be constructed by injecting a triple of an object and a pair of morphisms:

Optics compose by “zooming in”:

The identity optic is given by injecting the triple into the coend:

where:

is the left unitor for the monoidal action and the unit object.

The archetypical optic is a lens, whose action is defined as the cartesian product in :

In Haskell, we would encode it as an existential type:

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

This formula can be expanded using the mapping-in property of the product (or, in an alternative derivation, its mapping out property, that is currying):

Using the Yoneda reduction (a.k.a. “integrating” over ), we get:

which, in Haskell, corresponds to a pair of functions:

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

The getter extracts the subobject a, the focus of the lens. The setter replaces it with b.

Lenses compose by zooming in: the focus of one lens becomes the source of the other.

In Haskell this can be encoded as:

composeLens :: Lens a b a' b' -> Lens s t a b -> Lens s t a' b'
composeLens (Lens l2 r2) (Lens l1 r1) = Lens l3 r3
  where l3 = assoc' . second l2 . l1
        r3 = r1 . second r2 . assoc
        assoc ((c, c'), b')  = (c, (c', b'))
        assoc' (c, (c', a')) = ((c, c'), a')
  

As you can see, optic composition can be quite messy. That’s where the Tannakian representation saves the day.

Optics and Tambara modules

The idea is to follow the Tannakian reconstruction by defining the category of set-valued functors over the category of optics and use the end over these functors to represent optics.

It turns out that set-valued functors on optics are our old friends, Tambara modules. There is an equivalence of categories:

We use the opposite category of optics because, traditionally, optic composition is defiened in terms of zooming in rather than zooming out. Thus the slogan is: Presheaves on optics are Tambara modules.

Let’s first analyze the definition of a presheaf . On objects, it maps pairs to sets .

On morphisms, it maps optics to functions (reversing the direction). Thus an optic:

is mapped to a function:

.

The plan is to construct two mappings: from presheaves to Tambara modules and another from Tambara modules to presheaves. They have to be defined on (pairs of) objects as well as on morphisms. I will first sketch the proof using category theory and then translate it, step by step, to Haskell.

From presheaf to Tambara

On objects, given a presheaf , we define a profunctor:

We know that it’s a profunctor because, given a pair of morphisms:

we can construct a mapping:

We do this by lifting an optic of the type:

This optic can be instantiated by injecting into the coend.

The tricky part is to equip with the Tambara structure:

In this case, we want to implement:

We’ll do this by lifting a carefuly chosen optic of the type:

This optic is given by the following coend:

We instantiate it by injecting the triple into the coend.

On morphisms, we want to map an optic to an element of the hom-set . This mapping itself is an element of a bigger hom-set:

Using the co-continuity of the hom-set, we replace the mapping out of a coend with the end:

We have at our disposal a pair of morphisms:

which, together with the Tambara structure, give us the desired mapping:

From Tambara to presheaf

On objects, given a Tambara module , we define a presheaf :

On morphisms, we have to map a function on Tambara modules to an optic. To do that, we need to come up with a specific Tambara module to feed it to this function. Since we want to produce an optic, it makes sense that we feed it an optic. The question is: Are optics Tambara modules?

An optic is a profunctor in each pair of arguments. Let’s see if we can come up with a Tambara structure in while keeping the pair constant. Given:

We want to produce:

.

We have at our disposal a pair of morphisms:

We know that simple hom-sets are Tambara modules, so we can apply the Tambara structure to both morphism:

After re-associating the iterated actions we inject the triple that consist of and the two resulting morphisms into our target coend.

Profunctor representation of optics

Since presheaves on are Tambara modules, we can use the Tannakian reconstruction to represent a hom set in as an end over Tambara modules:

This is the general form of the profunctor representation of optics that works for any monoidal action.

Haskell implementation

In Haskell, we can encode general optics (morphisms in ) as:

data Opt ten act1 act2 s t a b = 
  forall m. (Actegory ten act1, Actegory ten act2) 
    => Opt (s -> m `act1` a) (m `act2` b -> t)
  

Notice that it’s okay to use two different actions (in fact, one can use two different categories). The corresponding Tambara modules are defined as:

class (Actegory ten act1, Actegory ten act2, Profunctor p) 
  => Tambara ten act1 act2 p where
    leftAct :: p a b -> p (m `act1` a) (m `act2` b)
  

The profunctor representation of these optics is given by a polymorphic function type:

type TamRep ten act1 act2 s t a b = 
    forall p . (Tambara ten act1 act2 p) => p a b -> p s t
  

Such functions can be composed (optics, zoomed in) using simple function composition.

Proof of equivalence

To prove the equivalence of the two representation, we need some additional definitions.

Here’s the unit optic that uses the unitors:

unitOpt :: (Actegory ten act1, Actegory ten act2) 
  => Opt ten act1 act2 a b a b
unitOpt = Opt unit' unit
  

Since we are working with the oposite category, we define the flipped version of optics:

data FlipOpt ten act1 act2 a b s t 
   = FlipOpt (Opt ten act1 act2 s t a b)
  

FlipOpt is an instance of Tambara:

instance (Actegory ten act1, Actegory ten act2) 
  => Tambara ten act1 act2 (FlipOpt ten act1 act2 a b) where
    leftAct (FlipOpt (Opt l r)) = FlipOpt (Opt l' r') 
      -- take advantage of the Tambara structure on hom-sets
      -- l :: s -> m a, l' :: n s -> n m a
      -- r :: m b -> t, r' :: n m b -> n t
      where l' = assoc' . leftAct @ten @act1 @act1 @(->) l
            r' =          leftAct @ten @act2 @act2 @(->) r . assoc
  

I made the use of the Tambara action on hom-functors explicit through type annotations.

Here’s the mapping from optics to the Tambara representation:

toProRep :: (Actegory ten act1, Actegory ten act2) => 
  Opt ten act1 act2 s t a b -> TamRep ten act1 act2 s t a b
toProRep (Opt s_ma mb_t) pab = dimap s_ma mb_t (leftAct pab)
  

The opposite mapping uses the flipped unit optics. This is why we needed the proof that flipped optic is a Tambara module. As such, we can pass it to our function that is polymorphic in Tambara modules:

fromProRep ::  (Actegory ten act1, Actegory ten act2) => 
  TamRep ten act1 act2 s t a b -> Opt ten act1 act2 s t a b
fromProRep pab_pst = opt
  where FlipOpt opt = pab_pst (FlipOpt unitOpt)
  

Examples

By plugging in different monoidal categories and their actions, we can immediately generate Tambara representations for a variety of optics.

We can use the Tambara encoding for the lens:

type Lens s t a b = forall p . 
  Tambara (,) (,) (,) p => p a b -> p s t
  

Here’s the example of a prism:

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

and its Tambara representation:

type Prism' s t a b = forall p . 
  Tambara Either Either Either p => p a b -> p s t
  

Haskell code for this post is available here.

Two friends, Alice and Bob, live in the same city, but on the opposite sides of a wide river. Every night, Bob looks at the lights on the other side and tries to guess, which one belongs to Alice. They come up with a clever arrangement: Alice will turn on her lights for 10 minutes every night at 10 p.m. Every night Bob will take a long-exposure photo at the pre-arranged time. At the end of the year, Bob will superimpose all the photos, and hopefully the only bright spot will be Alice’s window. This is Tannakian reconstruction in a nutshell.

A functor produces a picture of one category inside another. It’s a potentially lossy encoding, but it always preserves the structure of the source. If there is a connection (morphism) between two objects in the source category, there will always be a connection between their images in the target category.

In general it’s impossible to recover the structure of the source category by looking at only one such picture. But if the target category has enough resolution, and we superimpose all available pictures, we can recover the morphisms of the source category.

Fiber functors

A category with just the right resolution is the category of sets. Therefore we’ll be looking at functors in (for historical reasons, these are called co-presheaves). Such a functor maps objects to sets, and morphisms to functions.

When dealing with functors, we usually imagine varying objects and morphisms while keeping the functor constant. Here, we are interested in using the totality of all functors while keeping the objects constant. To every object we will associate a mapping from functors to sets, simply by applying each functor to this object :

This mapping is functorial. Indeed, a natural transformation between and is a family of functions . We define the action of on a natural transformation by taking its component .

is called a fiber functor. You may think of it as probing an object and, through morphisms, its immediate neighborhood.

Tannakian reconstruction

To probe a hom-set we’ll be looking at the set of functions under all possible functors .

This set happens to be the set of natural transformations between two fiber functors and , a hom-set in the functor category:

A set of natural transformations can be written as an end:

An end is like a gigantic product. In our analogy, it correspond to the superposition of all photos. Like with any product, if any of its components is empty, the whole end is empty. Since the end goes over every possible functor, what prevents us from hand-picking a functor that’s non-empty at and empty at ? Such a single bad apple would spoil the whole batch (there is no function from a non-empty set to an empty set).

What makes this end non-trivial is functoriality. Any time there is a morphism , we automatically have a function , for any functor . In fact, because of the Yoneda embedding being full and faithful, we have as many such functions as there are morphisms in . We have the isomorphism:

By superimposing the images of all functors, we recover the original hom-set. This is the categorical version of Tannakian reconstruction.

We’ll use the double-Yoneda trick to prove it. First, we use the Yoneda lemma:

to explode the functors under the end:

We can now apply the Yoneda reduction to “integrate” over . The result is:

which, again by Yoneda, is equivalent to:

As an example, let’s apply Tannakian reconstruction to a simple one-object category. Such a category has a single hom set, which forms a monoid under composition. A set-valued functor maps the single object of to a set — a representation of this monoid. Natural transformations between such functors are called equivariant maps. Tannakian reconstruction lets us recover the monoid from the totality of its representations. Notice that naturality/equivariance is baked into the definition of an end.

I was originally attracted to category theory when trying to understand Haskell optics. I was puzzled by the van Laarhoven’s functor representations and Kmett’s use of Tambara modules. By playing Tetris with the Yoneda lemma I was able to make some progress, attacking more and more esoteric topics. With a group of researcher and students at the Oxford Adjoint School in Applied Category Theory we cracked the problem of traversal optics and published a paper summarizing the advances in profunctor optics.

Optics sit at an intersection of monoidal actions and Tambara modules. There is a duality between optics and Tambara representations. It is related to what mathematicians call Tannakian reconstruction, when an algebraic object is recovered from the totality of its representations.

No wonder then that a recent article by Mateusz Stroiński, Module categories, internal bimodules and Tambara modules, piqued my interest. It turns out that Tambara modules can be thought of as horizontal arrows in a double category, which is also a proarrow equipment. I will try to sketch the contents of this paper and illustrate it using Haskell code.

The slogan is that Tambara modules are to monoidal functors as profunctors are to functors.

The main advantage of the double-categorical setting for Tambara modules is that it works out of the box for enriched categories.

Monoidal functors redux

For simplicity, I’ll be using a simplified version of a strict monoidal functor, which omits the object constraint from the definition of a monoidal category:

class (Actegory ten act1, Actegory ten act2, Functor f) =>
  MonFunctor ten act1 act2 f where
    alpha  :: m `act2` f a -> f (m `act1` a)
    alpha' :: f (m `act1` a) -> m `act2` f a
    

Here, alpha' is the inverse of alpha.

Monoidal functors compose:

newtype MonFunCompose f g a = 
  MonFunCompose { getMonFunCompose :: f (g a) }
  

and the composition is again a monoidal functor:

instance ( Actegory ten act1
         , Actegory ten act2
         , Actegory ten act3
         , MonFunctor ten act2 act3 f
         , MonFunctor ten act1 act2 g) 
        => MonFunctor ten act1 act3 (MonFunCompose f g)
  where
    alpha mfga = 
        let m3fga' = second getMonFunCompose mfga
            fmga = alpha @ten @act2 @act3 m3fga'
            fgma = fmap (alpha @ten @act1 @act2) fmga
        in MonFunCompose fgma
    alpha' (MonFunCompose fgma) = 
        let fmga = fmap (alpha' @ten @act1 @act2) fgma
            mfga = alpha'  @ten @act2 @act3 fmga 
        in  second MonFunCompose mfga
  

Notice the use of type application to help the Haskell type checker.

Tambara modules

A Tambara module is a profunctor that is compatible with the action of a monoidal category. If you interpret a profunctor as a proof-relevant relation, a Tambara module has the property that, whenever two objects are related, they remain related when you “multiply” them by the same object . Multiplication in this case means the action of a monoidal category . In other words, a Tambara module is a profunctor equipped with the transformation:

that is natural in and , and dinatural in . The action interacts nicely with the monoidal structure:

(modulo some associators and unitors).

We can illustrate this in Haskell as a typeclass:

class (Actegory ten act, Profunctor j) 
  => Tambara ten act j where
    leftAct :: j a b -> j (m `act` a) (m `act` b)
      

I chose to concentrate on the left action of the actegory, but it’s easy to define the right action, or both. For simplicity, I’m using the same action for both arguments. In full generality, we would have two separate actegories.

The simplest example of a Tambara module is the hom-functor:

instance (Actegory ten act) => Tambara ten act (->) where
    leftAct :: Actegory ten act => (a -> b) -> m `act` a -> m `act` b
    leftAct = second
    

Here I used the bifunctoriality of the action.

Tambara modules form a category, in which action-preserving natural transformations act as morphisms.

The usual profunctor composition using coends also works on Tambara modules.

data TamCompose p q d c where
  TamCompose :: p x c -> q d x -> TamCompose p q d c
  

The result of composition is again a Tambara module:

instance (Tambara ten act p, Tambara ten act q) 
  => Tambara ten act (TamCompose p q) where
    leftAct :: (Tambara ten act p, Tambara ten act q) =>
        TamCompose p q a b -> TamCompose p q (m `act` a) (m `act` b)
    leftAct (TamCompose pxc qdx) 
      = TamCompose (leftAct pxc) (leftAct qdx)
    

Taken together, we have a bicategory , where actegories are 0-cells, Tambara modules with coend composition are 1-cells, and natural transformations between them are 2-cells.

Moreover, endo-Tambara modules, that is Tambara modules that operate within a single category, form a monoidal bicategory, with profunctor composition acting as a tensor product and a hom-functor acting as a unit.

Tambara Equipment

We have previously studied a double category in which categories are 0-cells, profunctors are horizontal arrows, functors are vertical arrows, and natural transformations form 2-cells. This double category happens to be a proarrow equipment, which relates functors to representable profunctors in a specific way.

It turns out that there is an analogous construction with actegories as 0-cells, Tambara modules as horizontal 1-cells, and monoidal functors as vertical 1-cells. To form 2-cells, we first have to be able to lift (or restrict) a Tambara module along a pair of monoidal functors. We define a lifting of as the profunctor:

or, using placeholders, . In Haskell this is:

newtype Lift f g j a c = Lift (j (f a) (g c))
  

The lifting of a Tambara module is again a Tambara module with the structure map defined as a composition:

The second arrow lifts the (invertible) monoidal functor structure map to :

Here’s the same thing in Haskell:

instance ( Actegory ten act1
         , Actegory ten act2
         , MonFunctor ten act1 act2 f
         , MonFunctor ten act1 act2 g
         , Tambara ten act2 j) 
    => Tambara ten act1 (Lift f g j) where
    leftAct (Lift j) = Lift $ dimap alpha' alpha $ leftAct @ten @act2 j
    

I used type applications to select the correct left action corresponding to act2.

A 2-cell is then a natural transformation from to the lifting of .

Or, in Haskell:

type Cell f g h j = forall a c . h a c -> j (f a) (g c)
  

The companion and the conjoint are representable profunctors, that are automatically Tambara modules as long as f is a monoidal functor (the Identity functor is trivially monoidal):

type Companion f d c = Lift f Identity (->)
type Conjoint f d c  = Lift Identity f (->)
  

The unit and counit cells for the companion and the conjoint are reasonably easy to define (see the linked code).

Free Tambara and Optics

There is an obvious forgetful functor from to (it forgets the action). This functor has a left adjoint. For any profunctor , it produces a free Tambara module given by the following coend:

In Haskell, we model it as an existential data type:

data FreeTamb ten act j s t = 
  forall m x y. (MonoidalCategory ten, Actegory ten act) 
  => FreeTamb (s -> m `act` x) (j x y) (m `act` y -> t)
  

The result is indeed a Tambara module:

instance (Actegory ten act, MonoidalCategory ten, Profunctor j) 
  => Tambara ten act (FreeTamb ten act j) where
    -- na -> (nm)c, jcd, (nm)d -> nb
    leftAct (FreeTamb a_mc jcd md_b) = FreeTamb f jcd g
      where
        --f :: n `act` a -> (n `ten` m) `act` c
        f  na = assoc' $ second a_mc na
        --g :: (n `ten` m) `act` d -> n `act` b
        g nm_d= second md_b $ assoc nm_d
  

It so happens that optics can be defined as a free Tambara module acting on a representable profunctor . Indeed, applying the Yoneda reduction, we get:

In Haskell

data Rep a b x y = Rep (x -> a) (b -> y)
  

giving us:

type Optic ten s t a b = FreeTamb ten (Rep a b) s t 
  

which, by Yoneda reduction, is isomorphic to:

data Optic ten act s t a b = forall m.
    Optic (s -> m `act` a) (m `act` b -> t)
    

Internalizing monoidal actions

A monoidal action, seen as a functor , can be internalized in if it has a right adjoint:

If you think of the action as “multiplication,” the adjunction is reminiscent of currying, and the right adjoint plays to role on the “internal hom.”

In Haskell, we define a typeclass:

class (Actegory ten act, MonoidalCategory ten, Profunctor hom) 
  => IntHom ten act hom | hom -> act where
    icurry   :: (m `act` a -> b) -> (m -> hom a b)
    iuncurry :: (m -> hom a b)   -> (m `act` a -> b)
  

We can use this adjunction to simplify multiplicative optics:

Using the Yoneda reduction (a.k.a, “integrating” over ), this is equivalent to:

With additive optics, we use the right adjoint to coproduct to produce hom-sets in a product category.

Both tricks are used in simplifying traversals, which are optics generated by polynomial functors:

Here, is a natural-number-indexed family of objects with a monoidal structure given by convolution; and and are powers.

We first use the coproduct adjunction:

and follow it by the currying adjunction. We get the formula for a traversal:

The result can be illustrated in Haskell by replacing powers with lists:

type Traversal s t a b = s -> ([b] -> t, [a])
  

Internal monoid

The endo-hom is automatically a monoid in . Indeed, we can define monoid multiplication as:

The right hand side can be implemented as a double application of the counit of the adjunction:

In Haskell, we first define a monoid internal to a monoidal category:

class (MonoidalCategory ten) => IMonoid ten m where
    imempty  :: Unit ten -> m
    imappend :: m `ten` m -> m
    

and show that hom a a is an instance of it:

instance (Actegory ten act, MonoidalCategory ten, IntHom ten act hom)  
  => IMonoid ten (hom a a) where
    imempty = icurry unit
    -- imappend :: (hom a a) `ten` (hom a a) -> hom a a
    imappend = icurry (eval . second eval . assoc)
  

where counit of the adjunction is the eval function:

eval :: (Actegory ten act, MonoidalCategory ten, IntHom ten act hom) 
  => hom a b `act` a -> b
eval = iuncurry id
  

Haskell code for this blog post is available here.