reactive-banana
reactive-banana copied to clipboard
Successful evaluation for an undefined network
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:
-
onStartManual
occurs, causingonStart
to occur -
onStateChange
occurs, moving the state from(Nothing, [])
to(Nothing, ["Hello"])
- this is expected. -
onStep
occurs, causingonStateChange
to change from(Just "Hello", [])
. - However, at this instant we now know that
onStart
should occur, so the state transition should really have been the union of bothonStep
andonStart
, 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.
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.
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?)
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.
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 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.