Latest / Strachey Lectures / Strachey Lecture: Bidirectional Computation is Effectful

Transcript

Strachey Lecture: Bidirectional Computation is Effectful · Strachey Lectures

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