Hello. My name is Jeremy Gibbons, and I'm going to tell you a bit about bi directional computation and why it's effect for why you can think of it as a computational effect. This is a reconstruction of a talk I gave at the Summit on Advances in Programming Languages in May 2015. BI directional transformations do with the problem of keeping two or more bits of data in sync with each other.
Think about the so-called View Update problem in databases with a complicated source and a simplified view that you might want to update the round tripping laws if you view and then immediately update with that same view, nothing should change. And conversely, if you update with a new view and then view the current state, you should receive the view you first thought of.
Now let's make it symmetric with multiple views, none of which need have the full picture peer to peer rather than master slave. There are many applications. It's a particular concern in model driven development, where a complex system is modelled from multiple complementary perspectives, which all have to be kept consistent. For simplicity. Imagine two views A and B onto a common source, each of which you want to be able to get and to put.
There's evidently something stateful going on. Having put an A, you want to get it back again. And similarly for be. That suggests thinking about it in terms of the State Monad. But of course, the A and the B are not independent of each other like two memory cells would be. The whole point of the exercise is that when you update A, it influences B, formerly the put operations on each side. Do not compute with any operation on the other side, they are entangled.
But now we've introduced one class of effects state. We might as well consider others too. In Haskell, we would implement not using the State Monad Transformer, which combines the State Monad with another underlying monad of effects. For example, a partial B X could raise a controlled exception if it is unable to restore consistency using the maybe monad. Parameter Rise X could depend on some global configuration settings or other contextual information using the reader monad.
This is important enough to determine situations in which there may be multiple sensible ways of restoring consistency. The user may indicate out of band their preference for how to resolve that choice. And on deterministic b x when putting on the left a new a prime that isn't already consistent with the current B could not deterministically select amongst all those V prime consistent with a prime. This can be captured using the set or list monads.
An interactive voice might ask the user or another external oracle for help in restoring consistency using the IO Monad. It might also learn keeping track of the questions it asks so as not to ask the same question again. Combining IO with more state. And so on. This work is a means to an end for us and not an end in itself.
We are particularly interested in approaches modelling not just that two views are consistent but also how they are so in particular in complex scenarios like model driven development. When the data items are models, which are collections of model elements, developer tools have to keep track of how model elements correspond to each other. They typically maintain some witness structure, for example, a collection of triples in the form.
This element is in this relation to that element. That too would be part of the maintained state. Our grand plan and the raison d'etre of the grant that is funding this work is to study the principle of least change. The round tripping laws we saw at the beginning constrains some operation sequences to be know ops but say nothing about the sequences that do have to make changes in order to restore consistency. In these cases, one often expects the least consistency restoring change to be made.
This is an outstanding problem in the VCs community. This change seems desirable, but no one really knows precisely what it should mean. So in conclusion, the bi directional transformations are inherently stateful, and in fact that state is a kind of entangled state. Having introduced state as one effect, we might as well consider other effects too. It turns out that the conditions for preserving well behaved this are rather subtle.
I haven't had time to show you that here. This is joint work with Faris, Abu Saleh, James Chaney, James macKinnon and Peter Stevens. And we have a paper notions of bi directional computation and entangled state monads. The Mathematics of Program Construction 2015. The work has been supported by the UK FCC grant a series of lease change for the ex.