reactive-banana icon indicating copy to clipboard operation
reactive-banana copied to clipboard

Discrepancy in model and implementation

Open Abastro opened this issue 2 years ago • 15 comments

Just discovered this while trying to conjure Event a -> Event (Event a) up for convenience.

Documentation states the semantics as:

once e = \time0 -> take 1 [(t, a) | (t, a) <- e, time0 <= t]

Note the time0 <= t constraint, which means event occurrence at Moment time is accepted.

However, once is defined using switchE.

once :: MonadMoment m => Event a -> m (Event a)
once e = mdo
  e1 <- switchE e (never <$ e1)
  return e1

Now, from switchE we have

switchE e0 ee0 time0 =
    concat [ trim t1 t2 e | (t1,t2,e) <- intervals ee ]
  where
    laterThan e time0  = [(timex,x) | (timex,x) <- e, time0 < timex ]
    ee                 = [(time0, e0)] ++ (ee0 `laterThan` time0)
    intervals ee       = [(time1, time2, e) | ((time1,e),(time2,_)) <- zip ee (tail ee)]
    trim time1 time2 e = [x | (timex,x) <- e, time1 < timex, timex <= time2]

The trim function only allows event occurrence time1 < timex. Since the intervals ee should start with [(time0, time1, e0), ..], by trim occurrence of e0 before time0 is cut off!

According to this documentation, switchE e (never <$ e1) should not produce any value at the Moment time (time0). Hence, once should drop event occurrence at the Moment time / time0.

I am utterly confused here, which one is right?

Abastro avatar Feb 18 '23 10:02 Abastro

The comment on switchE is wrong. My guess is it simply wasn't properly fixed up (by me) whenever we added the initial event argument.

It's trying to convey that at the moment the event-of-events fires, if the event that it contains also fires, that inner event's value will not be present.

In plainer English: switchE e es acts like e up until (and including) the moment es fires, at which point it starts acting like the event that es fired, and so on.

Hope that helped somewhat. In my opinion, we should maybe rework the "semantics" comment of switchE. It's just a bit too complicated to extract meaning from. A nice image or something would be a lot clearer.

mitchellwrosen avatar Feb 19 '23 07:02 mitchellwrosen

I see. While trying to check the semantics, I noticed strange behavior regarding observeE and accumE.

Consider this code:

testCase = [Just n | n <- [0..5]]
listing event = accumE [] ((\x -> (++ [x])) <$> event)
nested event = switchE never (observeE (listing event <$ filterE even event))
interpret nested testCase

This gives [Nothing,Just [1],Just [1,2],Just [3],Just [3,4],Just [5]]

Note that filterE even event fires at [Just 0, Nothing, Just 2, Nothing, Just 4, Nothing]. The event parameter itself fires at the moment time, so observeE (listing event <$ filterE even event) should give alike [Just [Just [0], Just [0, 1], ..], Nothing, Just [Just [2], Just [2, 3], ..]], .. ] :: Event (Event [Int])

However, when collapsed with switchE, we can see that e.g. [2, 3] is missing: [Nothing,Just [1],Just [1,2],Just [3],Just [3,4],Just [5]].

I guess accumE is dropping event occurrence simultaneous with the moment, but this could be wild guess.

Abastro avatar Feb 19 '23 15:02 Abastro

That output looks right to me. Could you explain why [2,3] should appear?

mitchellwrosen avatar Feb 20 '23 04:02 mitchellwrosen

I should have stayed with the list semantics.. Let's say event = [(Time n, n) | n <- [0..5]]. I believe that docs imply accumE will include the simultaneous event occurrence. So, e.g. listingE event (Time 2) = [(Time 2, [2]), (Time 3, [2, 3]), (Time 4, [2, 3, 4]), (Time 5, [2, 3, 4, 5])]. As filterE even event also happens at Time 2, listingE event <$ filterE even event contains (Time 2, listingE event). Thus, we have

