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.

## No comments:

## Post a Comment