intro.tex

%!TEX root = dynamics-obt17.tex

Programming language definitions assign meaning to \textit{complete}
programs. Programmers, however, spend a substantial amount of time
interacting with \textit{incomplete} programs, using tools like program
editors or live programming environments that interleave editing and
evaluation. Semanticists have paid comparatively little attention to these
interactions, so the designers of tools like these lack foundational
principles comparable to those available to language designers. For
example, Agda does provide a notion of incomplete programs and a mechanism
to evaluate terms with holes in them, but it fails as soon as it actually
encounters a hole~\cite{norell:thesis}.

In our paper describing the Hazelnut structure editor, appearing at POPL
2017, we consider the static semantics of incomplete programs,
i.e. programs with holes in expressions and types~\cite{hazelnut:popl}. We
also introduce a notion of non-empty hole, which serves to safely
encapsulate putative subexpressions whose types may not yet be consistent
with the type that is expected. The ``beaten track'' strategy would be to
define a dynamics only for programs without holes, or to have holes act
like exceptions and end evaluation. Instead, our ``off the beaten track''
suggestion is to continue evaluation past a hole, revealing more about the
dynamic behavior of the incomplete term. This could benefit programmers by
tightening the feedback loop between editing and evaluation, even beyond
what is available in current live programming tools~\cite{burckhardt2013s}.

The main technical challenge is to recover a meaningful notion of type
safety---we seek recognizable statements of progress and preservation for
terms with holes in them, with respect to a dynamic semantics that matches
our intuition.

In the ideal system, a Hazelnut programmer writes their program with
confidence that her edits are all safe. When she arrives at a candidate,
possibly incomplete, program that she wants to explore more, she can run it
on specific values and observe how the holes in her program are actually
used in evaluation. She can then return to editing the program, working
towards a complete program with better insight into how the concrete values
of variables are used. This insight can help her develop intuition about
how to fill each hole in the incomplete program.