# [Haskell-cafe] A question about causality in FRP

Alan Jeffrey ajeffrey at bell-labs.com
Thu Oct 13 16:54:06 CEST 2011

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

```

More information about the Haskell-Cafe mailing list