Re: [Haskell-cafe] A question about causality in FRP

One more thing... The function: return :: a -> Beh a return x t = x fails to be causal when a is itself a behaviour, since it specializes to (after a bit of eta-conversion): return :: Beh a -> Beh (Beh a) return b t u = b u which isn't causal. This rules out return, which in turn means that Beh can't implement the Monad type class. I don't think this impacts arrowized FRP, but it does mean that any causal non-arrowized model can't form a monad, which seems unfortunate. If the "causality" requirement were replaced by "deep causality" then I believe the model would form a monad (cough cough but in a different category cough). A. On 10/14/2011 05:18 PM, Jeffrey, Alan S A (Alan) wrote:

I should add that I have a pragmatic reason for asking about causality, which is that over at https://github.com/agda/agda-frp-js I have an implementation of FRP for Agda running in the browser using an Agda-to-JS back end I wrote.

In that model, I can see how to implement deep causality, but I can't see how to implement shallow causality, since the back end interfaces to the DOM event and time model.

A.

...

On 10/13/2011 10:43 PM, David Barbour wrote:

...

...

On Thu, Oct 13, 2011 at 7:54 AM, Alan Jeffreymailto:ajeffrey@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.