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