Constructing Lists from Vectors: Kan Extensions of Graded Monads

---

Vectors and Lists

When considering data structures that arrange elements, we sometimes distinguish between them as follows:

• Vectors have a length determined in advance (at the type level).
• Lists can take any arbitrary length.

Representing this with Haskell types:

data Vector n a = ...

data [] a = [] | a : [a]

In this way, Vector takes a length n as a type argument, whereas a list does not hold length information at the type level and is defined as a recursive type.

Lists are well known to have a monadic structure, but what about vectors?

Actually, it is possible to give a monadic structure to vectors as well.

join :: Vector n (Vector n a) -> Vector n a

If we consider a function that takes the elements along the "diagonal" as join, we can indeed create a monad.

However, this implementation treats Vector n a as Finite n -> a—that is, a "function" that returns an element when given an index up to n—making it a monad (behaving the same as the Reader monad), which has slightly different properties than the behavior of the List monad.

If we try to think of an implementation that corresponds to the behavior of the List monad:

join' :: Vector n (Vector m a) -> Vector (n * m) a

We might want to consider such a function, but it's not straightforward because we need to account for the manipulation of extra type variables like n and m, which aren't part of a simple monad.

In fact, a vector can be made into an instance of a graded monad^[1], which is a slight extension of a regular monad^[2].

class GradedMonad (m :: k -> Type -> Type) where
  type Unit m :: k
  type Plus m (i :: k) (j :: k) :: k
  type Inv  m (i :: k) (j :: k) :: Constraint

  pure' :: a -> m (Unit m) a
  bind' :: Inv m i j => m i a -> (a -> m j b) -> m (Plus m i j) b

The kind of the type that becomes an instance of GradedMonad is k -> Type -> Type, which has one more type argument compared to the kind Type -> Type of types that become regular monads. GradedMonad expects this new type argument to have a monoid structure at the type level, where:

• Unit m corresponds to the identity element.
• Plus m i j corresponds to the binary operation of the monoid.

pure' and bind' are functions corresponding to pure and >>= in regular monads.

pure' is a function that wraps a value of any type a into the type m (Unit m) a, which is a functor m (Unit m) corresponding to the monoid's identity element.

Also, bind' is a function that behaves similarly to the monad's

(>>=) :: m a -> (a -> m b) -> m b

for i and j that satisfy the constraints given by Inv m. At this time, the type arguments i and j of kind k are mapped to Plus m i j by the monoid's binary operation.

Let's actually make Vector an instance of GradedMonad.

import qualified Data.Vector.Sized as V

instance GradedMonad Vector where
  type Unit Vector = 1
  type Plus Vector m n = m * n
  type Inv  Vector m n = ()

  pure' = V.singleton
  bind' = flip V.concatMap

singleton and concatMap are functions provided by vector-sized and have the following types:

singleton :: a -> Vector 1 a
concatMap :: (a -> Vector m b) -> Vector n a -> Vector (n * m) b

Graded Monads

Now, let's talk about something more abstract.

A graded monad is a lax monoidal functor from a monoidal category $({\mathscr M}, \otimes, I)$ to the monoidal category of endofunctors $([{\mathscr C}, {\mathscr C}], \circ, {\rm id}_{\mathscr C})$^[3].

Let's assume the concept of monoidal categories is known (Monoidal category - Wikipedia).
To understand lax monoidal functors, first recall the definition of a functor $F$.

A functor $F$ maps objects and morphisms of a category ${\mathscr C}$ to objects and morphisms of a category ${\mathscr D}$ such that it preserves identity morphisms and the composition of morphisms.

Now, if we consider two monoidal categories $({\mathscr C}, \otimes_{\mathscr C}, 1_{\mathscr C})$ and $({\mathscr D}, \otimes_{\mathscr D}, 1_{\mathscr D})$, we can think of a regular functor that also preserves the structure of the monoidal categories. Such a functor maps the unit object to the unit object and preserves the tensor product (it also needs to be compatible with associators and unitors).

