Hacker News Reader

Comment by lstyls | Hacker News Reader

What I got from this paper is that the authors are using a flavor of symbolic logic called "temporal logic" to formalize concepts fundamental to the event-driven programming paradigm. The notation seems to make intuitive sense as an extension to the formal logic I learned in my undergraduate discrete math course.

I'm not all the way through the paper but I actually find it quite helpful in explaining the essential meaning of these concepts. I haven't worked with these concepts much, and the tutorials I've read in my free time have focused more on practical use of various implementations of eg futures rather than explaining their actual abstract meaning.

Caveat: I am not familiar with this academic domain so this is my own interpretation. If someone who is better versed can elaborate or correct me, please, please do so.

View on HN

That's pretty accurate! (I'm one of the authors.)

In event-based programming, one of the basic abstractions are something variously called "events", "futures", or "promises". The idea of a future is that it is a data structure that can yield a value at some point in the future, but not might be ready to produce one right away. This idea dates back to (at least) MultiLisp and the Connection Machine, but many modern languages support this primitive -- for example, Javascript, Rust, Ocaml, C#, Java and Scala all have good library support for it.

Our basic idea is that futures correspond very closely to the interpretation of the "eventually" operator in temporal logic. So if we could give a typed lambda calculus for temporal logic, then we could implement the eventually operator with futures. The benefit of doing this is that we could design languages which combine the easiness of reasoning featured by purely functional programming, while still offering good support for event-based programming (eg, for GUIs). In addition, if we are coming from a typed language that has enough invariants, we can also simplify the implementation of futures (since we know statically that certain problems like deadlock can't arise).

My personal goal is to figure out the fundamental primitives of interactive programming. Ultimately I'd like to be able to go from a framebuffer to a comfortable GUI toolkit in a few hundred lines of code, so that teaching the principles of how to implement these things can fit into a semester-long course. (Since there is a fairly small limit on how much code a student can reasonably write/comprehend in a term, the better we understand a problem the more we can teach.)

Very nice explanation.

> we could design languages which combine the easiness of reasoning featured by purely functional programming, while still offering good support for event-based programming (eg, for GUIs).

Are there any particular difficulties (or niceties!) when these are combined?

For example, does this cause implementation details to leak, like requiring the programmer to choose between multiple definitions of things like function types: "a -> b", "a -> eventually b", "eventually a -> b", "eventually a -> eventually b", "a eventually-> b", "a eventually-> eventually b", ....?

Does it make reasoning easier or harder, e.g. regarding resource usage (space leaks, lazy IO, etc.)? How does it compare to lazy evaluation?

If someone uses events internally to a library, e.g. to read from some stream, could they encapsulate that such that users of their API wouldn't have to notice/care about the events? I'm picturing something like exceptions, or lazily-evaluated IO values, which can trigger errors inside seemingly pure code, e.g. like in Haskell where the `readFile` call in `do { content <- readFile "foo.txt"; return (toUpperCase content); }` might work fine, but then an IO error is triggered inside the pure `toUppercase` function. Would such things cause reasoning problems about futures?

Well, one can imagine a smart enough language could perform some trivial mappings to reduce the zoo of potential function types: a -> b can be trivially mapped to both (a -> eventually b) and (eventually a -> eventually b).

Really good stuff. The GUI is often where the ease of reasoning breaks down and I'm glad to see work like this trying to change that.

Just realized that this is not even close to "like I'm five". Least bad thing I can come up with:

It's math for lazy computers talking to each other.

It's a formal specification of the concepts you are used to use on GUI programing.

Reply on news.ycombinator.com