[Haskell-cafe] A question about causality in FRP

[Alan Jeffrey]

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