Proposal: Infinitesimal delays about reactive-banana HOT 10 CLOSED

Unfortunately, infinitesimal delays are a huge can of worms.

Main problem: Executable model

The main problem is that I don't have a model that supports recursion properly. I mean, the model Event a = [(Time,a)] you refer to is fine as an intuition about events, but I can't use it as executable Haskell code because it doesn't support recursion. That's why the Reactive.Banana.Model module uses Event a = [[a]] instead, but I don't know how to put infitesimal delays in there.

Finding a working model for infinitesimal delays looks like a more elaborate research topic to me, and probably not something that can be solved in a github issue.

Union

A very desirable property of the primitive union combinator is that the law

id = split . union'

holds, where

union' :: (Event a, Event b) -> Event (Either a b)
union' (a,b) = (Left <$> a) `union` (Right <$> b)

split  :: Event (Either a b) -> (Event a, Event b)
split e = (fromLeft <$> filterE isLeft e, fromRight <$> filterE isRight e)

Unfortunately, the delays introduced in your proposed version of union destroy this property. In other words, it now makes a difference whether you first union two event streams and then filter one of them, or whether you work with the first event stream right from the start.

from reactive-banana.

Main problem: Executable model

Well, I did have some ideas about fitting infinitesimal delays into a similar model to the current one, but of course it's perfectly possible (even likely) they my ideas have been tried before and shown to not work.

Union

Hmm — this is ugly, but I'm not sure it is that big a deal, since the "error" in timings is infinitesimal. union' . split . union' ≡ id holds, for instance.

from reactive-banana.

Main problem: Executable model

If you come up with something, I'm happy to hear it, of course. :) I just wanted to clarify what I think the core problem is and why it's difficult.

Union

The effect on the example from the previous thread would be that the following two event streams are no longer equivalent

buttonClicked1 = filterE isA $ (A <$ aClicked) `union` (B <$ bClicked)
buttonClicked2 = A <$ aClicked

They can be distinguished by taking snapshots with behaviors, as that would be the point of infinitesimal delays. So, it's probably not a good idea to bake delays into the union combinator.

from reactive-banana.

Another problem is that it isn't clear to me what should happen if two simultaneous events are separately delayed. Does that mean that both of those events appear simultaneously an instant later, or does it mean that they each get their own instant?

from reactive-banana.

Also, the discussion illustrates why if we are going to bake delays into a union-like combinator, then said combinator should probably be called something like unionUsingDelays in order to make it clear that it will break laws that we might have otherwise expected to hold.

from reactive-banana.

Main problem: Executable model

I'll try and come up with a concrete model implementation and see how it goes :)

Union

Hmm. I agree they're no longer equivalent, but I'm not sure it would cause problems in practice. One of the most compelling things about delays to me are that they allow union to have reasonable semantics. Do you have an example where the difference between these two would cause problems?

Delaying multiple events

The intention is that if a and b occur simultaneously, then delay a and delay b do, too. I can't think of any sort of model where they wouldn't, and I think that would break a huge range of invariants. As far as the [(Time,a)] thinking-model goes, it would break referential transparency:

a = (t,x) : ...
b = (t,y) : ...
delay a = (t+ε,x) : ...
delay b = (t+ε,y) : ...

So delay a and delay b must occur simultaneously.

Naming of delaying union

I think a long, verbose name would be a shame; if the problem brought up by @HeinrichApfelmus is minor or solvable (I'm not sure yet), then it makes sense to name the combinator that Does The Right Thing in the majority of cases with a short, simple name, and a name like unionUsingDelays is not really more descriptive unless you already know what union is supposed to mean.

If the problems aren't solvable, then I'm not sure infinitesimal delays are desirable in the first place.

from reactive-banana.

The thing is, it really isn't obvious to me that introducing delays really is The Right Thing in the majority of cases and therefore the best way to give union reasonable semantics. Furthermore, it is not clear to me that introducing a delay (which breaks laws as Heinrich illustrated) is so obviously the Right Thing that it is what a user would expect this behavior from the union combinator. That is why at least for now something like unionDelayed (to shorted my earlier proposal) would probably be a better name since it makes the introduction delay explicit.

I do see your point, though, that it is hard to envision a model where delay a and delay b do not occur simultaneously without violating referential transparency.

from reactive-banana.

The thing is, it really isn't obvious to me that introducing delays really is The Right Thing in the majority of cases and therefore the best way to give union reasonable semantics.

Well, that's why this proposal exists: to flesh out the cases for and against delays and what effects they have :)

which breaks laws as Heinrich illustrated

I think this might be misleading; the proposal is to change the semantics, and laws are part of the semantics. It doesn't break anything, it just changes what does and doesn't hold. There's trade-offs involved in any semantic change.

from reactive-banana.

Well, that's why this proposal exists: to flesh out the cases for and against delays and what effects they have :)

Actually, I would consider that to be a very separate discussion from whether it makes sense to bake delays into union --- that is, there is a huge difference between merely adding the possibility of delays to the semantics and making them the standard way that merging of simultaneous events is handled.

I think this might be misleading; the proposal is to change the semantics, and laws are part of the semantics. It doesn't break anything, it just changes what does and doesn't hold. There's trade-offs involved in any semantic change.

Yes, but the reason why such laws are being brought up is because they are arguably the intuitive way that a standard union combinator should behave. In particular, the law Heinrich brought up --- which is essentially that after using union to merge two events you should always be able to split the resulting event back up again to recover the original events --- is a consequence of the intuition a standard combinator called union should never by itself cause a loss of information at the present instant. However, that is exactly what would happen if it automatically inserted a delay in one of the events.

from reactive-banana.

I no longer believe that delays are the solution, so I'm closing this issue.

from reactive-banana.