Editor Arrow: An arrow-based model for editor-based programming

摘要

State-based interactive applications, whether they run on the desktop or as a web application, can be considered as collections of interconnected editors of structured values that allow users to manipulate data. This is the view that is advocated by the CEC and iData toolkits, which offer a high level of abstraction to programming desktop and web GUI applications respectively. Special features of these toolkits are that editors have shared, persistent state, and that they handle events individually. In this paper we cast these toolkits within the Arrow framework and present Editor Arrow: a single, unified semantic model that defines shared state and event handling. We study the properties of Editor Arrow, and of editors in particular. Furthermore, we present the definedness properties of the combinators. A reference implementation of the Editor Arrow model is given with some small program examples. We discuss formal reasoning about the model using the proof assistant Sparkle. The availability of this tool has proved to be indispensable in this endeavor.