Izaak Meckler

String diagrams, traversables, and positive braids

Posted on July 18, 2015

Today I want to describe some kind of possible connection between what in Haskell-land are called traversable functors and "positive braids. I really don't have many answers here, so I'd say the primary purpose of this post is to explain an observation and then invite comment from others.

Natural Transformations

Throughout this post I'll talk about natural transformations. If you're a mathematician, just think of it as a natural transformation. If you're a Haskeller, think of a natural transformation from a(n) (endo)functor \(F\) to a functor \(G\) as a polymorphic function of type \(\texttt{forall a. F a -> G a}\).

String diagrams

Skip to the next section if you know what string diagrams are.

Given a collection of natural transformations \(\eta_1, \eta_2, \cdots\), there are a bunch of other natural transformations we can define. Namely, we can

  • compose natural transformations whose types match up, and
  • given \(\varphi : S \to T\), for any functor \(F\) we can define both
    • \(F\varphi : FS \to FT\) (written \(\texttt{fmap}\; \varphi\)) for a Haskeller) and
    • \(\varphi F : SF \to TF\) (this is just the restriction of \(\varphi \texttt{ :: forall a. S a -> T a}\) to the type \(\texttt{forall a. S (F a) -> T (F a)}\)).

(where juxtaposition of functors denotes composition). We thus obtain a set of terms inductively defined out of the base set of \(\eta_i\).

Some equations automatically hold between terms built up in this way. The basic equations are that

  • for any \(\varphi : A \to B\), \(\epsilon : C \to D\), we have \(B\epsilon \circ \varphi C = \varphi D \circ A\epsilon\) by naturality
  • for any \(F, \varphi : A \to B, \epsilon : B \to C\), by functoriality \(F(\epsilon \circ \varphi) = F\epsilon \circ F\varphi\)
  • for any \(F, \varphi : A \to B, \epsilon : B \to C\), \((\epsilon \circ \varphi)F = \epsilon F \circ \varphi F\) which is clearly true since these are just restrictions.

Thinking about which terms built up out of functor-mapping and composition are equal is a bit annoying because its not always clear how to apply these equations to check. String diagrams solve this problem. They are an alternative notation for describing natural transformations built out over some base set, but one in which the naturality equations hold automatically so that recognizing when things are equal is a lot easier.

A string diagram is essentially a directed graph with edges labeled by functors and vertices labeled by natural transformations, along with an embedding in the plane (up to isotopy) in which all edges travel downward from source vertex to target vertex.

To really understand string diagrams, let's see how we can translate terms as described above into string diagrams (by "pattern matching" on the term). This will essentially explain the meaning of string diagrams.

  • A basic \(\eta_i : S_{i,1} \cdots S_{i,n} \to T_{i,1} \cdots T_{i,m}\) gets sent to the string diagram
  • If the types of \(\varphi\) and \(\epsilon\) match up so we can compose them, and if and are the string diagrams corresponding to \(\varphi\) and \(\epsilon\) respectively, then is the string diagram corresponding to \(\epsilon \circ \varphi\).
  • If \(\varphi\) has corresponding string diagram as above, then is the string diagram corresponding to \(F\varphi\).
  • If \(\varphi\) has corresponding string diagram as above, then is the string diagram corresponding to \(\varphi F\).

Let's see why naturality holds automatically. Remember that naturality says that for any \(\varphi : A \to B\), \(\epsilon : C \to D\), we have \(B\epsilon \circ \varphi C = \varphi D \circ A\epsilon\). Using our translation into string diagrams, the left side has string diagram while the right side is But these are equal since we can smoothly smush around the picture on the left to get the picture on the right. The other equations (functoriality and the fact that restriction respects composition are even more obviously true on-the-nose for string diagrams).

Braids

What I'll call braid diagrams are a sort of extension to string diagrams in which certain basic natural transformations \(TF \to FT\) have some kind of structure (exactly what kind will be discussed later) that makes it justifiable to draw them like this as two strands crossing over each other instead of as a "black box" vertex as in a regular string diagram.