observeE (listingE event <$ filterE even event)
  = [.., (Time 2, listingE event (Time 2) ,..]
  = [.., (Time 2,  [(Time 2, [2]), (Time 3, [2, 3]), (Time 4, [2, 3, 4]), (Time 5, [2, 3, 4, 5])] ), ..]

Then, switchE switches after each event occurrence, so we should have

switchE never (observeE (listingE event <$ filterE even event))
  = [..,  (Time 3, [2, 3]), (Time 4, [2, 3, 4]), ..]

so I think the fourth element should be Just [2, 3].

Abastro avatar Feb 21 '23 13:02 Abastro

At (the end of the moment at) time 2, we switch to a new observeE (listingE event), which first emits at time 3 with value [3]. The event doesn't exist at time 2, therefore it doesn't accumulate a [2]. Does that make sense?

mitchellwrosen avatar Feb 21 '23 15:02 mitchellwrosen

I do not understand why external switching would cause changes to the event.

In fact, I found the discrepancy between the Model and the Combinators module.

import Reactive.Banana.Combinators as C
testCase = [Just n | n <- [0..5]]
listingE event = C.accumE [] ((\x -> (++ [x])) <$> event)
evenE event = C.filterJust $ (\n -> n <$ guard (even n)) <$> event
nested event = C.switchE never (C.observeE (listingE event <$ evenE event))
C.interpret nested testCase

gives [Nothing,Just [1],Just [1,2],Just [3],Just [3,4],Just [5]]

while

import Reactive.Banana.Model qualified as M
testCase = [Just n | n <- [0..5]]
listingE event = M.accumE [] ((\x -> (++ [x])) <$> event)
evenE event = M.filterJust $ (\n -> n <$ guard (even n)) <$> event
nested event = M.switchE M.never (M.observeE (listingE event <$ evenE event))
M.interpret nested testCase

gives [Nothing,Just [0,1],Just [0,1,2],Just [2,3],Just [2,3,4],Just [4,5]] as I expected.

I wonder which one is implemented wrong.

EDIT: Failing test

Abastro avatar Feb 21 '23 22:02 Abastro

Huh, yes, I see what you mean now. Sorry it took so long for me to understand. I agree with your assessment; the model seems correct to me, too.

mitchellwrosen avatar Feb 22 '23 06:02 mitchellwrosen

So, what needs to be fixed to correct the semantics?

Abastro avatar Feb 22 '23 10:02 Abastro

I think we just need to rewrite the comment on switchE to treat the initial event specially, because its first occurrence is visible in the output, unlike the others. Is that what you mean? Or maybe you understood that's what I meant by this comment, but you see a mistake with that explanation?

In plainer English: switchE e es acts like e up until (and including) the moment es fires, at which point it starts acting like the event that es fired, and so on.

mitchellwrosen avatar Feb 22 '23 11:02 mitchellwrosen

Oh, I think that would be fine for a documentation, I was commenting on fixing the Failing test.

Abastro avatar Feb 22 '23 11:02 Abastro

Oh, I think that's a puzzle for @HeinrichApfelmus or another intrepid adventurer.

If I had to speculate, it seems we're building the event too late. We ought to build it the moment it's switched to, even if we only start observing its values in the next.

... wait, heh, I think I'm starting to lean towards the model being incorrect. The preceding paragraph seems a little nonsense - we delay rebuilding the network until the end of a moment because it's inefficient to do it "live".

But either way, great find!

mitchellwrosen avatar Feb 22 '23 12:02 mitchellwrosen

This note seems relevant:

{-
* Note [PulseCreation]

We assume that we do not have to calculate a pulse occurrence
at the moment we create the pulse. Otherwise, we would have
to recalculate the dependencies *while* doing evaluation;
this is a recipe for desaster.

-}

mitchellwrosen avatar Feb 24 '23 15:02 mitchellwrosen

Does the Moment here means in logical time, or something else?

Abastro avatar Feb 25 '23 00:02 Abastro

Yes, the logical time

mitchellwrosen avatar Feb 25 '23 02:02 mitchellwrosen

If I understood correctly, switchE documentation is right while once and accumE need to be fixed. Correct? Is this an wrong assessment?

Abastro avatar Feb 25 '23 13:02 Abastro