OK so there's this thing called FRP
- Functional Reactive Programming
- Building programs that vary in time out of Signals and Events
- Signals, Events
- these are objects that you can work with, and you have a set of combinators for making new signals out of old signals, etc,
And existing implementations -- I haven't looked at every existing implementation, but the ones I have looked at -- either don't allow you to create Signals dynamically (ie all your signals are there at program initialization), or have problems with memory management.
and the problems with memory management come because you have Signals implemented in terms of callbacks, which must use weak pointers, so, even though you can't technically overflow the heap this way, you're relying on the underlying garbage collector to stop active behavior -- to stop events from firing.
So I was thinking, we can do better -- one way we can do better, at least -- is if we drop Signals and Event streams for now and focus on one-shot events, because these have a definite expiration attached to them -- once the one-shot has fired you no longer need to hold on to it, so that should improve the memory situation a little bit.
And in addition to that, we can write down a set of axioms that are obviously true of events, so that if we target an implementation to the axioms in a minimal way, we can limit ourselves to only necessary screw-ups, avoiding superfluous screw-ups not required be the axioms.
So, my first attempt goes,
Events1.agda 1 -- https://lists.chalmers.se/pipermail/agda/2010/002484.html 2 -- https://lists.chalmers.se/pipermail/agda/2010/002485.html 3 {-# OPTIONS --no-positivity-check #-} 4 {-# OPTIONS --no-termination-check #-} 5 {-# OPTIONS --type-in-type #-} 6 7 -- Compiled against standard library 0.6 8 module Events1 where 9 10 open import Data.Sum using (_⊎_; inj₁; inj₂) 11 open import Data.Product using (_×_; proj₁; proj₂; _,_) 12 13 record EventSystem : Set where 14 infixl 5 _map_ 15 field 16 -- The type of a one-shot event, ie it does not repeat. 17 Event : (result-type : Set) → Set 18 19 -- Axioms of Events 20 21 -- Basic map. 22 _map_ : ∀ {r₁ r₂} (ev : Event r₁) (f : r₁ → r₂) → Event r₂ 23 24 -- Wait for the latter of one or two events. 25 chain : ∀ {r} (ev : Event (r ⊎ Event r)) → Event r 26 27 -- For any two events, one of them happens first. 28 order : ∀ {r₁ r₂} (ev₁ : Event r₁) (ev₂ : Event r₂) 29 → Event ((r₁ × Event r₂) ⊎ (r₂ × Event r₁))
and I believe -- and you can look at these and tell me if I'm right or not -- but I believe that these are obviously true -- in a single-threaded, non-relativistic world. The order axiom is obviously not true in a multi-threaded world, where in waiting for the first of two events you may miss the second.
So. The first thing I notice, is that we're very close to having a monad, except we're missing pure, and chain aka join has that funny union type.
Well, I had a very good reason for not including pure. When I was writing this I was very worried about having a way to create an event in a side-effectless manner, which is what pure is. I wanted every event to be grounded to another event, so you never had events as pure objects just floating around. I even considered a cojoin-like definition
main 1 instantly : ∀ {r} → Event r → Event (Event r)
except that that turned out not to be very useful for writing actual programs.
But anyway, I remembered after writing this that applicatives don't need pure, and you can see how you can use that same exact trick for monads, so we can forgive ourselves for writing it like this:
1 record EventSystem : Set where 2 infixl 5 _map_ 3 field 4 Event : (result-type : Set) → Set 5 6 instantly : ∀ {r} (x : r) → Event r 7 8 _map_ : ∀ {r₁ r₂} (ev : Event r₁) (f : r₁ → r₂) → Event r₂ 9 10 chain : ∀ {r} (ev : Event (Event r)) → Event r 11 12 order : ∀ {r₁ r₂} (ev₁ : Event r₁) (ev₂ : Event r₂) 13 → Event ((r₁ × Event r₂) ⊎ (r₂ × Event r₁))
Now, honestly, I like the first rules better. The first rules are obviously true, in my opinion, whereas with the second rules we have to do more self-convincing. But monads are ubiquitous and there's no use in fighting a monad when you have a monad, so we go with the monadic Event, plus the order axiom.
(Though we should remember, if we're ever going to implement these axioms, the fact that we had to use a disjoint union to convince ourselves that instantly is valid is a clue that we will need to special-case constant signals).
Now these axioms, despite what I still insist is there obvious trueness, have a serious problem. Let's say I have two events
2 x : Event ⊤ 3 y : Event ⊤
and I use the Event axioms to derive
4 xy = chain (x map (λ _ → y)) 5 yx = chain (y map (λ _ → x))
which intuitively mean "wait for x to happen, then wait for y to happen", and "wait for y to happen, then wait for x to happen." Now one of these must hang. Either x comes first or y comes first, and if x comes first and you wait for y, then wait for x, the second waiting will never occur.
Now I claim that this does not falsify the Event axioms. An event that never returns is not illegitimate -- you could still have an event resulting in ⊤ that never comes to pass in the same way you can have a function returning ⊤ that goes into an infinite loop and never returns. It would result in ⊤ if it ever resulted in anything.
So we have to ask ourselves a question. Is this a problem worth fixing? Because if we're going to fix it, we're going to have to introduce extra restrictions in the Event axioms AND, critically, it will be impossible to make Event a monad, since we used only monad combinators to derive a never-occurring event, so we'd be giving up on a good deal of friendly generality by giving up on the monad.
But if I just think back to how often my interactive programs hang up waiting for events in the wrong order, the answer is "a lot". This is actually a pretty common problem. This is actually something we could stand to benefit from in the Event laws. Here is an attempted fix:
SafeEvents.agda 1 {-# OPTIONS --type-in-type #-} 2 {-# OPTIONS --no-positivity-check #-} 3 {-# OPTIONS --no-termination-check #-} 4 5 module SafeEvents where 6 7 open import Data.Sum using (_⊎_) 8 open import Data.Product using (_×_) 9 10 π : {T : Set} → (T → Set) → Set 11 π {T} A = (t : T) → A t 12 13 record EventSystem : Set where 14 field 15 -- Time is probably not going to be represented by a Double or Int. It's not a "time" so 16 -- much as a handle for getting at events. 17 Time : Set 18 19 -- We don't really care what this means. 20 min : Time → Time → Time 21 22 Event : (A : Time → Set) → (t : Time) → Set 23 24 -- An event that happens without delay. 25 instantly : ∀ {t A} (x : π A) → Event A t 26 27 -- This is like usual map, but be careful, you also get a time. 28 _map_ : ∀ {t A B} (ev : Event A t) (f : ∀ {t} → A t → B t) → Event B t 29 30 -- This represents waiting for the second of two events. 31 chain : ∀ {A t} → Event (Event A) t → Event A t 32 33 -- Total ordering: for any two events, one happens first, and the other second. 34 order : ∀ {A₁ A₂ t₁ t₂} (ev₁ : Event A₁ t₁) (ev₂ : Event A₂ t₂) 35 → Event (λ t → (A₁ t × Event A₂ t) ⊎ (A₂ t × Event A₁ t)) (min t₁ t₂)
These axioms, I think, are not so obvious, so they require some explanation.
First, Event now takes a Time parameter in its type:
6 Event : (A : Time → Set) → (t : Time) → Set
t is not the time at which the event happens; it is some time before the event happens. ie, an Event A t is an event that results in A after time t. So if t₁ comes before t₂, for example (a property not describable by these axioms), an event t₂ could also plausibly be an event t₁ -- though we have no axioms to get at this concept.
Now, instantly is written differently:
7 instantly : ∀ {t A} (x : π A) → Event A t
The π is hiding some things; this could be written
8 instantly : ∀ {t A} (x : (t : Time) → A t) → Event A t
In other words, the argument you give to instantly should be a function taking a Time as its argument, and returning a result whose type depends on that time. I say "should" rather than "must" because you can see that this is not actually a restriction on the caller -- x is free to ignore the time and return the same result it would have anyway; this type of instantly is actually more powerful and less general than the old one.
Here is how _map_ turned out:
9 _map_ : ∀ {t A B} (ev : Event A t) (f : ∀ {t} → A t → B t) → Event B t
There might be a more useful way to write map, one that gave f more access to the times, but I was worried that could create a problem, so I stuck pretty close to the usual _map_ definition.
But chain holds the difference from the old Event laws, and this is more restrictive on the caller:
10 chain : ∀ {A t} → Event (Event A) t → Event A t
Some of the parameters have been eta-removed, making it look suspiciously monadic, but this can be written as:
11 chain : ∀ {A t} → Event (λ t′ → Event A t′) t → Event A t
In other words, you can chain an event producing an event provided that the inner event is constructed based on any time. This is giving me some kind of hints that times need types associated with them -- maybe Time actually represents an observable object -- but I'm not sure what to do about that right now.
And lastly, order gives us the kind of useful information needed to call chain:
12 order : ∀ {A₁ A₂ t₁ t₂} (ev₁ : Event A₁ t₁) (ev₂ : Event A₂ t₂) 13 → Event (λ t → (A₁ t × Event A₂ t) ⊎ (A₂ t × Event A₁ t)) (min t₁ t₂)
And we can verify that the necessary information is contained in order by writing a second function to get the second of two events:
14 second : ∀ {r t₁ t₂} → Event r t₁ → Event r t₂ → Event r (min t₁ t₂) 15 second ev₁ ev₂ = chain (order ev₁ ev₂ map λ { 16 (inj₁ (r , next)) → next; 17 (inj₂ (r , next)) → next 18 })
And that works. And now we have time-safe events.
