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