paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Pantograph: A Fluid and Typed Structure Editor

Pantograph:一种流畅且带类型的结构编辑器
POPL 9(POPL)2025匹配度 2/10 · 该论文属于程序语言与类型系统方向,关注结构编辑器的类型化一洞上下文与类型差分,并包含形式化元理论与实现;但它不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户当前核心研究方向仅有宽泛的 PL 领域关联。引用 0 inbox
Jacob Prinz, Henry Blanchette, Leonidas Lampropoulos
crossref: 2026-09-10

AI 速览

一句话:提出 Pantograph 结构编辑方案,用类型化一洞上下文与类型差分,在保持程序良构的同时实现流畅编辑。

结构编辑器直接操作程序的语法树,这使程序有望按构造保持良构甚至良类型。但传统结构编辑刚性强制这些性质时面临“黏滞性”:修改现有程序常需临时破坏结构,禁止破坏又使编辑困难。本文提出一种始终维护有效程序结构、同时不牺牲编辑流畅性的结构编辑方案。其关键有两点:一是为树结构开发新的选择泛化,用户可通过剪切粘贴一洞上下文自由重排代码;二是用类型差分范畴为这些一洞上下文赋予类型,并探索系统在系统化维护良类型性时的元理论。作者实现 Pantograph 编辑器,并开展研究,成功教学生使用它编程,并将其表现与传统文本编辑器进行比较。

问题
传统结构编辑器为强制程序结构或类型正确性,往往要求编辑过程中不能临时破坏结构,导致所谓的黏滞性问题,使用户难以自由修改程序。
方法
提出树结构上选择操作的泛化,使用一洞上下文的剪切粘贴来重排代码;并用类型差分范畴类型化这些上下文,探索系统化维护良类型性的元理论。
评估
实现 Pantograph 编辑器,开展教学研究,成功教学生使用该编辑器编程,并将其表现与传统文本编辑器进行对比。
原文摘要(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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3240,
  title = {Pantograph: A Fluid and Typed Structure Editor},
  author = {Jacob Prinz and Henry Blanchette and Leonidas Lampropoulos},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {POPL},
  year = {2025},
  doi = {10.1145/3704864}
}