June 2026

Monthly Archive

June 30, 2026

Actegories

Posted by Bartosz Milewski under Category Theory, Haskell | Tags: , , , , |
Leave a Comment 

Previously: Kan Extensions in Double Categories.

In programming, actegories play a central role in optics: lenses, prisms, traversals, etc. To understand actegories, let’s start with the definition of a monoidal category.

Monoidal Category

A monoidal category \mathbf M is a category equipped with a tensor product. A tensor product is a functor \otimes \colon \mathbf M \times \mathbf M \to \mathbf M. We assume that this product is associative and unital– up to isomorphism. It means that there is an invertible associator:

\alpha_{a, b, c} \colon (a \otimes b) \otimes c \to a \otimes (b \otimes c)

natural in all three arguments. We also have a unit object 1 and two (invertible, natural) unitors:

\lambda_a \colon 1 \otimes a \to a

\rho_a \colon a \otimes 1 \to a

To get a better feel for it, we can try to model a monoidal category in Haskell. We parameterize it by the type of the tensor product, ten, which we want to be a Bifunctor:

class (Bifunctor ten) => MonoidalCategory ten where ...

The standard way to define a subcategory of Hask is to restrict the types of objects by imposing a constraint. Such a restriction has a special kind, Constraint:

class Bifunctor ten
  => MonoidalCategory (obj :: Type -> Constraint) ten where ...

A common example of such a constraint is a typeclass. For instance Monoid will restrict the objects of the category to be monoids. (In principle, we should also restrict the type of arrows, here to monoid morphisms.)

We can specify the unit of a monoidal category as an associated type (parameterized by ten):

    type Unit ten :: Type

The unit should be an object of the category, so it should satisfy the constraint. We can encode this in our definition as a precondition: obj (Unit ten). This leads to a circularity, which we can overcome using the language pragma UndecidableSuperClasses:

class (Bifunctor ten , obj (Unit ten))
  => MonoidalCategory (obj :: Type -> Constraint) ten where
    type Unit ten :: Type
    ...

Finally, we can add the associator and the unitors (and their inverses):

class (Bifunctor ten , obj (Unit ten))
  => MonoidalCategory (obj :: Type -> Constraint) ten where
    type Unit ten :: Type
    alpha  :: (obj a, obj b, obj c) =>  (a `ten` b) `ten` c -> a `ten` (b `ten` c)
    lambda :: (obj a) => (Unit ten) `ten` a -> a
    ...

Notice the obj constraints in the type of these functions and the infix notation for the tensor.

Let’s work out a few examples. The simplest is the category of all types with a cartesian product as tensor. 

instance MonoidalCategory Hask (,) where
    type Unit (,) = ()
    alpha ((a, b), c) = (a, (b, c))
    lambda ((), a) = a
    ...

We define Hask using an empty class, and we make all objects its instances:

class Hask a
instance Hask a

Similarly, we can define a monoidal category with Either as the tensor product, or with Monoid as the object constraint.

Actegory

An actegory is a category that supports the action of a monoidal category. You may think of it as “multiplying” or “scaling” the objects of this category by objects of the monoidal category. The (left) action can be defined as a functor from the product category to C:

\triangleright \colon \mathbf M \times C \to C

or, after currying, as a functor from \mathbf M to the endofunctor category:

\triangleright \colon \mathbf M \to [C, C]

The coherency conditions are the invertible natural transformations that relate the action \triangleright to the tensor product \otimes and its unit 1:

\alpha_{m n a} \colon (m \otimes n) \triangleright a \to m \triangleright (n \triangleright a)

\lambda_{a} \colon 1 \triangleright a \to a

The action is functorial in both arguments, so our Haskell translation pegs it, for simplicity, as a Bifunctor. (A Profunctor action is also possible. Categorically, it would correspond to using \mathbf M^{op} as the monoidal category.)

class (MonoidalCategory obj ten, Bifunctor act) 
  => Actegory obj ten act | act -> ten where
    assoc  :: (obj m, obj n) 
           => (m `ten` n) `act` a -> m `act` (n `act` a)
    assoc' :: (obj m, obj n)
           => m `act` (n `act` a) -> (m `ten` n) `act` a
    unit   :: Unit ten `act` a -> a
    unit'  :: a -> Unit ten `act` a