$$\begin{matrix} 1_{\mathscr D} &=& F(1_{\mathscr C}) \\ F(x)\otimes_{\mathscr D}F(y) &=& F(x \otimes_{\mathscr C} y) \end{matrix}$$

Such a functor is called a strict monoidal functor.

A "lax monoidal functor" is one where these conditions joined by equality are "relaxed" to simply requiring the existence of a morphism. That is, we assume the existence of a morphism $\epsilon$ and a natural transformation $\mu$ as follows (again, they must be compatible with associators and unitors):

$$\begin{matrix} \epsilon&:& 1_{\mathscr D} &\rightarrow& F(1_{\mathscr C}) \\ \mu_{x, y}&:& F(x)\otimes_{\mathscr D}F(y) &\rightarrow& F(x \otimes_{\mathscr C} y) \end{matrix}$$

Now that we know what a lax monoidal functor is, let's consider $\epsilon$ and $\mu$ in the context of a lax monoidal functor from a monoidal category $({\mathscr M}, \otimes, I)$ to the monoidal category of endofunctors $([{\mathscr C}, {\mathscr C}], \circ, {\rm id}_{\mathscr C})$.

$$\begin{matrix} \epsilon&:& {\rm id}_{\mathscr C} &\rightarrow& F(I) \\ \mu_{i, j}&:& F(i)\circ F(j) &\rightarrow& F(i \otimes j) \end{matrix}$$

These are a natural transformation from the identity functor to $F(I)$ and a natural transformation from $F(i)\circ F(j)$ (note that $\circ$ is functor composition) to $F(i \otimes j)$. Writing these as Haskell types:

pure' :: a -> m (Unit m) a
join' :: m i (m j a) -> m (Plus i j) a

We can see that these correspond to the implementation of GradedMonad.

In fact, a regular monad can also be viewed as a graded monad. Now, if we consider the discrete category ${\mathbb 1}$ consisting of only a single object as a trivial monoidal category, a lax monoidal functor to the monoidal category of endofunctors $([{\mathscr C}, {\mathscr C}], \circ, {\rm id}_{\mathscr C})$ maps the unique object in ${\mathbb 1}$ to an endofunctor that becomes a monad (where compatibility with associators and unitors corresponds to monad laws).

By the way, if there is a graded monad as a functor $H$ from a monoidal category ${\mathscr M}$ to the category of endofunctors $[{\mathscr C}, {\mathscr C}]$, and a monad can be thought of as a functor $L$ from a monoidal category ${\mathbb 1}$ to the category of endofunctors $[{\mathscr C}, {\mathscr C}]$, wouldn't you want to know if the monad $L$ can be obtained as a left Kan extension of the graded monad $H$?

In particular, since we are now considering a graded monad called a vector and a monad called a list, it would be very interesting if a list could be obtained as a Kan extension of a vector.

From Vector to List

Let's actually implement this in Haskell and verify it. In Haskell, we can define a left Kan extension using coends as follows:

data Lan g h a where
  Lan :: (g b -> a) -> h b -> Lan g h a

Lan g h a is the left Kan extension of h along g. The key point is that b is hidden as an existential type. This implementation is provided by the library kan-extensions.

Let's use this to define a list as a Kan extension of a vector.

newtype Flip f a b = Flip { runFlip :: f b a }

newtype List a = List { getList :: Lan (Const ()) (Flip Vector a) () }

Flip is a type for swapping the order of type arguments of Vector. List a is defined as the left Kan extension of Flip Vector a along Const ().

Let's confirm that List a defined in this way is actually isomorphic to [a].

-- | Helper function to treat a vector as a list
fromVector :: Vector n a -> List a
fromVector v = List (Lan (const ()) (Flip v))

toList :: List a -> [a]
toList (List (Lan _ (Flip v))) = V.toList v

fromList :: [a] -> List a
fromList xs = V.withSizedList xs (\v -> fromVector v)

