evincarofautumn / hap-hs

Haskell [re]implementation of Hap, a simple event-based programming language.
MIT License
12 stars 2 forks source link

Temporal analysis #5

Open evincarofautumn opened 4 years ago

evincarofautumn commented 4 years ago

Hap seems amenable to formal analysis using a temporal modal logic, which might offer improvements to ergonomics and performance.

As for performance, the main thing we care about is probably preventing event leaks, that is, we shouldn’t retain event listeners for events that can never happen. Currently, one proxy for this is that we remove a listener when the cells it references expire (via weak references), or when it depends on the presence of a cell in a collection, and the cell is removed (via removal events). However, this doesn’t identify cases where an event could occur, but will never occur because there’s no code path that will ever modify a cell in such a way that its listeners could trigger. In general this is undecidable, because conditions can include arbitrary code. Although maybe they shouldn’t be able to—at least conditions should almost certainly be free of effects, and should probably be total, even though we can support effects and follow-up events without too much trouble.

We should (unfortunately) expect to retain most listeners in interactive mode, since there is new code continually arriving that could make a heretofore impossible event become possible. That may lead to slowdowns in long-running interactive sessions. But in batch mode, we’ll generally have the whole program at hand, and be able to analyse it exhaustively. (I don’t know if separate compilation makes sense at all; we shouldn‘t rule it out, but it’s not a primary goal.)