[Haskell-cafe] A question about causality in FRP

[Alan Jeffrey]

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 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.