David Barbour wrote:

If you want first-class behaviors or behavior transformers, those will need a different abstraction than 'nested' behaviors. Nested != First Class. You'd have special functions to lift a first-class behavior as an argument (e.g. add a phantom type to prohibit non-causal observation), and to lower it into the main system for sampling (e.g. ArrowApply).

The usual model for arrowized FRP is based on this type: newtype Auto a b = Auto (a -> (b, Auto a b)) I would be very interested in how you would write an ArrowApply instance for such a type. So far my conclusion is: It's impossible. Do you have a different AFRP model in mind? Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/

David Barbour wrote:

...

The usual model for arrowized FRP is based on this type:

newtype Auto a b = Auto (a -> (b, Auto a b))

I would be very interested in how you would write an ArrowApply instance for such a type. So far my conclusion is: It's impossible.

Interesting claim. The implementation is obvious enough: runAuto (Auto f) = f app = Auto $ \ (f,x) -> let (x',f') = runAuto f x in (x',app)

Which arrow laws does this violate? Or is your concern that a fresh arrow supplied to `app` at each instant obviously cannot accumulate state?

It's not about the laws, it's about losing state.

Yampa AFRP model chooses to model products using the `Either` type - i.e. indicating that either element can be updated independently. Using this, one could accumulate state in the captured arrow, though there'd be a funky reset whenever the arrow is updated.

Of course you can make a trade-off, but I don't think it's possible to solve this in a clean way in the automaton model.

The reactive model I'm developing, Reactive Demand Programming, is actually anti-causal: behavior at any given instant may depend only upon its present and future inputs (anticipation), but never the past. State is treated as an external service, part of an abstract machine, orchestration of registers or a database. I think this setup works better than FRP, e.g. for controlling space-leaks, supporting smooth transitions and upgrades of dynamic behavior, modeling the app as a whole as dynamic, and orthogonal persistence.

I would be very interested in such a model. Are there any resources online? Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/

David Barbour wrote:

Alan Jeffrey wrote:

...

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

Yes. Function outputs only depend on the past values of the input function.

Your solutions for double and weird are accurate. Double is lifting the future at each instant into the present, which is obviously not causal. And the `weird` function presumes you already have a obtained a complete view of a behavior at each instant.

The `problem` such as it exists: you will be unable to causally construct the argument to 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.

I concur with that. The function double :: Behavior a -> Behavior (Behavior a) double x = const x is not causal because it makes all future values of the behavior x available "at once". However, weird :: Behavior (Behavior a) -> Behavior a weird = join . fmap (. (+1)) where join a t = a t t is clearly causal as a composition of two causal functions. The point is that the innermost behavior was already available "in full", so it's perfectly possible to evaluate it at any time desired. Of course, the function double' x t = \t' -> if t' <= t then x t' else _|_ is causal. Best regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com

On Fri, Oct 14, 2011 at 7:27 AM, Alan Jeffrey wrote:

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

...

On Thu, Oct 13, 2011 at 7:54 AM, Alan Jeffrey mailto: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 [snip]

Making worlds explicit like this I think helps clarify why one person's "weird" is another person's "perfectly reasonable function" :-)

Well, I think you have the concept right. But `weird` is always causal. The burden of violating causality has been shifted to the user of weird. Regards, Dave

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.