paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Set-Theoretic Types for Erlang in Practice (Experience Report)

集合论类型在 Erlang 中的实践(经验报告)
ICFP 10(ICFP)2026匹配度 3/10 · 论文属于程序语言与静态分析中的类型系统研究,与用户对静态分析的广泛兴趣有交集,但核心是 Erlang 的集合论类型检查器,未涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析,也不面向 ML/Agentic 程序。引用 1 inbox
Albert Schimpf, Annette Bieniusa
crossref: 2026-09-10

AI 速览

一句话:将集合论类型检查器 Etylizer 应用于自身实现,实证其在真实 Erlang 代码中的表达力、可用性与可扩展性。

集合论类型连接词(并、交、补)理论上适合刻画 Erlang 等动态类型语言,但实际可行性未知:类型求解在真实代码上是否可处理?无主类型时能否反映程序员意图?能否发现或避免错误?本文以集合论类型检查器 Etylizer 为对象,将其应用于自身实现这一非平凡 Erlang 代码库,检验其表达实际模式的能力,并分析在穷尽性检查、函数重载、数值精度、渐进类型与 occurrence typing 等维度上的设计权衡,且与其他类型系统对比。结果表明:集合论类型足以表达 Erlang 程序员的意图,交类型与自动穷尽性检查优势明显,且与 let-it-crash 风格不冲突;虽无主类型,类型可通过注解按需细化;可扩展性大体解决,遗留问题在表达力更弱的工具中也存在。

问题
集合论类型连接词对动态类型语言具有理论吸引力,但其在真实 Erlang 代码中的可处理性、意图表达能力与错误检测能力尚未得到实践检验。
方法
作者将集合论类型检查器 Etylizer 应用于自身实现,检验其类型系统表达非平凡 Erlang 代码模式的能力,并从多个设计维度与其他类型系统比较权衡。
评估
以自身实现为案例进行经验评估,考察表达力、可用性与可扩展性,并讨论穷尽性、重载、数值精度、渐进类型和 occurrence typing 等实践问题。
原文摘要(Abstract)

Set-theoretic type connectives with their native support for union, intersection, and negation have the potential to capture the idioms of dynamically typed languages like Erlang. We investigate whether this theoretical expressiveness translates into practice: does the resulting type solver remain tractable on real-world code? Can the type system reflect the programmer's intention even though no principal types exist? And does it actually detect or avoid errors in real codebases? This paper reports on our experience on applying Etylizer, a set-theoretic type checker for Erlang, to its own implementation. We test whether the type system can express the patterns arising in a non-trivial Erlang codebase. In addition, we examine the design tradeoffs that set-theoretic types present across exhaustiveness, function overloading, numeric precision, gradual typing, and occurrence typing, and relate them to how other type systems handle the same dimensions. Our findings suggest that set-theoretic types are expressive enough to capture Erlang programmers' intentions: intersection types and automatic exhaustiveness checking provide clear advantages, and the approach is not in conflict with Erlang's let-it-crash idiom. Although the type system lacks principal types, types can be refined as needed through annotations. Scalability for type checking is largely addressed, and in the cases where it remains an issue, less expressive tools face similar limitations.

链接与引用

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

BibTeX
@article{SchimpfB26,
  title = {Set-Theoretic Types for Erlang in Practice (Experience Report)},
  author = {Albert Schimpf and Annette Bieniusa},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {ICFP},
  year = {2026},
  doi = {10.1145/3828708}
}