1
00:00:00,450 --> 00:00:02,639
Hello. My name is Jeremy Gibbons,

2
00:00:02,640 --> 00:00:09,990
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.

3
00:00:10,800 --> 00:00:16,920
This is a reconstruction of a talk I gave at the Summit on Advances in Programming Languages in May 2015.

4
00:00:19,860 --> 00:00:25,320
BI directional transformations do with the problem of keeping two or more bits of data in sync with each other.

5
00:00:26,370 --> 00:00:33,089
Think about the so-called View Update problem in databases with a complicated source and a simplified view that

6
00:00:33,090 --> 00:00:39,740
you might want to update the round tripping laws if you view and then immediately update with that same view,

7
00:00:40,050 --> 00:00:41,040
nothing should change.

8
00:00:41,700 --> 00:00:48,690
And conversely, if you update with a new view and then view the current state, you should receive the view you first thought of.

9
00:00:51,240 --> 00:00:58,590
Now let's make it symmetric with multiple views, none of which need have the full picture peer to peer rather than master slave.

10
00:01:00,180 --> 00:01:04,260
There are many applications. It's a particular concern in model driven development,

11
00:01:04,650 --> 00:01:09,960
where a complex system is modelled from multiple complementary perspectives, which all have to be kept consistent.

12
00:01:13,230 --> 00:01:20,100
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.

13
00:01:21,600 --> 00:01:27,300
There's evidently something stateful going on. Having put an A, you want to get it back again.

14
00:01:27,480 --> 00:01:32,480
And similarly for be. That suggests thinking about it in terms of the State Monad.

15
00:01:34,430 --> 00:01:38,990
But of course, the A and the B are not independent of each other like two memory cells would be.

16
00:01:39,740 --> 00:01:47,719
The whole point of the exercise is that when you update A, it influences B, formerly the put operations on each side.

17
00:01:47,720 --> 00:01:51,530
Do not compute with any operation on the other side, they are entangled.

18
00:01:54,760 --> 00:01:59,560
But now we've introduced one class of effects state. We might as well consider others too.

19
00:02:00,760 --> 00:02:08,890
In Haskell, we would implement not using the State Monad Transformer, which combines the State Monad with another underlying monad of effects.

20
00:02:09,970 --> 00:02:16,690
For example, a partial B X could raise a controlled exception if it is unable to restore consistency using the maybe monad.

21
00:02:17,990 --> 00:02:24,900
Parameter Rise X could depend on some global configuration settings or other contextual information using the reader monad.

22
00:02:25,920 --> 00:02:31,980
This is important enough to determine situations in which there may be multiple sensible ways of restoring consistency.

23
00:02:32,880 --> 00:02:36,800
The user may indicate out of band their preference for how to resolve that choice.

24
00:02:39,020 --> 00:02:44,929
And on deterministic b x when putting on the left a new a prime that isn't already consistent with

25
00:02:44,930 --> 00:02:50,690
the current B could not deterministically select amongst all those V prime consistent with a prime.

26
00:02:51,440 --> 00:02:54,290
This can be captured using the set or list monads.

27
00:02:56,430 --> 00:03:04,050
An interactive voice might ask the user or another external oracle for help in restoring consistency using the IO Monad.

28
00:03:04,920 --> 00:03:09,990
It might also learn keeping track of the questions it asks so as not to ask the same question again.

29
00:03:10,620 --> 00:03:14,580
Combining IO with more state. And so on.

30
00:03:16,930 --> 00:03:20,110
This work is a means to an end for us and not an end in itself.

31
00:03:20,710 --> 00:03:25,840
We are particularly interested in approaches modelling not just that two views are consistent

32
00:03:26,110 --> 00:03:31,990
but also how they are so in particular in complex scenarios like model driven development.

33
00:03:32,290 --> 00:03:35,530
When the data items are models, which are collections of model elements,

34
00:03:36,100 --> 00:03:39,790
developer tools have to keep track of how model elements correspond to each other.

35
00:03:41,320 --> 00:03:46,240
They typically maintain some witness structure, for example, a collection of triples in the form.

36
00:03:46,570 --> 00:03:52,120
This element is in this relation to that element. That too would be part of the maintained state.

37
00:03:54,430 --> 00:04:00,820
Our grand plan and the raison d'etre of the grant that is funding this work is to study the principle of least change.

38
00:04:02,440 --> 00:04:07,240
The round tripping laws we saw at the beginning constrains some operation sequences to be know ops

39
00:04:07,570 --> 00:04:12,130
but say nothing about the sequences that do have to make changes in order to restore consistency.

40
00:04:13,090 --> 00:04:17,950
In these cases, one often expects the least consistency restoring change to be made.

41
00:04:18,820 --> 00:04:26,020
This is an outstanding problem in the VCs community. This change seems desirable, but no one really knows precisely what it should mean.

42
00:04:29,060 --> 00:04:37,700
So in conclusion, the bi directional transformations are inherently stateful, and in fact that state is a kind of entangled state.

43
00:04:39,310 --> 00:04:43,750
Having introduced state as one effect, we might as well consider other effects too.

44
00:04:44,950 --> 00:04:48,670
It turns out that the conditions for preserving well behaved this are rather subtle.

45
00:04:48,820 --> 00:04:58,380
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.

46
00:04:58,740 --> 00:05:04,140
And we have a paper notions of bi directional computation and entangled state monads.

47
00:05:04,620 --> 00:05:14,590
The Mathematics of Program Construction 2015. The work has been supported by the UK FCC grant a series of lease change for the ex.