Pantograph: A Fluid and Typed Structure Editor

TL;DR

A novel generalization of selection for tree-based structures that properly generalizes text-based selection and editing, allowing users to freely rearrange pieces of code by cutting and pasting one-hole contexts and exploring the metatheory of the system that arises for maintaining well-typedness systematically.

Abstract

Structure editors operate directly on a program's syntactic tree structure. At first glance, this allows for the exciting possibility that such an editor could enforce correctness properties: programs could be well-formed and sometimes even well-typed by construction. Unfortunately, traditional approaches to structure editing that attempt to rigidly enforce these properties face a seemingly fundamental problem, known in the literature as viscosity. Making changes to existing programs often requires temporarily breaking program structure -- but disallowing such changes makes it difficult to edit programs! In this paper, we present a scheme for structure editing which always maintains a valid program structure without sacrificing the fluidity necessary to freely edit programs. Two key pieces help solve this puzzle: first, we develop a novel generalization of selection for tree-based structures that properly generalizes text-based selection and editing, allowing users to freely rearrange pieces of code by cutting and pasting one-hole contexts; second, we type these one-hole contexts with a category of type diffs and explore the metatheory of the system that arises for maintaining well-typedness systematically. We implement our approach as an editor called Pantograph, and we conduct a study in which we successfully taught students to program with Pantograph and compare their performance against a traditional text editor.

Figures (20)

• Figure 1: Structured vs Text Editing Example
• Figure 2: Text- and Tree-based Cursors and Selection
• Figure 3: Inserting a around a term of the program: Users query the name of the construction that they want to insert, and Pantograph wraps it around the term at the cursor; $?0$ represents an unknown type.
• Figure 4: Cutting and pasting a selection into a different location in Pantograph. Zipper editing lends itself to a nice user interface similar to text editing. The user may make a selection with a familiar click and drag motion. The user may also cut selections into a clipboard, and paste them later at the cursor.
• Figure 5: Various edits each performed with a single cut and paste of a one-hole context selection. The first selection in each example is made by the user, but the second selection is only illustrative.

Theorems & Definitions (25)

• Theorem 1: Identity-Compose
• Theorem 2: Associativity of composition
• Theorem 3: Progress
• Theorem 4: Type Preservation
• Theorem 5: Termination
• Theorem 6: Confluence
• Theorem \ref{thm:terminationtheorem}: Termination
• Lemma 1
• Definition 1: Neutral form
• Definition 2: Maximal Neutral Form