Another simplifying assumption is that the action uniquely identifies the tensor product, encoded here as the functional dependency act -> ten.

The simplest example of an actegory is the self action of the cartesian product. Here, the monoidal category acts on itself:

instance Actegory Hask (,) (,) where
    assoc ((m, n), a) = (m, (n, a))
    assoc' (m, (n, a)) = ((m, n), a)
    unit ((), a) = a
    unit' a = ((), a)

Monoidal Functors

Actegories that use the same monoidal category for their actions form a category. The morphisms in this category are (strict) monoidal functors. These are functors that map one action to another:

f (m \triangleright_1 a) \cong m \triangleright _2 f a

In Haskell, we can model them as:

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

In fact, actegories form a bicategory, with action-preserving natural transformations acting between monoidal functors.

Here’s an interesting example of a monoidal functor between non-trivial actegories:

instance (Traversable f) => MonFunctor Monoid (,) (,) (,) f where
    as (m, fa) = fmap (m, ) fa
    as' = sequenceA

Haskell code is available here.

 

June 13, 2026

Kan Extensions in Double Categories

Posted by Bartosz Milewski under Category Theory, Double category, Haskell, Kan extensions, Profunctor Equipment | Tags: , , |
Leave a Comment 

Previously: Kan extensions in Haskell.

In a double category that is also a proarrow equipment, we have the ability to bend arrows. In particular, in the definition of the counit of the right Kan extension:

we can bend the vertical j arrow, replacing it with its horizontal conjoint B(1, j). In a profunctor equipment, this is just a representable profunctor \langle b, a\rangle \mapsto B(b, j a).

A natural generalization is to replace this representable with a general profunctor. This way we get a definition of a right Kan extension along a profunctor J.

In a more general setting of a double category, the counit of the right Kan extension is a 2-cell:

The universal condition can be similarly generalized by bending the j arrows.

However, the universal condition for pointwise right Kan extensions is stronger. It involves an additional horizontal 1-cell H. It states that any 2-cell \phi of the shape below can be uniquely factorized through the counit \epsilon:

Right Kan extensions in Haskell

In Haskell, the right Kan extension of a functor d along a profunctor j can be written as a data type:

newtype Ran j d a = Ran (forall x . j a x -> d x)

This is a direct translation of the categorical formula that uses an end:

(\text{Ran}_J d) \, a = \int_x \text{Set}(J a x, d \, x)

Compare this with the earlier implementation of the Kan extension, in which j was a functor:

newtype Ran j d a = Ran (forall x . (a -> j x) -> d x)

The counit is a 2-cell from j to the identity profunctor (->):

epsilon :: (Profunctor j, Functor d) => 
  Cell (Ran j d) d j (->)
epsilon jab (Ran ran) = ran jab

The 2-cell Phi goes from the profunctor composition of j and h to the identity profunctor:

type Phi s d j h  = Cell s d (Procompose j h) (->)

The factorization cell Phi' goes from h to identity:

type Phi' s d j h = Cell s (Ran j d) h (->)

For any Phi, we can find the corresponding Phi':

rightAdj :: (Profunctor j, Profunctor h, Functor d, Functor s) =>
        Phi s d j h -> Phi' s d j h
rightAdj phi hac sa = Ran (\ jcb -> phi (Procompose jcb hac) sa)

This function replaces the right adjoint used in the traditional definition of a Kan extension.

The result satisfies the factorization property:

factor :: (Profunctor j, Profunctor h, Functor d, Functor s) => 
  Phi s d j h -> Phi s d j h
factor phi = funComp . vcomp (rightAdj phi) epsilon

Here vcomp is the vertical composition of 2-cells:

vcomp :: (Functor f, Functor g, Functor h
         , Profunctor p, Profunctor q, Profunctor r, Profunctor s) =>
  Cell f g p r -> Cell g h q s 
  -> Cell f h (Procompose q p) (Procompose s r)
vcomp fg_pr gh_qs (Procompose qxc pax) 
    = Procompose (gh_qs qxc) (fg_pr pax)

and funComp is hom-functor composition:

funComp :: Procompose (->) (->) a b -> (a -> b)
funComp (Procompose f g) = f . g

