Successful evaluation for an undefined network

[ocharles]

I believe the following FRP system has undefined behavior:

{-# language LambdaCase, BlockArguments,  RecursiveDo #-}
module Test where

import Reactive.Banana
import Reactive.Banana.Frameworks
import Reactive.Banana.Combinators
import Data.Functor

main :: IO ()
main = do
  (ah1, doStart) <- newAddHandler
  (ah2, doStep) <- newAddHandler

  actuate =<< compile mdo
    onStartManual <- fromAddHandler ah1
    onStep <- fromAddHandler ah2

    let onStart = unionWith const onStartManual ("Won't see me!" <$ filterJust (fst <$> onStateChange))

    onStateChange <- accumE (Nothing, []) $ unions
      [ onStart <&> \y (_, xs) -> (Nothing, xs ++ [y])
      , onStep $> \case
          (_, x:xs) -> (Just x, xs)
          (_, [])   -> (Nothing, [])
      ]

    reactimate $ putStrLn "onStartManual" <$ onStartManual
    reactimate $ putStrLn "onStart" <$ onStart
    reactimate $ print <$> onStateChange

  doStart "Hello"
  doStep ()

The problem is onStart is defined in terms of onStateChange, but onStateChange is defined in terms of onStart. This is mutual recursion between events, and the documentation writes

In general, mutual recursion between several Events and Behaviors is always well-defined, as long as an Event depends on itself only via a Behavior, and vice versa.

That's not the case here, so this recursion isn't well defined. What concerns me is that it does run though! What we see in practice is:

> main
onStartManual
onStart
(Nothing,["Hello"])
onStart
(Just "Hello",[])

This is quite confusing:

1. onStartManual occurs, causing onStart to occur
2. onStateChange occurs, moving the state from (Nothing, []) to (Nothing, ["Hello"]) - this is expected.
3. onStep occurs, causing onStateChange to change from (Just "Hello", []).
4. However, at this instant we now know that onStart should occur, so the state transition should really have been the union of both onStep and onStart, so we'd expect to be at (Just "Hello", ["Won't see me!"]). This doesn't happen, and we instead enter a state that I think is impossible

I wonder if it's possible to spot this impossible recursion and to crash. I would much rather things crash than enter strange states.

Reading old resources like https://stackoverflow.com/questions/7850389/can-reactive-banana-handle-cycles-in-the-network/7852344#7852344, I think <<loop>> would be a reasonable outcome, as would just spinning.

[HeinrichApfelmus]

Hm. Let's digest the call to doStep. If onStart does not have an occurrence, then the state change for onStateChange should be

(Nothing, ["Hello"]) → (Just "Hello", [])

but this invalidates the assumption that onStart does not occur. On the other hand, if both onStart and onState have an occurrence, then the state change for onStateChange should be

(Nothing, ["Hello"]) → (Nothing, ["Won't see me!"])

and this invalidates the condition for onStart to occur.

This looks like a classic let x = not x paradox and I agree that it should be outlawed. It's probably possible to shrink this example to use only Bool, that would make for a useful unit test.

How does the model implementation behave for this example?

Internally, it seems that the Reactive.Banana.Prim.Plumbing.dependOn function does not notice when a cycle of event dependencies is being created.

[mitchellwrosen]

Question: is the Graph data structure meant to be a DAG? Its docs only mention being directed, but seems to have an API that relies on it being acyclic, too (e.g. walkSuccessors claims to visit a vertex only after all of its predecessors are visited).

If so, perhaps insertEdge should just call error instead of making a cycle? (And would that fix this issue?)

[HeinrichApfelmus]

Question: is the Graph data structure meant to be a DAG?

Yes, it's meant to be a DAG.

If so, perhaps insertEdge should just call error instead of making a cycle?

That would be nice — but we would have to detect that there is a cycle. 😅 This can be done with a depth first search, but that is an expensive operation in that it needs to visit all the vertices on the putative cycle. I'm currently not aware of an algorithm that keeps track of the transitive closure and can do incremental updates that are faster than this. 🤔

That said, it may be possible to detect the cycle while the Event is turned into a Pulse, as this process does involve a depth first search of sorts anyway.

[mitchellwrosen]

That said, it may be possible to detect the cycle while the Event is turned into a Pulse, as this process does involve a depth first search of sorts anyway.

@HeinrichApfelmus could you provide some guidance on where in the code one might find an Event turning into a Pulse, with this depth-first-search-of-sorts nearby? I'm interested in tackling this issue, to the extent that it can be tackled, but (as usual) the code is all a little over my head 😃

[HeinrichApfelmus]

@HeinrichApfelmus could you provide some guidance on where in the code one might find an Event turning into a Pulse, with this depth-first-search-of-sorts nearby?

That's a tough one. 🤔 The best I can do in a pinch is to point you to the documentation of observable sharing in the design document: https://github.com/HeinrichApfelmus/reactive-banana/blob/master/reactive-banana/doc/design/design.md .

The issue is that the Cache type supports arbitrary recursion and cannot distinguish between Event → Behavior → Event (allowed) and Event → Event (disallowed).

If you look at the implementation of Reactive.Banana.Prim.High.Combinators.mapE and friends, you will find the function liftCached1 which eventually results in a call to Reactive.Banana.Prim.High.Cached.cache. This functions pretends that the monadic action that creates the Pulse will succeed, and caches its value for recursive use. This is necessary to handle the case of a Event → Behavior → Event recursion, but unfortunately, it also yields a result when recursing Event → Event; the problem is that this result is now semantically unsound.

The only viable solution is to reify the issue in the structure of the code somehow. In other words, one would probably need two distinct Cache types — one for Event, one for Behavior — in such a way that mutual recursion between them is allowed, but recursion within a type is forbidden.