paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Persimmon: Nested Family Polymorphism with Extensible Variant Types

Persimmon:具有可扩展变体类型的嵌套族多态
OOPSLA 8(OOPSLA1)2024匹配度 1/10 · 论文属于编程语言类型系统与可扩展性设计,核心是嵌套族多态、可扩展变体类型及类型可靠性证明,与用户关注的 PL 与 AI/LLM、静态分析、浮点程序分析、贝叶斯程序分析等交叉方向没有直接关联。虽然包含形式化证明和 Scala 编译实现,但未涉及 AI/Agent 或程序分析。引用 3 inbox
Anastasiya Kravchuk-Kirilyuk, Gary Feng, Jonas Iskander, Yizhou Zhang, Nada Amin
crossref: 2026-09-10

AI 速览

一句话:提出 Persimmon 函数式系统,以嵌套族多态和可扩展变体类型支持模块化扩展,并证明其类型可靠性。

模块化可扩展代码面临多重障碍:模式匹配等语言构造不易扩展,继承代码在扩展类型下可能失去类型安全,设计模式带来负担,参数杂乱降低可读性,最终常导致代码重复。Persimmon 是一个函数式系统,提供嵌套族多态、可扩展变体类型和可扩展模式匹配,将多数构造设计为内置的“扩展钩子”,以减少参数杂乱和用户负担。它在继承时保持嵌套族之间的关系,从而支持大规模扩展;嵌套族多态可表达可组合扩展,因此可通过编码支持 mixin。论文给出到 Scala 的翻译,说明无需可扩展变体即可编译,并证明 progress 与 preservation,确立系统可靠性。

问题
如何设计兼具模块化与可扩展性的语言构造,使模式匹配与继承代码在扩展类型时仍类型安全,并避免设计模式负担与参数杂乱导致的代码重复。
方法
提出 Persimmon 函数式系统,内置嵌套族多态、可扩展变体类型和可扩展模式匹配作为扩展钩子,保持继承下嵌套族关系,并通过编码支持 mixin,进而翻译到 Scala。
评估
通过到 Scala 的翻译展示可编译性,并证明 progress 与 preservation 以确立类型可靠性。
原文摘要(Abstract)

Many obstacles stand in the way of modular, extensible code. Some language constructs, such as pattern matching, are not easily extensible. Inherited code may not be type safe in the presence of extended types. The burden of setting up design patterns can discourage users, and parameter clutter can make the code less readable. Given these challenges, it is no wonder that extensibility often gives way to code duplication. We present our solution: Persimmon, a functional system with nested family polymorphism, extensible variant types, and extensible pattern matching. Most constructs in our language are built-in "extensibility hooks," cutting down on the parameter clutter and user burden associated with extensible code. Persimmon preserves the relationships between nested families upon inheritance, enabling extensibility at a large scale. Since nested family polymorphism can express composable extensions, Persimmon supports mixins via an encoding. We show how Persimmon can be compiled into a functional language without extensible variants with our translation to Scala. Finally, we show that our system is sound by proving the properties of progress and preservation.

链接与引用

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

BibTeX
@article{paperbot2549,
  title = {Persimmon: Nested Family Polymorphism with Extensible Variant Types},
  author = {Anastasiya Kravchuk-Kirilyuk and Gary Feng and Jonas Iskander and Yizhou Zhang and Nada Amin},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {OOPSLA1},
  year = {2024},
  doi = {10.1145/3649836}
}