Toward a Live Stepper for Typed Expressions with Holes
To understand the dynamic behavior of an expression, programmers can use a “stepper” to interactively simplify the expression according to the dynamic semantics of the programming language. The problem that motivates this work is that a standard dynamic semantics assigns meaning only to complete, well-typed expressions, but there are situations where a programmer might want to explore the dynamic behavior of an expression well before it is complete. This paper proposes the development of a dynamic semantics for incomplete expressions, which we take to mean expressions with holes. Holes indicate portions of the expression that have yet to be filled in, or, following our recent work (Omar et al. 2017a), that have a local type inconsistency that has yet to be resolved. The result would be a program editor where the programmer has access to the stepper at all times, not just when the program is in a complete state, and where evaluation does not stop immediately at the hole, but rather proceeds as far as possible past the hole.
Even this would not be entirely satisfying when engaging in live programming, where editing and evaluation are interleaved, because naively, the programmer would need to restart the stepper aer each edit. To address this problem, this paper further proposes a mechanism that tracks the dynamic environment around each hole as well as its evaluation status. This allows for the specification of a live stepper, i.e. a stepper where evaluation can continue where it left off even after holes are filled in, because the current state of the stepper can be “patched” to accurately reflect each edit that was made.
This paper reports early conceptual progress in these directions. Many details have yet to be considered. We hope to discuss both the human aspects and the formal aspects of the design with the workshop participants
Tue 24 Oct
|10:30 - 11:20|
|11:20 - 11:40|
|11:40 - 12:00|
|Pre-print Media Attached|