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.