These functions show that List a can be converted back and forth with a regular list without losing any information.

In fact, looking closely at the type of List a and transforming it:

Lan (Const ()) (Flip Vector a) ()

<=> {- From the definitions of Lan and Flip -}

exists n. (Const () n -> (), Vector n a)

<=> {- From Const () n <=> (), () -> () <=> (), ((), A) <=> A -}

exists n. Vector n a

This simply represents that a list is a vector with some length. Note that exists n. denotes that n is an existential type (though this notation doesn't directly exist in Haskell syntax).

Now, so far we've seen that the Kan extension of a vector becomes a list as a data structure. From here, let's see to what extent we can restore the properties of the list monad from the graded monad properties of the vector through this construction.

First, the Functor and Applicative instances can be implemented as follows:

instance Functor List where
  fmap f (List (Lan _ (Flip v))) = fromVector $ fmap f v

instance Applicative List where
  pure a = fromVector $ pure' a
  (List (Lan _ (Flip vf))) <*> (List (Lan _ (Flip va))) =
    fromVector $ vf `bind'` \f -> fmap f va

Interestingly, the implementations of Functor and Applicative are automatically obtained from the GradedMonad implementation (this isn't limited just to vectors). Running this shows it behaves as expected.

> toList $ fmap (+1) $ fromList [1,2,3]
[2,3,4]

> toList $ (fromList [(+1), (*2)]) <*> (fromList [1,2])
[2,3,2,4]

Finally, let's implement the monad. However, as you'll see after a little trial, this is not straightforward. In general, even if a Kan extension of a graded monad exists, it is not necessarily a graded monad itself. "A Criterion for Kan Extensions of Lax Monoidal Functors" describes a sufficient condition (Theorem 2.1) for a graded monad (along a strong monoidal functor) to again be a graded monad. Translating this condition to our vector and list example roughly requires that an isomorphism exists between:

List (List a) and Lan (Const ()) (\(n, m) -> Vector n (Vector m a)) ()

(Please bear with me as some parts haven't been fully translated into Haskell syntax). This condition is very strong, as it requires that the value of List (List a) can be represented by some $n \times m$ two-dimensional array, and it does not hold in general. Here, let's assume the existence of a weaker function, in the sense that if this condition holds, then the following holds:

joinL :: List (List a) -> List a
joinL = fromList . concatMap toList . toList

I've pretty much assumed the existence of exactly what I wanted 😅. However, this is just an assumption that the value of List (List a) can be represented by a vector of some length, so it is weaker than the previous condition. Using this, we can successfully implement the monad:

instance Monad List where
  m >>= k = joinL $ fmap k m

And there we have it! 👏

Afterword

I learned about this topic while reading graded monad in nLab: 3. Uses. I wasn't sure how much could be reproduced in Haskell, but I'm relieved it went better than expected. We successfully obtained an implementation of the list monad as a left Kan extension of a vector viewed as a graded monad. In the end, I had to assume the existence of a strong function only for the monad implementation, but perhaps a looser condition might suffice (if you know one, please let me know privately). Using the same construction as this time, there might be other well-known Haskell data types that can be implemented as a Lan of a GradedMonad. It's exciting to discover deep relationships between data structures.

Finally, special thanks to ryota-ka for staying up until "2 AM" to discuss this for the sake of this article 🙏

---

＼Thank you for reading!／
If you found this article interesting, I would be happy to receive a Like ♡ ☺️
If you send me a badge, it will encourage me to write the next article! 🙌

脚注

1. The name "graded" comes from graded rings.
   Fujii, Soichiro, Shin-ya Katsumata, and Paul-André Melliès. "Towards a formal theory of graded monads." International Conference on Foundations of Software Science and Computation Structures. Springer, Berlin, Heidelberg, 2016.

2. The implementation here is based on Dominic Orchard, Tomas Petricek, Embedding effect systems in Haskell, (pdf).

3. Is there a problem?