[reactive] "Time travel" with withNextE

Luke Palmer lrpalmer at gmail.com
Fri Nov 21 13:56:21 EST 2008

On Fri, Nov 21, 2008 at 7:23 AM, Robin Green <greenrd at greenrd.org> wrote:
> withNextE seems to allow occurrences' values to depend on occurrences
> which haven't yet occurred.
> Of course, it doesn't actually allow time travel. If the occurrence is
> not yet computed, presumably it will block until it does.
> Still, this is problematic theoretically. It allows "simulations"
> to be constructed which contain reverse causality (if the simulation
> makes all the input occurrences available immediately). Is this a case
> of making the framework a little too powerful?

I have been on-and-off experimenting with formalizations of FRP in
which this function would be illegal -- i.e. semantically meaningless.
Causality is one of the two big problems I see with the semantics.

I believe that "blocking thunks" can be of huge benefit to an
implementation since they are exposed to the optimizer.  However, I
think it's a bad idea to ever expose a blocking thunk to a user of the
reactive library.  I played with a "time" module for a little while
that encoded time relations in the type system, in order that you had
to prove you were after an occurrence of a future in order to get its
value.  I still think that a reactive implementation ought to be based
on an abstraction like this, so it comes with at least one sort of
correctness proof.

More information about the Reactive mailing list