[w4-structure-editors] Added initial draft version #11
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
The image should work out -- otherwise we will help you serve it from an external site. |
topics/w4-structure-editors.md
Outdated
|
|
||
| #### 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**. |
There was a problem hiding this comment.
I like the intro! The infinite monkey theorem is very engaging
topics/w4-structure-editors.md
Outdated
| #### 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... 👀). |
There was a problem hiding this comment.
It's a good coverage of work on the history of structure editing before the hazel paper
topics/w4-structure-editors.md
Outdated
| - 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. |
There was a problem hiding this comment.
Perhaps you can also discuss the other challenges come with structure editing, either before or after the introduction of Hazel
topics/w4-structure-editors.md
Outdated
|
|
||
| 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. |
There was a problem hiding this comment.
I am curious on what you think about structure editing as the future of programming --- do you think this will be a mainstream way of programming? or what stops it from being a mainstream way of programming?
There was a problem hiding this comment.
What about AI-assisted programming? Can structure editing improve the way of how programmers validate and steer code generated by AI?
BILLXZY1215
force-pushed
the
main
branch
2 times, most recently
from
f0153b8 to
e106008
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
My initial version of the post. I go into a bit more detail on Hazel as I find its contribution with typed lambda calculi very interesting and see many applications of it.
Technical
I want to include some figures in my post, I just created a new folder and put them all there with relative links in my blog post. Let me know if I should handle image files differently (I saw the homepage directly contains the raw base64 image data). In case the images can be left as files, also let me know if we should use Git LFS for images (would require modifying
.gitattributes).Looking forward to your feedback!
Best,
Federico
P.S.: My ETH email is [email protected], I'm unfortunately using my personal GitHub account as I don't have an ETH one.