The Weird World of Bi-Directional Programming

Benjamin C. Pierce. The Weird World of Bi-Directional Programming, March 2006. ETAPS invited talk.

This nice set of slides (related to Harmony) begins with a detailed exploration of the design space for lenses (the bi-directional constructs), which is quite fun even if you aren't interested in the the rest of the presentation.

It's hard to convey to people what language design is about. I think these slides are a nice example. The process includes exploring various use cases, trying to come up with reasonable semantics, and specifying these decisions formally.

Don't worry: Types are part of the story, as well...

Comment viewing options

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

Excellent presentation

Agreed, it's such an excellent presentation that it has me interested in a subject from which I would have otherwise run away screaming.

There are a great many cases where it is valuable to be able to statically express and verify algorithms that are bijective or fit elsewhere in Pierce's "Lens Bestiary".

Applications

I haven't found many examples of PLs taking advantage of bijective functions. I thought it would come in handy in many situations -- for instance, projecting a data structure onto a UI view, and then updating the data structure back through the view lens (or a series of lenses).

But yeah, it's a very well-done presentation.

logic programming

Bijective AKA invertible functions can be used in logic programming to get smaller search spaces.

E.g. in KANREN:


examples/pure-bin-arithm.scm

Pure, declarative, and constructive binary arithmetics: Addition, multiplication, division with the remainder as sound and complete, pure, declarative relations that can be used in any mode and that recursively enumerate their domains. The relations define arithmetics over base-2 non-negative numerals of arbitrary size. If z is instantiated but x and y are not, (++o x y z) delivers all non-negative numbers that add to z and (**o x y z) computes all factorizations of z.

There have been some UIs based on constraint systems; I'm not sure about pure-logic-based systems.

constraint systems

I thought bijective functions smelled like constraint programming -- I guess because you can search for the inverse of a function via unification.

What makes this interesting to me is how many things in the computing world "pretend" to be bijective, when this is not explicitly declared in the programming language -- data conversion, compression/decompression, data persistence, UI forms, etc. I wonder if we'll see programming languages that explicitly declare this relationship. But I suppose it's non-trivial to derive a LZW decompressor from a compressor? :)

How to derive an LZW decompressor from a compressor

Check out There and Back Again, Arrows for Invertible Programming where you define the operation in one direction and get the reverse almost for free.

The free version of the paper is available somewhere, though I don't remember where I found it.

There and Back Again paper

Good old CiteSeer has it.

A while ago I made a

I thought it would come in handy in many situations -- for instance, projecting a data structure onto a UI view, and then updating the data structure back through the view lens (or a series of lenses).

A while ago I made a combinator library / DSL embedded in Haskell for specifying forms (Settings/Options/Prefs dialogs), which handles this view updating through "reference values" similar to lenses. Instead of composing the view side (UI) and the model side (data structure) using one combinator, I tried to separate these two sides. (This worked nice for product-like data structures and got a little murky for structures containing disjoint sums.) More info on the FunctionalForms website, and apologies for the self-plug.

link

the Harmony link in the topic appears to be missing a href.

Fixed. Thanks.

Fixed. Thanks.

Someone care to explain what was that all about?

I understood very little. Someone care to explain what was that all about? or give some links to introductions etc?

Maybe not the best introduction, but something:

A Language for Bi-Directional Tree Transformations, which I ran across in 2003. It covers similar material to the slides, but in the form of a paper; so, it's less bright and graphical, but it also doesn't gloss over the more involved parts the way a presentation has to.

An over-simplified view, from a long time LtU lurker

Could the problem Pierce addresses, in many cases, be cleared up by applying the model-view-controller (MVC) pattern? He seems to be coping with the difficulty of applying the degenerated MV(no C) pattern: the "view" covertly usurps "controller" responsibilities -- the model must maintain consistency by any means necessary.

Imagine a car with no gas pedal or brake pedal; instead, the driver grabs the speedometer needle and torques it this way or that. It falls to subtle, powerful, and expensive engineering to keep the car's speed in perfect accord with the position of the needle. Buckle up!

I modestly suggest that the client ("target") be presented with a view and a controller. With the controller, he updates the model ("source"). In due course, the model updates his view. Bada bang, bada bing.

terminology

In database-speak, "why can't we do it with triggers?" Yeah we can.

triggers or MVC?

I'm not sure I understand how database triggers or MVC can solve the problem Pierce presents.

Let's say we have a list (or a table) containing [social security, name, age, gpa]. If we project out social security and age, we are left with [name, gpa] (perhaps for display purpose). Now the user wishes to change the GPA for "John." There may be 10 different "John," we no longer have the social security number to tell us exactly which John.

How can we make sure the rigt "John" gets the gpa update? Do we keep the social security information, even though the user projected it out? What if we only have one John (bijective), clearly in that situation the solution is trivial.

We can write a trigger or provide a controller to handle this specific instance of GPA updates, but is there a general solution that requires no user intervention? If there is not general solution, is there a subset of scenarios in which the computer can figure out the 'right thing to do' without forcing the user to do work?

I have to admit that I went through Pierce's slides a while ago when they were mentioned on Wadler's blog, and I missed some of the more technical parts. I hope to be corrected.

generality

Of course MVC (or triggers) isn't a general solution. It needs lots of special-case logic.

There are general solutions for certain subsets of scenarios. Oracle's "updateable views" form one such tractable subset.

The question is whether a general solution is desirable at all. The only practical way to create general reversible transforms is by composing smaller reversible transforms in guaranteed-correct ways. This severely limits the kind of transforms we can build.

Let's consider another topic: real numbers, and bijective functions from R to R. Is there a "general way" to build computable bijective functions from smaller building blocks? Does it allow us to build, say, f(x) = x5? Or are we better off working out inverse functions by hand?

My understanding

I believe the point of the presentation was to come up with a rigorous way to derive the controller operations based on the model and the view. Right now you essentially have to construct a controller in an ad hoc fashion, based on what "seems right". The work the Pierce is doing seems to be aimed at allowing you to derive a controller that has particular properties with respect to the model and view. At least, that is what I got from the presentation (I may be completely off-base though - I only skimmed the slides).

The Simple Solution

I think you are mostly right, to me MVC and triggers look like the simple solutions of slide 12.

This is what happens...

when you apply category theory to programming. :) Seriously, what are the significant differences between a lens and a functor-cofunctor pair?

I think you mean morphisms

I think you mean morphisms rather than functor/cofunctor?

Lenses...

Did anyone use Boomerang, from the same project Harmony?