[Haskell-cafe] A question about causality in FRP

[Alan Jeffrey]

Hi everyone,

Not sure this is the right venue, as this is a question about the 
semantics of FRP rather than Haskell...

I have a question about the definition of "causality" for stream 
functions. A quick recap... Given a totally ordered set T (of times), 
the type of behaviours Beh A is defined to be (T -> A). Behaviours come 
with an equivalence relation a =t b (equal up to time t) defined as:

   a =t b  iff  forall s <= t . a(s) = b(s)

A function (f : Beh A -> Beh B) is causal whenever it respects =t, i.e. 
(forall t . a =t b => f a =t f b).

This is fine and good, until we hit nested behaviours, where there are 
oddities. Consider the function:

   double : Beh A -> Beh Beh A
   double a t u = a u

This fails to be causual, because (using list notation for behaviours 
where the time domain is natural numbers) we have:

   [0,1,2,...] 0 = 0 = [0,2,4,...] 0
   double [0,1,2,...] 0 = [0,1,2,...] != [0,2,4,...] = double [0,2,4,...]

On the other hand:

   weird : Beh Beh A -> Beh A
   weird a t = a t (t + 1)

is causal, even though on the surface the behaviour at time t depends on 
the behaviour at time t+1. An alternate definition, which allows double 
and disallows weird, is a "deep" equality:

   a ~t b  iff  forall s <= t . a(s) ~s b(s)

Note that this depends on deep equality being defined at type A. Some 
appropriate definitions for ~t at other types includes:

   at type A -> B: f ~t g iff forall s <= t, a ~s b implies f a ~s f b
   at type (A,B): (a1,a2) ~t (b1,b2) iff (a1 ~t b1) and (a2 ~t b2)

[And yes, I don't think it's a coincidence that this looks a lot like a 
parametricity definition or step-indexed logical relation.]

Has such a definition of "deep" causality been investigated?

Alan.