by Neil Sculthorpe on March 8, 2010.
Tagged as: Lunches.
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).