The computational meaning of the universal construction is that, in order to define a 2-cell (natural transformation) from some functor s to Ran j d along a profunctor h, it’s enough to provide a 2-cell from s to d along a composite Procompose j h.

Left Kan extensions

We can apply similar generalization to left Kan extensions. This time we start with the unit given by the 2-cell:

The universal condition that defines the pointwise left Kan extension of a vertical 1-cell d along a horizontal 1-cell J is given by the following unique factorization:

Left Kan extensions in Haskell

In Haskell, we define the left Kan extension along a profunctor as an existential data type:

data Lan j d a where
    Lan :: j x a -> d x -> Lan j d a

This is a direct translation of the coend formula:

(\text{Lan}_J d)\, a = \int^x ( J x a \times d \,x)

The unit is a 2-cell:

eta :: (Profunctor j, Functor d) => Cell d (Lan j d) j (->)
eta jab da = Lan jab da

The universal condition states that, for any 2-cell:

type Phi s d j h  = Cell d s (Procompose h j) (->)

there is a unique 2-cell:

type Phi' s d j h = Cell (Lan j d) s h (->)

given by the mapping:

leftAdj :: (Profunctor j, Profunctor h, Functor d, Functor s) =>
        Phi s d j h -> Phi' s d j h
leftAdj phi hac (Lan jxa dx) = phi (Procompose hac jxa) dx

that uniquely factorizes through the unit eta:

factor :: (Profunctor j, Profunctor h, Functor d, Functor s) =>
    Phi s d j h -> Phi s d j h
factor phi = funComp . vcomp eta (leftAdj phi)

Again, computationally, this defines a mapping-out property of the left Kan extension.

Complete Haskell code is available here: left Kan extensions, right Kan extensions.

 

June 8, 2026

Kan Extensions in Haskell

Posted by Bartosz Milewski under Category Theory, Haskell, Programming | Tags: , , , |
1 Comment 

Previously: Tabulation Tribulations.

If you think of functor composition as a form of multiplication, Kan extensions are an attempt to construct inverses of this multiplication. But unlike multiplication, composition is not symmetric, so we have extensions that attempt to undo precomposition, and lifts that do the same for postcomposition. Furthermore, there rarely is a single inverse to any form of composition, so we have the parsimonious right extensions and lifts, and the generous left extensions and lifts. We end up with four combinations that correspond to four different adjunctions:

(- \circ j) \dashv \text{Ran}_j -

\text{Lan}_j - \dashv (- \circ j )

(j \circ -) \dashv \text{Rift}_j -

\text{Lift}_j - \dashv (j \circ -)

We’ll concentrate on the extensions, since we can provide explicit point-wise formulas for them in cases that are of interest to us, that is in \mathbf{Cat} and in \mathbb{P}rof.

Right Kan extensions

The definition of the right Kan extension relates the mapping out of the composition to the mapping into \text{Ran}. In Haskell, we can define them as two types:

type Phi  j s d = Compose s j ~> d
type Phi' j s d = s ~> Ran j d

The wavy arrows denote natural transformations:

type f ~> g = forall x. f x -> g x

To show that there is an adjunction we can either prove the (natural) isomorphism between Phi and Phi', or implement the unit and counit of the adjunction (together with zigzag identities):

eta     :: (Functor j, Functor d) => d ~> Ran j (Compose d j)
epsilon :: (Functor j, Functor d) => Compose (Ran j d) j ~> d

In Haskell we can implement the right Kan extension as:

newtype Ran j d a = Ran (forall x . (a -> j x) -> d x)

This is a straightforward translation of the categorical formula that uses an end:

(\text{Ran}_j d) \,a = \int_x \text{Set}(C(a, j \,x), d \, x)

The adjunction can then be implemented as a pair of mappings:

leftAdj :: (Functor j, Functor d, Functor s) =>
   Phi j s d -> Phi' j s d
leftAdj phi sx = Ran (\x_jx -> phi (Compose (fmap x_jx sx)))
rightAdj ::  (Functor j, Functor d, Functor s) =>
   Phi' j s d -> Phi j s d
rightAdj phi' (Compose sj) = 
    let (Ran ran) = phi' sj
    in ran id

Or as the unit/counit pair:

