Lambda the Ultimate

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.

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? :)

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.

Good old CiteSeer has it.

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.

Fixed. Thanks.

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.

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

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.

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) = x⁵? Or are we better off working out inverse functions by hand?

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).

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

I think you mean morphisms rather than functor/cofunctor?