# Matrix traversals and unification

While playing with Conor McBride’s material for his summer school on dependently-typed metaprogramming, I was puzzled as to how easy it was to implement matrix transposition. I will detail here what goes on, as I find the insight slightly amusing.
First, some boilerplate code:
We define standard length-indexed lists (usually named vectors), and related operations.
We now define applicative functors, along with two instances for the identity functor and the fixed-sized vector functor (you can think of it as a finite tabulation).
We then proceed to define the traversable interface.
You can try to think of traverse’s signature in these terms: given a G-effectful action transforming an element of S into an element of T, and a F-structure containing some elements of S, we can compute a G-effectful action building up a F-structure of elements of T. In some sense, we map the action into the structure, and then we fold the structure of actions into a structure of results.
Vectors of a given size are traversable:
The given exercise at this point in the course was to implement matrix transposition. It was heavily hinted that this would be implemented as a traversal, so I let myself be guided by the types, and write the following, where the question mark stands for a hole, a placeholder for a term that you do not want to write yet:
At that point, the type of the hole (the expected type of the term to be filled in place of the hole) was the following:
Well, do I have just the right candidate for that type! Even Agsy, the automated program search tool shipped with Agda, knows what to put in that hole!
At that point though, the doubt builds in my mind. It seems to me that a traversal with the ineffectful identity function should just give me back the same structure I started with... Yet given the type of transpose, it definitely modifies the shape of the input structure. And at such a polymorphic type, with such a generic implementation, there’s only so much it can be doing! How does it work!?
Before trying to solve that question, I wonder whether I could implement the identity function as a matrix traversal... Again, being type-directed:
Can you guess the type of the hole? :-)
And indeed, here comes the implementation:
Sounds familiar? Indeed, to implement matrix transposition and matrix identity, I wrote the exact same code! So something must be happening under the covers, at the level of implicit arguments.
Let’s play the part of the unification algorithm with our two toy functions. Recall the full polymorphic type of traverse:
So, by unification (the question-marked variables are now unification variables in scope):
For our two examples, we ascribe the following type signatures:
The following unification problems are to be solved:
This gives rise to the following unification equations:
And here are the potential solutions:
However, another additional constraint, namely the implicit instance argument that requires ? G to be an applicative functor, prevents the second equation from being solved, as we did not provide a way for Agda to build nested instances.
The mystery is therefore solved: even though we wrote the same code, the implicit arguments have been inferred, type-directed by the unification, to be different. In the case of matrix transposition, the F-structure is the outermost vector layer, and the G-effect is the innermost vector layer. In the case of matrix identity, the entire matrix is the F-structure, and the G-effect is identity. It makes sense then, that traversing with no effect and the identity function preserves the matrix completely.
One may now wonder how come traversing a vector with a vector effect effectively transposes the entire structure, seen as a matrix. It is actually fairly simple once you start unfolding the definitions:
All in all, matrix transposition is not implemented as a matrix traversal, but as a vector traversal with a column-building effect!
Finally, here is how it goes for matrix identity: