Causal Semantics of (A)FRP

March 8th, 2010 by Neil Sculthorpe

Having being inspired by Conal Elliott’s blog post about the inaccuracy of the (Arrowised) FRP semantical model, I was trying to find as simple a model as possible that is inherently causal.

The basic concept in FRP is of time-varying values called signals (or behaviours):

Signal : Set -> Set
Signal A = Time -> A

Where Time is the non-negative real numbers.

In Arrowised FRP there are then Signal Functions, conceptually functions between signals:

SF : Set -> Set -> Set
SF A B = Signal A -> Signal B

Signal functions are nicely modular, and AFRP programs are constructed by composing signal functions together.

As an example of a signal function, consider “delay”, which delays an input signal by a specified amount of time:

delay : Time -> SF A A
delay d = \ s t -> s (t - d)

The problem with this semantics of SF, is that it isn’t inherently causal. One could define a “future” signal function that is similar to delay, but produces the future input as the current output.

future : Time -> SF A A
future d = \ s t -> s (t + d)

In FRP we want to always be able to produce the current output from the current and past inputs, so this is bad.

Consequently, a causality constraint is usually placed on signal functions. All primitive signal functions must be causal, and all primitive combinators must preserve causality.

Causality can be defined:

Causal : SF A B -> Set
Causal sf = (s1 s2 : Signal A) -> (t : Time) -> ((t' : Time) -> (t' <= t) -> (s1 t' == s2 t')) -> (sf s1 t == sf s2 t)

So a causal signal function is a product of the signal function and the causality property:

CausalSF A B = Sigma (SF A B) Causal

I was hoping to find a model of AFRP that is inherently causal, and so doesn’t require the addition of a causality property on top of it. Starting from the definition of SF:

SF A B = Signal A -> Signal B
{expanding}
SF A B = (Time -> A) -> (Time -> B)
{flipping arguments}
SF A B = Time -> (Time -> A) -> B
{constraining the input signal}
SF A B = (t : Time) -> ((t' : Time) -> (t' <= t) -> A) -> B

We’re now constraining the input signal. We are now only required to know the input signal up to the point in time at which we are sampling the output.

As far as I can tell, this is now inherently causal, and it seems to work out okay for defining primitives. For example, composition is:

_>>>_ : SF A B -> SF B C -> SF A C
sf1 >>> sf2 = \ t sa -> sf2 t (\ t' ltB -> sf1 t' (\ t'' ltA -> sa t'' (transitive ltA ltB)))

However, so far we’ve only considered continuous signals. FRP also contains discrete signals, most notably events. Events only occur at certain points in time, and the event signal is undefined elsewhere. We require that only a finite number of events occur within any finite interval. This can be modelled as a (co)list of time-delta/value pairs:

EventSignal : Set -> Set
EventSignal A = List (Dt , A)

where Dt is the type of positive Time, representing the time since the previous event occurrence.

We can incorporate this into the original model by parametrising signals with a signal descriptor that contains this time-domain information (rather than just a Set):

data SigDesc : Set1 where
C : Set -> SigDesc
E : Set -> SigDesc

Signal : SigDesc -> Set
Signal (C A) = Time -> A
Signal (E A) = List (Dt , A)

SF : SigDesc -> SigDesc -> Set
SF x y = Signal x -> Signal y

However, it doesn’t work with the causal version, as we don’t have the same Signal types. Once we’ve put the time constraint on, we really have a signal history. That is, a signal indexed by some finish time:

SignalHistory : SigDesc -> Time -> Set
SignalHistory (C A) t = (t' : Time) -> (t' <= t) -> A
SignalHistory (E A) t = EventList A t

where an EventList is just a list of time-delta/value pairs with an added constraint that the sum of all the time deltas does not exceed the index. (If anyone can suggest a better datatype for this then please do so; this is just the first one that came to mind.)

data EventList (A : Set) : Time -> Set where
[] : {t : Time} -> EventList A t
cons : {t t' : Time} -> (d : Dt) -> A -> EventList A t'
-> (t' + d) <= t -> EventList A t

Returning to our signal function definition, we can now define signal functions for either kind of input signal, but only continuous output signals:

SF : SigDesc -> SigDesc -> Set
SF x (C B) = (t : Time) -> SignalHistory x t -> B
SF x (E B) = ?

And that’s where I got stuck stuck.

I did consider:

SF : SigDesc -> SigDesc -> Set
SF x y = (t : Time) -> SignalHistory x t -> SignalHistory y t

but this isn’t properly causal. It is to some degree (at any given point in time, the output signal history does not depend upon future input), but there’s nothing preventing the past from being rewritten later (because at each point in time a new signal history is produced, which may or may not be consistent with previous histories).

6 Responses to “Causal Semantics of (A)FRP”

  1. Noam Lewis Says:

    Hi,
    I’ve just been thinking about similar things. I’ve summarized my ideas in

    http://www.ee.bgu.ac.il/~noamle/_downloads/gaccum.pdf

    Unfortunately I can’t understand most of the post (is this in Agda? Is it possible to summarize the constraints with traditional mathematical notations?)

    My approach is more limiting, I am not only prohibiting systems to causality – but also to not being able to access values at arbitrary times (even if it’s the past). On the other hand I do want to allow “memory-full” operations. The only way I found to do this is by considering the *interface* I would like the semantic model of signal functions to have. I’ve yet to find a model that naturally imposes the above limitation, but allows memory-full operations. See the above report for more details :)

    - Noam

  2. Noam Lewis Says:

    As a side note, the approach I took was inspired by another of Conal’s blog posts: http://conal.net/blog/posts/garbage-collecting-the-semantics-of-frp/

    Additionally, I also avoid the problem of “rewriting history”, because the interface I allow is inherently point-wise, also in the output. Another consequence is that time delay can’t be expressed using this interface, but I’m not sure that’s a bad thing.

  3. Noam Lewis Says:

    I just noticed that we’re quoting the same blog post. Never mind :)

  4. Neil Sculthorpe Says:

    Yes, it’s Agda notation.

    As a quick guide:

    `Set’ is similar to kind `*’ in Haskell.

    Datatypes are defined GADT style.

    There’s no restrictions on the use of upper and lower case letters, but I tend to capitalise the first letter of type constructors.

    A dependent function of type:

    (s : Time) -> (s < = t) -> A

    is similar to a non-dependent function of type:

    Time -> A

    with the constraint that the Time argument must be less than or equal to `t’. ((s <= t) is the type of proofs that the value `s’ is indeed less than or equal to the value `t’. The dependent version of the function requires this proof as an additional argument)

  5. Alba Marchisio Says:

    Hi All.
    I don’t know very well Agda (my fault, I know), and my question is about how many Agda notation is related with Yampa notation. Is the AFRP notation completely supported in FRP.Yampa?

    Sorry if my question is particulary stupid, but I’ve just started using Yampa and I stil a bit cunfused about notation.

    Bye.

    Alba.

  6. Neil Sculthorpe Says:

    Hi Alba

    I’m not entirely sure what you mean.

    AFRP was the original name of Yampa.

    Yampa is embedded within Haskell, so much of its syntax is Haskell syntax.
    One could embed Yampa, or a Yampa-like FRP language in Agda. The notation will differ slightly, as Agda has some syntactic differences from Haskell. There aren’t any Agda implementations suitable for FRP programming at the moment (that I am aware of), though I have used Agda to prototype several FRP variants with extended type-systems.

    However, the above post was about defining the semantics of FRP, not its implementation.

    In the Haskell embedding, Yampa makes use of the Arrows Framework, and the Arrow Notation that GHC supplies to go with it. To use the Arrow Notation you need to use the appropriate GHC extension:

    {-# LANGUAGE Arrows #-}

    Agda doesn’t provide Arrows in its standard library, but they can easily be defined. The Arrow Notation on the other hand would be harder, though something close should be possible as Agda is pretty liberal in terms of user-definable syntax.

Leave a Reply