On the Static Nature of Traversals

2012-12-09T18:29:14Z

One aspect I enjoy about functional programming is the immutable and static nature of data. Rather than having to think about how an object changes over time, often I get to think about data that is static, unchanging, which is easier to visualize. Sometimes I even think of functions not as a process, but a static relation between input and output. This can often be done with probability distributions, for example.

Traversable functors, which is functional programming’s answer to iterators, by definition appear to require dynamic behaviour to understand them. Traversable functors come with a traverse function.

traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
The traverse takes an applicative action h :: a -> f b and uses it to iterate through all the elements of the container t a, producing a new container t b while sequencing all the applicative effects of the action.

In order for traversals to be proper, they need to satisfy three laws. Laws one and two are analogous to the functor laws

  1. traverse Identity = Identity
  2. traverse (Compose . fmap g . f) = Compose . fmap (traverse g) . traverse f

The zeroth law is more difficult to state, but is easier to prove. It says that for every pair of applicative functors F and G, if eta :: F a -> G a is an applicative transformation, which means

then eta distributes through traverse, which means
eta . traverse f = traverse (eta . f)

The zero law is a free theorem, which effectively means one can always take it for granted for any traversal function one writes.

There is a static way of understanding a traversable functor satisfying these laws. Recently I have been working with Mauro Jaskelioff to prove that every traversable functor is a finitary container. For those eager for a preview, a Coq proof is available.

The upshot of all this technical work is that the traverse function is secretly a recipe for simply separating out from a container, t a, a list of the values it contains. This separation allows one to update or replace the values of the container with new values.

This static understanding has nothing to do with sequencing effects. Of course, one can separate out the contents of a container, sequence an applicative action over the contents, and reassemble the container with the new contents. Thus the dynamic understanding is derivable from the static understanding. However, the static understanding lets one see more possibilities than the dynamic understanding allows.

Recently, Jasper Van der Jeugt poses the following problem: Given a traversable functor t a and a wiggle function wiggle :: a -> [a], we want wigglesum to produce a list [t a] of the traversable functors with each value in the container independently adjusted by the different values produced by the wiggle function. For example, if we are given a wiggle function

wiggle :: Float -> [Float]
wiggle x = [x - 0.5, x + 0.5]
and a list of Floats
example :: [Float]
example :: [0.0, 1.2, -0.3]
then we want wigglesum wiggle example to be
[[-0.5, 1.2, -0.3], [0.5, 1.2, -0.3]
,[0.0, 0.7, -0.3], [0.0, 1.7, -0.3]
,[0.0, 1.2, -0.8], [0.0, 1.2, 0.2]]
where each value of the list is “wiggled” while all the other elements of the list remain fixed.

Most of the proposed solutions require defining an intermediate data structure; however, one can solve the problem with traverse and a few combinators. Knowing that traverse is really separating out the sequence of values held in the container, we should be able to use it to do something like create a list of lenses, each focusing in on one particular element of the container. It is not quite possible to produce a list of lenses, but the holesOf combinator come close enough to solve our problem. Given a traversal, then holesOf traverse :: t a -> [Context a a (t a)] maps a container of values to a list of contexts (also known as an indexed store comonad) which separate out each element of the container in turn. Then, for each element separated out of the the container, we can use the wiggle function to adjust the separated value. The experiment function provides exactly the behavour we want with experiment wiggle :: Context a a (t a) -> [t a]. Now it is a simple matter to combine these two components together

wigglesum :: Traversable t => (a -> [a]) -> t a -> [t a]
wigglesum wiggle = holesOf traverse >=> experiment wiggle

Although it is possible to solve this problem using a dynamic understanding of traversals, I believe it is much easier it solve this and other problems with a static understanding of traversals.

Many thanks goes to Twan van Laarhoven and Edward Kmett who helped me craft this understanding.

For those interested in an advanced puzzle: How do you write notches :: Traversable t => t a -> t (Store a (t a)) such that toList . notches = holesOf traverse? I have only been able to solve this by resorting to rank-2 polymorphism or by using partial functions internally.

Tags

,

Responses


Russell O’Connor: contact me