{"id":"d51a5ab2-f2a9-41c8-abd5-cdc3ab72bd68","arxiv_id":"2411.16571","paper_version":2,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper presents a structure editor where selecting and editing one-hole contexts preserves well-formedness, and typed edits propagate via type diffs while preserving well-typedness.","lead":"Pantograph is a new kind of code editor that works on the program's tree structure and never lets the code become syntactically broken, while still allowing cut-and-paste style edits. It introduces a way to select parts of trees and uses 'type diffs' to automatically update the rest of the program when types change.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The propagation rules in §5.4 are under-specified: the generic Propagate↓/↑ rules rely on an existential decomposition σ,C with no canonical choice or unification algorithm, so the rewrite relation and Theorems 5–6 are not fully pinned down for the core calculus as written.","rationale":"The reader's weakest assumption focuses on scaling the formal metatheory from the small core calculus to richer languages. That is a fair and honest concern, but my stress-test identifies a more immediate issue: the formal system for the core calculus itself is not fully specified. The generic propagation rules in §5.4 and Appendix A are written with existential quantifiers over a diff substitution and a one-hole-context decomposition; no algorithm is given for finding them, and no uniqueness or canonicity result is proved. Consequently, the small-step relation is ambiguous as stated, and the confluence proof—which handles pairs of different rules and two-boundary interactions—does not explicitly handle two different decompositions of the same boundary by the same rule. This matters because the central claim 'always maintains a valid program structure without sacrificing fluidity' is backed by Theorems 3–6; if the relation is not deterministic or its nondeterminism is not fully confluent, the claim that the editor's edits are well-typed by construction is not established even for the core calculus. The paper has real independent support: a shipped artifact, a user study, and substantial proof sketches. The concern is therefore not that the approach is wrong, but that a key formal step needs to be made precise. A proof-assistant formalization or an explicit matching algorithm would settle it. For this reason, I would make acceptance conditional on supplying that missing specification rather than rejecting the work.","tokens_in":124,"tokens_out":17166,"duration_ms":420784,"concrete_test":"Formalize the core calculus and the §5.4/Appendix A rules in a proof assistant such as Agda, Lean, or Coq, with an explicit, deterministic unification/decomposition procedure replacing the existential 'find σ,C'. If Theorems 3–6 hold for that formalized relation, the concern is resolved. Alternatively, write a small enumerator over all reachable diff-boundary states that computes every possible σ,C decomposition for each Propagate rule and checks local confluence of the resulting one-step reducts; any non-joinable pair would falsify Theorem 6 as stated, while a proof that all decompositions yield joinable reducts would supply the missing lemma.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central formal claim that Pantograph always maintains well-typedness rests on the small-step diff-propagation system of §5. The generic rules Propagate↓ and Propagate↑ are stated as: find a diff substitution σ and a one-hole context C such that the incoming diff has the form (σ_id C)[σ s′], with s = C[s′]. The paper says such a substitution is found by a 'unification procedure' but never defines that procedure, nor proves that the decomposition is unique or canonical. As written, the rules are existential: a single term can admit multiple distinct one-step reducts from different choices of σ/C for the same boundary. Appendix B.3's local-confluence proof enumerates pairs of different rules and boundary–boundary interactions, but it does not analyze two applications of the same Propagate rule with different decompositions of the same diff. Therefore, the confluence theorem does not, on its face, cover all nondeterminism present in the stated rewrite relation. Since Progress, Type Preservation, Termination, and Confluence are the formal backbone of the paper's central claim, this under-specification is load-bearing: the reader cannot verify that the metatheory describes the same deterministic algorithm that the artifact implements.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents Pantograph, a structure editor that generalizes text selection to tree-based one-hole contexts (\"zipper editing\") and uses this abstraction to maintain syntactic well-formedness of programs at every edit. To additionally preserve well-typedness, the paper introduces a category of type diffs: each one-hole context is assigned a diff that describes how the type and typing context change when that context is inserted or removed. The main formal device is a small-step diff-propagation system that carries diff boundaries through a simply-typed core calculus with integers, booleans, functions, lists, pattern matching, typed holes, and three explicit error forms (free variables, commented applications, and type-error boundaries). The paper claims Theorems 3--6 for this system: Progress, Type Preservation, Termination, and Confluence, with proofs in Appendices B and C. It also reports on an implementation of Pantograph and a user study with 13 students, finding that participants could learn to use the editor and solve tasks, though they were on average slower than with a text editor. The final sections discuss limitations and related work.","tokens_in":40814,"tokens_out":7235,"duration_ms":74181,"significance":"The central idea of the paper---generalizing text selection to one-hole contexts and typing those contexts with a category of diffs---is a genuine and non-obvious contribution to the structure-editor literature, and it is developed with unusual care. The formal development is largely self-contained: diffs are defined from scratch, the category laws for diffs are proved, and the small-step system is shown to preserve types and terminate. The paper is also honest about scope: the metatheory is for the small simply-typed core of Figure 6, and the user study is presented as a feasibility study with explicit limitations. An artifact is available, which strengthens the empirical claims. If the formal system is fully pinned down, this is a solid POPL contribution; the main barrier to acceptance is the underspecification of the generic propagation rules discussed in the major comments.","major_comments":[{"comment":"The treatment of the final top-level up boundary is not fully specified. The proof of Theorem 3 says that if the final program has the form {t}↑_{Δ⊢δ}, an invariant shows Δ = id and \"Pantograph removes the boundary and the program has a new type.\" However, no small-step rule removes a non-identity up boundary (Identity↑ requires δ = id), and removing such a boundary changes the type of the program, which would conflict with the statement of Theorem 4 if the removal is considered a step of the relation. Please clarify whether the removal is part of the rewrite relation or an external \"commit\" operation, and state how Type Preservation is meant to account for the resulting type change.","section":"§5.6, Theorem 3 proof"}],"minor_comments":[{"comment":"The statement of Lemma 6 refers to a neutral form u, but the case analysis inside the proof uses t instead of u; aligning the notation would avoid confusion.","section":"Appendix B.3, Lemma 6"},{"comment":"The rule as written in the main text uses t on the left and t in the output, while the neighboring Displace-App↑ and the appendix rule use t1 and t2; please make the metavariable usage uniform across the two presentations.","section":"§5.5, Insert-App↑"},{"comment":"The treatment of omitted participants and discarded data points is described in prose but would benefit from a small table listing per-participant task counts, skipped tasks, and which data points were discarded, to make the reported 124 data points easy to verify.","section":"§6.1"},{"comment":"The sentence \"All but two participants made use of the diff propagation to solve the problem - one manually rewrote a function call instead, and the other skipped the problem\" gives numbers for 13 participants, but the analysis earlier in the section is based on 11 participants; please reconcile these counts explicitly.","section":"§6.2"},{"comment":"The grammar of type diffs introduces +⟨T→⟨δ⟩⟩ and −⟨T→⟨δ⟩⟩, while Section 5.2 generalizes these to +⟨c⟨d⟩⟩ and −⟨c⟨d⟩⟩; a short sentence explaining that the earlier T→⟨δ⟩ is the specialization of the one-hole context c to a function type would help readers connect the two presentations.","section":"§3"},{"comment":"The paper states the formal theorems for the core calculus of Figure 6 and acknowledges in Section 7 that the full language is not covered; a closing sentence in Section 9 noting that extension to features such as polymorphism, effects, and dependent types remains open would match the paper's otherwise careful limitations statement.","section":"§5.6"}],"recommendation":"major_revision","confidential_remarks":"Dear Editor, I agree with the positive assessment of the paper's novelty and scope, but I found the concern about the under-specified propagation rules substantial. The existential formulation of Propagate↓/↑ and the incomplete local-confluence case analysis are fixable in a revision, but as written they leave a gap in the paper's central formal claims. I see no circularity or data-fitting issue, and the user study is small but transparent about its limitations; it should not block acceptance. I therefore recommend major_revision rather than accept: once the matching algorithm is specified (or uniqueness is proved) and the confluence proof is extended accordingly, the paper would be suitable for publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is worth your time. The core idea — generalizing text selection to one-hole contexts and typing those selections with a category of diffs — is a real step past the usual zipper/ornament story, and the authors actually build the machinery: a small-step diff-propagation system, proofs of progress, preservation, termination, and confluence, plus an artifact and a candid user study. The formal development is careful and mostly convincing, and the user study is refreshingly honest about its own limitations, including slower task times and the authors' personal involvement.\n\nThe soft spot is exactly what the stress-test note flags. The generic Propagate-down and Propagate-up rules in §5.4 are stated existentially: find a diff substitution σ and one-hole context C such that the incoming diff decomposes as (σ_id C)[σ s′]. The paper never defines the unification procedure, never claims the decomposition is unique, and the local-confluence proof in Appendix B.3 enumerates rule/rule overlaps but does not analyze two different applications of the same Propagate rule with different decompositions of the same boundary. Since the same diff can indeed be decomposed in more than one way (e.g., a context diff matched against Γ vs. a type diff matched against the conclusion's type), the rewrite relation as stated is not pinned down, and the confluence theorem does not cover all its nondeterminism. This is a load-bearing issue for the formal part, but it looks fixable: define a deterministic decomposition algorithm, prove it total on reachable states, and prove confluence for the resulting deterministic system (or prove a uniqueness lemma for the decomposition under the paper's invariants).\n\nThe other weaknesses are real but proportionate. The metatheory is only for a simply typed core; scaling to polymorphism, dependent types, or effects is asserted, not shown. The eight alteration rules are hard-coded and not characterized for completeness or user-facing adequacy. The user study is small, in-person, and biased, though the authors disclose this and frame it as feasibility, not superiority.\n\nWho should read this: PL researchers working on structure editors, typed holes, refactoring, or type-error localization, and HCI people interested in editor design. It deserves a serious referee; send it out, but push the authors to close the decomposition gap. I'd accept after revisions.","headline":"A genuinely new and mostly solid structure-editing paper whose main formal gap is an under-specified unification step in the generic propagation rules, leaving the confluence claim slightly loose as written.","tokens_in":21,"tokens_out":3524,"would_cite":true,"duration_ms":80135,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68N30","68Q42","03B70"],"pacs":[],"model":"deepseek-v4-flash","headline":"By generalizing selection to one-hole contexts and typing edits with diffs, a structure editor can stay well-formed and well-typed at every moment without sacrificing fluidity.","keywords":["structure editors","zipper editing","one-hole contexts","type diffs","diff propagation","type preservation","confluence","viscosity"],"falsifier":"Run the propagation system on reachable edit states in the implemented core calculus and search for a term that contains a diff boundary not at the top to which no rewrite rule applies; any such stuck state falsifies the Progress theorem, and two different terminal terms from one edit state falsify confluence. A ready target is a language extension with a polymorphic typing rule in which a type variable appears twice in a premise, where the paper's linearity-based invariants are known to be delicate.","tokens_in":40321,"feed_emoji":"✂️","tokens_out":9956,"duration_ms":84189,"temperature":0.7,"pith_summary":"This paper argues that the viscosity problem of structure editors is solvable: an editor can keep every program state syntactically well-formed and well-typed while still letting users freely rearrange code the way text editors do. The key is to generalize text selection to trees as one-hole contexts, so selecting and editing what lies between two tree cursors becomes a single cut-and-paste operation. To keep edits well-typed in addition to well-formed, the paper types each one-hole context by a diff between its inner and outer types, and propagates that diff through the surrounding program with a small-step rewriting system, automatically updating type annotations, inserting arguments, or placing first-class error forms where needed. The formal claims are progress, type preservation, termination, and confluence for this propagation system, proved for a small simply-typed core language.","feed_headline":"Edit programs as fluidly as text, never breaking types","feed_subtitle":"A structure editor that propagates type diffs automatically, so the program never becomes ill-typed while you edit.","key_machinery":"The central objects are one-hole contexts and type diffs. A one-hole context $C[\\cdot]$ is a tree with a single missing subterm; generalizing text selection to trees means selecting, cutting, and pasting an arrangement $C_1[C_2[t]]$, i.e., the program decomposed into two contexts and a focus term. Type diffs $\\delta$ describe how a type changes across an edit, with constructors for identity, childwise change, adding or removing a function argument, and replacement; they form a category under composition. Diff boundaries $\\{t\\}^{\\uparrow}_{\\Delta \\vdash \\delta}$ and $\\{t\\}^{\\downarrow}_{\\Delta \\vdash \\delta}$, carrying diffs for both the typing context and the type, are propagated through terms by rules derived from intrinsic typing rules via diff substitutions over metavariables. The eight alteration rules (insert/delete abstraction, insert/displace/delete application, local-to-free and free-to-local) make the actual code changes, and error boundaries $\\{t\\}^{!}$ abort propagation when no other rule applies.","core_discovery":"The paper's central discovery is that the viscosity problem of structure editors is not fundamental: a selection mechanism based on one-hole contexts supports the same cut-and-paste fluidity as text editing while preserving well-formedness, and typing those contexts with a category of diffs extends the guarantee to well-typedness. A user edit to the program (inserting, removing, or altering a one-hole context) is represented as a diff boundary, an internal term-shaped marker carrying a context diff and a type diff; a small-step rewriting system then propagates the boundary through the program by matching each language construct's typing rule, and eight hard-coded alteration rules decide how to update the surrounding code, inserting lambdas or applications, displacing arguments into commented applications, converting bound variables to free ones, or wrapping an offending subterm in a first-class type error boundary. The propagation system is proved terminating, type-preserving, confluent, and total (progress).","pith_inferences":["Nothing in the proof prevents the same machinery from being used outside an editor, for example as a refactoring engine for typed ASTs where a program transformation is specified as a diff and then propagated; the paper does not explore this direction.","A natural stress test is polymorphic recursion: the confluence invariant relies on at most one up-like boundary at a time, and it is unclear whether this survives language features with nonlinear typing rules beyond the core calculus.","The user study compares only against a text editor and reports roughly 1.4x slower average task time; a direct comparison with gradual structure editors that allow grammar-breaking edits, which the paper does not run, would separate the cost of typed diff propagation from the cost of tree-based interaction.","Multi-hole selections (cutting two disjoint subtrees at once) might remove the remaining multiplicity barriers that the paper lists as limitations; this is a concrete interface extension the authors do not implement."],"forward_implications":["Restructuring edits such as adding a parameter to a function become a single cut-and-paste operation, with the system automatically updating the type signature, call sites, and recursive calls.","An editor built on this scheme never needs to re-parse or re-typecheck the program after an edit, since each state is well-formed and well-typed by construction.","Type errors become first-class, user-editable forms (free variables, commented applications, and error boundaries) that can be selected and deleted like any other construct.","The diff category gives edit sequences a compositional semantics: two consecutive edits compose into a single diff, which is the basis for undo/redo and for reasoning about refactorings."],"supporting_citations":[{"why":"Introduces the zipper, the one-hole-context decomposition of a tree that underlies Pantograph's cursors, selections, and local editing operations.","marker":"Huet [1997]"},{"why":"States that one-hole contexts are the derivative of a regular type, the formal view of contexts that the paper generalizes into selections and typed diffs.","marker":"McBride [2001]"},{"why":"Defines viscosity, the structure-editing friction that this paper's zipper editing and typed diffs are designed to eliminate.","marker":"Blackwell and Green [2003]"},{"why":"Presents Hazelnut, an intrinsically typed structure editor with typed holes and statics for incomplete programs; Pantograph's typed states and first-class error forms build on this line of work.","marker":"Omar et al. [2017]"},{"why":"Introduces Tylr, a gradual structure editor that addresses viscosity by allowing grammar-breaking edits with obligations, the closest alternative approach this paper compares against.","marker":"Moon et al. [2022]"},{"why":"Describes the current Hazel marking algorithm that re-checks programs after edits, which contrasts with Pantograph's strategy of placing errors during the edit itself.","marker":"Zhao et al. [2024]"}],"fun_headline_variants":["Cut-and-paste code without ever breaking types","Structure editor with text-like fluidity and type safety","Editing that never makes your program ill-typed","A structure editor that respects types while you edit","Fluid code editing, type errors impossible"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The formal guarantees are proved only for a small simply-typed core language with integers, booleans, functions, lists, and pattern matching, and the paper assumes the same typed-diff propagation works in full languages with polymorphism, dependent types, or effects.","fun_headline_variants_meta":{"raw":{"variants":["Cut-and-paste code without ever breaking types","Structure editor with text-like fluidity and type safety","Editing that never makes your program ill-typed","A structure editor that respects types while you edit","Fluid code editing, type errors impossible"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000606,"raw_usage":{"total_tokens":2826,"prompt_tokens":948,"completion_tokens":1878,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":564,"completion_tokens_details":{"reasoning_tokens":1807}},"tokens_in":564,"tokens_out":1878,"duration_ms":13514,"temperature":1.0,"reasoning_tokens":1807,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T12:57:40.842269+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the propagation system on reachable edit states in the implemented core calculus and search for a term that contains a diff boundary not at the top to which no rewrite rule applies; any such stuck state falsifies the Progress theorem, and two different terminal terms from one edit state falsify confluence. A ready target is a language extension with a polymorphic typing rule in which a type variable appears twice in a premise, where the paper's linearity-based invariants are known to be delicate.","supporting_citations":[],"review_version":1}