[w4-structure-editors] Added initial draft version

topics/w4-structure-editors.md

@@ -1,10 +1,40 @@
-# W4 - Structure Editors
+![typing_monkey_upscaled](./w4-structure-editors.assets/typing_monkey_upscaled.png)
 
-### Reading List
+# Structure Editors -- Formal Language Theory for Provably Correct Program Analysis
 
-#### Required Reading
-* [Hazel](https://hazel.org/): Omar, C., Voysey, I., Hilton, M., Aldrich, J., & Hammer, M. A. (2017). Hazelnut: a bidirectionally typed structure editor calculus. ACM SIGPLAN Notices, 52(1), 86-99.
+There is a famous theorem, called the "infinite monkey theorem"[^1], which states that an immortal monkey typing at random on a typewriter, for an infinite amount of time, will eventually reproduce every single work of literature ever written, including complete works of William Shakespeare. The same statement can also be applied to a monkey programmer typing on a computer keyboard, that will eventually write every single correct program, including ones that offer solutions to problems we have not managed to solve yet. However, hopefully, most programmers cannot and should not be likened to a typing monkey. Indeed, the number of valid programs, although infinite, is vanishingly small in comparison to all possible combinations of symbols. As such, programmers need to take great care to produce a valid program. Unfortunately, this has the downside that we as programmers inherently need to know, which programs are valid and which ones aren't. Especially for beginner programmers this can distract from learning the actual essence of programming, which does not care for any syntactical trivialities, as these result from our limitations in effectively communicating with computers. In this spirit, let's build a special kind of typewriter, that instead of producing garbage text most of the time, **always** produces a **valid program** with every keystroke. This special typewriter encapsulates the main concept behind **structure editors**.
 
-#### Optional Reading
-* [Polymorphic Blocks](https://cseweb.ucsd.edu/\~lerner/poly-blocks.html): Lerner, S., Foster, S. R., & Griswold, W. G. (2015, April). Polymorphic blocks: Formalism-inspired UI for structured connectors. In Proceedings of the 33rd Annual ACM Conference on Human Factors in Computing Systems (pp. 3063-3072).
-* [Envision](https://www.pm.inf.ethz.ch/research/envision.html): Asenov, D., Hilliges, O., & Müller, P. (2016, May). The effect of richer visualizations on code comprehension. In Proceedings of the 2016 CHI Conference on Human Factors in Computing Systems (pp. 5040-5045).
+Early works in the field of structure editors include the Cornell Program Synthesizer[^2], in which the authors note that programs are not simply text, but instead complex syntactical structures, which should also be edited, executed, and debugged as such. Perhaps the most well-known structure editor is Scratch[^3], which allows users to drag-and-drop program blocks to form a program. Researchers have tried a number of variations on this concept, including hybrid approaches such as Envision[^4], which allows users to switch between graphical and textual representations of code, and quickly scaffold common program structures with keyboard commands. Unfortunately, such visual code editors get impractical and slow when working with larger projects in professional environments. The workflow they provide is simply too rigid for efficient use. For this reason, programmers try to minimize the use of graphical tools, and work exclusively through textual interfaces (looking at you, Vim users... 👀).
+
+![ucpi-final-blog-structure-editors](./w4-structure-editors.assets/ucpi-final-blog-structure-editors.png)
+
+At this point, it we seem to have conflicting interests:
+
+- On one hand, we want to completely eliminate invalid program states, making it impossible to produce syntactically incorrect code. This would allow us to reason about the code in a provably correct fashion at all times.
+- On the other hand, we want to allow programmers to interact with code in the way they are used to, namely through textual edits, minimizing the time and mental load required to switch to a new editing environment.
+
+Inevitably, as you write a program, not all states will be valid programs. The text might contain errors and missing parts. But as it turns out, it is indeed possible to reconcile these two goals, which is exactly what the researchers behind the Hazel[^5] programming environment did. Instead of looking at programs as just text, which either is a valid program or not, we can treat *every* text as valid, and augment the program text with "blanks" (referred to as "holes" in Hazelnut), which the programmer still needs to fill out or correct. While the underlying program written in Python or Haskell might contain mistakes, the program text is still a valid program in the Hazelnut formalism (now called an **edit state**). If additionally we treat a program not as a collection of syntactical tokens, but instead as a sequence of **edit actions** that the programmer made to produce the program, we effectively created a system where the programmer can write code as usual, but *every* edit state is a valid state. In short, this means that no matter what the programmer types, and no matter how wrong the underlying program may be, the text is still a valid program in the Hazelnut formalism.
+
+It is conceptually quite easy to implement an editor for such a formalism such as Hazel: We need to define some sort of empty edit state, and translate user inputs (e.g. key presses) into edit actions, which in turn transform the current edit state into another edit state. We can derive the underlying program from an edit state and display it in the editor; However, at this point we have a formal understanding of the semantics of the program, such as which parts are correct or where there is some missing code. This differs quite strongly from the way such diagnostics are usually implemented in code editors, which rely entirely on heuristics to infer the user's most likely intent.
+
+![hazel-schematic](./w4-structure-editors.assets/hazel-schematic.png)
+
+Under the hood, Hazel is implemented through a bidirectionally typed structure editor calculus. What exactly this means is irrelevant, but the gist of it is that we use tools from formal type theory, especially typed lambda calculi, to formally define the semantics and well-typedness of a given program. In hazelnut, starting from a well-typed edit state, it is impossible to apply an edit action in such a way that the resulting edit state is ill-typed, giving a provable guarantee for correctness. You can try the Hazel editor in action on https://hazel.org/build/dev/.
+
+While in my personal experience the benefits of the method are not immediately apparent from the paper and the live demo the authors provide, other works have used this framework to implement provably correct editor diagnostics features. For example, it is possible to leverage the formal grammar to provide a better starting point for code auto-completion, as the required type for program holes is known[^6]. Another possible application is something that is close to my heart as a web developer: Type error localization. Anyone who has worked with TypeScript professionally knows the horrors that the TypeScript type system is able to produce:
+
+![enter image description here](./w4-structure-editors.assets/YbG9Q.png)
+
+Such errors are utterly unreadable leading to developers simply ignoring the error message, and relying on their common sense or other heuristics to find the error. We can leverage the information given by type holes (which represent missing or incorrect types in a partial program) to provide more localized and meaningful information about a given type error, pinpointing the error to the developer[^7].
+
+In conclusion, structure editors provide a more natural, and often also more principled approach to code editing. Programming languages are designed to be easily understandable by computers, with the side effect of having a very rigid syntax, which we can exploit to our advantage. With structural editing, aspiring programmers can easily reason about program logic without having to worry about the strict confinements of program syntaxes. While most structure editors focus on minimizing the number of invalid program states during development, Hazel takes this concept a step further by introducing "holes", augmented with additional type information about incorrect or incomplete programs. A big advantage of Hazel is its closeness to traditional editing environments, which makes it easier for experienced programmers to adopt. By integrating structural editing techniques in existing code editors, we can provide provably correct code diagnostics such as auto-completion and type error localization, possibly increasing overall code quality and speed of development.
+
+## References
+
+[^1]: Borel, É. (1913). La mécanique statique et l'irréversibilité. *J. Phys. Theor. Appl.*, *3*(1), 189-196.
+[^2]: Teitelbaum, T., & Reps, T. (1981). The Cornell program synthesizer: a syntax-directed programming environment. *Communications of the ACM*, *24*(9), 563-573.
+[^3]: Resnick, M., Maloney, J., Monroy-Hernández, A., Rusk, N., Eastmond, E., Brennan, K., ... & Kafai, Y. (2009). Scratch: programming for all. *Communications of the ACM*, *52*(11), 60-67.
+[^4]: Asenov, D., & Muller, P. (2014, July). Envision: A fast and flexible visual code editor with fluid interactions (overview). In *2014 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC)* (pp. 9-12). IEEE.
+[^5]: Omar, C., Voysey, I., Hilton, M., Aldrich, J., & Hammer, M. A. (2017). Hazelnut: a bidirectionally typed structure editor calculus. *ACM SIGPLAN Notices*, *52*(1), 86-99.
+[^6]: Pelsmaeker, D. A., van Antwerpen, H., Poulsen, C. B., & Visser, E. (2022). Language-parametric static semantic code completion. *Proceedings of the ACM on Programming Languages*, *6*(OOPSLA1), 1-30.
+[^7]: Zhao, E., Maroof, R., Dukkipati, A., Blinn, A., Pan, Z., & Omar, C. (2024). Total type error localization and recovery with holes. *Proceedings of the ACM on Programming Languages*, *8*(POPL), 2041-2068.