Comonadic Functional Attribute Evaluation

Comonadic Functional Attribute Evaluation. Tarmo Uustalu and Varmo Vene.

We have previously demonstrated that dataflow computation is comonadic. Here we argue that attribute evaluation has a lot in common with dataflow computation and admits a similar analysis. We claim that this yields a new, modular way to organize both attribute evaluation programs written directly in a functional language as well as attribute grammar processors.

(This is an extended abstract. I believe a longer version is here, but I haven't read it.)

We've previously seen The Essence of Dataflow Programming, and in one sense this is a follow-up. Applying comonads to dataflow programming was not uncritically accepted as being "essential," as I recall. For attribute grammars, this approach seems elegant enough from a casual read, but they don't offer a detailed comparison with prior work on attribute grammars, and I'm nowhere near familiar enough to judge for myself.

Whether or not this is a significant step forward in that sense, it certainly has some nice examples of comonads. There's also this claim:

This does not seem to have been mentioned in the literature, but the type constructor CxtTree E is a comonad (just as LS is; in fact, the same is true of all zipper type constructors).

(Emphasis mine.) This seems to be a relatively well-known fact about zippers, but perhaps not?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I found this paper a great way to...

...get my head around the relationship between comonads and contexts that I've seen mentioned in many places but I didn't quite get.

Suppose you are working with a datatype that has some kind of notion of a neighbourhood. What I mean is something like a tree, with elements of some type, say A. Each element in the tree has neighbours in the form of its parent and its children (if they exist). Now suppose you have a function that takes as argument a neighbourhood of A's and returns a value A. Then there is a natural way to compose these functions. The easiest way to see this is to notice that the function from neighbourhoods to values gives rise to a function from trees to trees. You take the original tree and then update each value (simultaneously) by applying the function to the neighbourhood of each element replacing the element with the return value. Functions from trees to trees obviously compose and it's not hard to see that the composition can be viewed as another function that maps neighbourhoods to values. (These functions are examples of coKleisli arrows.) The key thing is that the type of a neighbourhood forms a comonad because the glue to compose these coKlesli arrows satisfies all of the requirements required of cobind. And this makes sense of the idea that comomads can be used to describe the notion of a value in a context (where context = neighbourhood).

The use of zippers to talk about these neighbourhoods is also pretty nice.

As a result of this paper I now see comonads everywhere. For example many image processing operations can be viewed naturally as comonadic operations that map pixels and their neighbourhoods to new values. I'm not sure it actually helps me solve any useful problems though...

But can you do stuff?

I seem to remember that Bad Things Happen if you try to add side effects to a comonadic notion of computation, and in particular this was a flaw in Kieburtz' paper.