[Haskell-cafe] A question about causality in FRP

[Alan Jeffrey]

On 10/13/2011 10:43 PM, David Barbour wrote:
> On Thu, Oct 13, 2011 at 7:54 AM, Alan Jeffrey <ajeffrey at bell-labs.com
> <mailto:ajeffrey at bell-labs.com>> wrote:
> The `problem` such as it exists: you will be unable to causally
> construct the argument toith the `weird` function, except by modeling a
> nested/simulated world (i.e. modeling one FRP system within another).
> This is not an unrealistic endeavor, e.g. one might model the future
> position of a thrown baseball in order to predict it. In this sense,
> `weird` is not weird.

Ah, I think this is a very good summary. It seems that there's an 
implicit shift of worlds when you nest FRP behaviours. The top level 
world (the one that reactimate is executing) uses wall-clock time, but 
nested behaviours are in a different world, where time is simulated.

Making these worlds explicit (I never met a problem that couldn't use 
some more phantom types :-) we have a type Beh W A for a behaviour in 
world W of type A, and a definition of causality that's indexed by 
worlds. Writing RW for the top-level real world, and SW for a simulated 
world, we have:

   weird : Beh RW (Beh RW A) -> Beh RW A
   weird b t = b t (t + 1) -- not causal

   weird : Beh RW (Beh SW A) -> Beh RW A
   weird b t = b t (t + 1) -- causal

and:

   double : Beh RW A -> Beh RW (Beh RW A)
   double b t u = b u -- causal

   double : Beh RW A -> Beh RW (Beh SW A)
   double b t u = b u -- not causal

[Caveat: details not worked out.]

Making worlds explicit like this I think helps clarify why one person's 
"weird" is another person's "perfectly reasonable function" :-)

Does something like this help clarify matters?

A.