eta :: (Functor j, Functor d) => d ~> Ran j (Compose d j)
eta dx = Ran (\x_jx -> Compose (fmap x_jx dx))
epsilon :: (Functor j, Functor d) => Compose (Ran j d) j ~> d
epsilon (Compose (Ran ran)) = ran id

Universal arrows

There is a third way, which gives a better starting point for generalizations. It can be used on an object-by-object basis, even if there is no global adjunction. It’s based on the idea of the universal arrow.

A universal arrow is a terminal object in the comma category. For a given functor L \colon D \to C, the comma category L/c consists of pairs (d, f \colon L d \to c). In other words, it’s a category of arrows from the image of L to some fixed object c \in C. Morphisms in the comma category are arrows h: d \to d' in D that make the corresponding triangles in C commute:

A terminal object in L/c is a pair (t, \tau) , through which every arrow \Phi \colon L d \to c factorizes uniquely. That means, there is a unique arrow h \colon d \to t that makes the following triangle commute:

If there is an adjunction L \dashv R, then we can easily construct the universal arrow as a pair (R c, \epsilon_c), where \epsilon_c is a component of the counit of the adjunction. Indeed, every \Phi \colon L d \to c factorizes through \epsilon_c:

\Phi = \epsilon_c \circ L \Phi'

where \Phi' = \text{leftAdj}\, \Phi.

The advantage of the universal arrow approach is that it’s pointwise. We can do it for each object c separately.

Reversing this process, rather than building an adjuncion, we can directly construct a universal arrow. We start by defining of a component of a counit. Then we postulate that any other counit-like mapping factorizes uniquely throught that counit.

Let’s see how it works for our definition of the right Kan extension. The counit has the following signature:

epsilon :: (Functor j, Functor d) => Compose (Ran j d) j ~> d

We can illustrate it with the following string diagram:

In general, the functors go between three different categories: A, B, and M. In Haskell we have just one category and three endofunctors.

Any other mapping of this form has the signature (replacing Ran j d with an arbitrary functor s):

type Phi j s d = Compose s j ~> d

Or, as a string diagram:

We postulate that, for every Phi, there is a unique Phi' that factorizes it through epsilon. That is, we have a function:

leftAdj :: (Functor j, Functor d, Functor s) =>
   Phi j s d -> Phi' j s d

such that:

factor :: (Functor j, Functor d, Functor s) => Phi j s d -> Phi j s d
factor phi = epsilon . Compose . leftAdj phi . getCompose

Modulo newtype shenanigans, this is exactly \epsilon \circ (L_j \Phi'), where L_j s = s \circ j is functor precomposition. Or as a string diagram:

Notice that rightAdj doesn’t appear anywhere in this construction.

The computational interpretation of this universal construction lets us calculate a mapping into a right Kan extension. Namely, to determine a natural transformation from some functor s to Ran j d, it’s enough to provide a mapping phi from Compose s j to d.

Left Kan extensions

We can now apply the same idea to the left Kan extension. This time we start with the unit:

eta :: (Functor j, Functor d) => d ~> Compose (Lan j d) j

We postulate that for any other mapping of this form (replacing Lan j d with and arbitrary s):

type Phi j s d = d ~> Compose s j

there is a unique Phi':

type Phi' j s d = Lan j d ~> s

that factorizes it through eta:

factor :: (Functor j, Functor d, Functor s) => Phi j s d -> Phi j s d
factor phi = Compose . rightAdj phi . getCompose . eta

In Haskell, the left Kan extension is given by the existential data type:

data Lan j d a where
    Lan :: (j x -> a) -> d x -> Lan j d a

In category theory, this formula uses a coend:

(\text{Lan}_j d) \, a = \int^x C(j \, x, a) \times d \, x

Indeed, for any given Phi, we can obtain a Phi' by applying this function:

rightAdj :: (Functor j, Functor d, Functor s) =>
   Phi j s d -> Phi' j s d
rightAdj d_sj (Lan jx_a dx) = 
    let Compose sjx = d_sj dx
    in fmap jx_a sjx

The result factorizes Phi through eta:

factor :: (Functor j, Functor d, Functor s) => Phi j s d -> Phi j s d
factor phi = Compose . rightAdj phi . getCompose . eta

The computational interpretation of this universal construction let us calculate a mapping out of the left Kan extension.

See Haskell code for right and left Kan extensions.

Next, we’ll generalize these construction to a double category setting.