(If you know a bit about braids, note here that I'm ignoring the group structure and working only with the monoid of positive braids. That is, braids where all "over" strands cross from left to right as you move from top to bottom.)

The exact conditions required on a natural transformation to draw it like that amount to guaranteeing that we can treat the "strands" and "crossings" of a braid diagram as physical strands of string and crossings of strands without getting into trouble.

Braids in Haskell

A while ago I noticed some candidate natural transformations to play the role of such braiding maps. Namely, for any \(T\) a traversable and \(F\) an applicative functor we have \(\texttt{sequenceA :: forall a. T (F a) -> F (T a)}\). Hereafter, I'll notate this map \(\sigma^T_F\),

Now, my hope is to represent \(\sigma^T_F\) as the diagram For this to be justifiable (i.e., to be able to manipulate diagrams containing this one as if that was a crossing of physical strings) we have to check that a few basic equations hold, which then guarantee the validity of all possible equations resulting from treating that as a crossing of strings. These equations are which is just a particular instance of the naturality of \(\sigma^{T_1}_{F_1}\) and which is not immediately clearly true. Keeping things grounded, In Haskell the first equation is written

(fmap . fmap) sequenceA . sequenceA = sequenceA . (fmap . fmap) sequenceA

and the second is

sequenceA . fmap sequenceA . sequenceA = fmap sequenceA . sequenceA . fmap sequenceA

To check if this second equation is true, let's first take a detour investigating the laws holding of traversables and how they look when interpreted as equations of braid diagrams. One of them is "linearity", which says that for any traversable \(T\) and applicative functors \(F\) and \(G\), the following diagram commutes Or, as an equation of braid diagrams, this looks like

Another is "naturality for applicative transformations". It says that for any natural transformation \(\alpha : F \to G\) which preserves the applicative structure (this is called an "applicative transformation" see e.g., here or here) we have that the following diagram commutes: Or, as an equation of braid diagrams, this looks like which says we can pull strands over applicative transformations.

Ok, now we can try to use these laws to prove the equation we wanted. The first equation follows from linearity, as does the last. The second equation follows from an application of "naturality for applicative transformations" assuming that the map \(\sigma^T_F\) is in fact an applicative transformation.

I know of some non-trivial \(T\) where \(\sigma^T_F\) is an applicative transformation for each \(F\), but they are all "fixed sized" functors. This includes for example, the (traversable, applicative) functor given by

data Diagonal x = Diagonal x x

Another example is, for \(m\) a monoid, (,) m. By \(T\) being "fixed size", I mean that length . (toList :: forall a. T a -> [a]) is a constant function. I think this should be sufficient since I think (i.e., I have an argument but didn't work it out fully) it implies \(T \cong X \mapsto A \times X^n\) for some \(n\) and for some \(A\) and (I think! I didn't check) the traversals for such functors are always applicative transformations.

Conclusions

Let \(\mathcal{T}\) be the class of traversable applicative functors \(T\) such that \(\sigma^T_F\) is an applicative transformation for each \(F\). Then by the above, for any \(T_1, \dots, T_n \in \mathcal{T}\) and any permutation \(\tau \in S_n\) (the symmetric group on \(n\) thingies), the natural transformations \(\eta : T_1 \cdots T_n \to T_{\tau(1)} \cdots T_{\tau(n)}\) defined over the \(\sigma^{T_i}\) are characterized by the positive braids project to \(\tau\) under the homomorphism from the braid group \(B_n\) to \(S_n\). If one wanted to decide the equality of two programs giving such natural transformations, one could simply compare them as braids, using Garside's/Thurston's algorithm for deciding equality of positive braids (see for example the accurately but to the uninitiated misleadingly named Word Processing in Groups).

My remaining questions are as follows.

  • Is \(T\) being fixed size necessary for \(\sigma^T_F\) to be an applicative transformation for all \(F\)?
  • If not, what are counterexamples and what is a necessary condition?

Discussion on reddit