paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Casts and costs: harmonizing safety and performance in gradual typing

类型转换与开销:协调渐进类型中的安全性与性能
ICFP 2(ICFP)2018匹配度 2/10 · 该论文属于渐进类型与程序分析/抽象解释方向,研究类型标注带来的性能开销预测与推荐,但未涉及用户核心关注的 PL×AI/LLM、Agentic 程序分析、浮点程序分析或贝叶斯程序分析。其静态分析与开销推断方法有一定 PL 背景相关性,但不在当前研究主线上。引用 11 inbox
John Peter Campora, Sheng Chen, Eric Walkingshaw
crossref: 2026-09-10

AI 速览

一句话:提出静态开销语义与开销推断技术,为渐进类型程序推荐兼顾安全与性能的类型标注。

渐进类型允许静态与动态类型混用,但二者交互常导致难以预测的性能下降,阻碍用户添加类型标注。本文提出静态开销语义,准确预测渐进类型程序中静态-动态交互的开销;提出高效推断程序中所有可推断类型分配组合开销的技术;并将分析结果转化为具体建议与解释,帮助程序员理解、调试和优化性能。作者实现 Herder,对 Reticulated Python 程序的不同类型配置进行静态性能分析。在 15 个 Python 程序上的评估表明,Herder 能准确高效地推荐既优化性能又不牺牲静态类型安全保证的类型分配方案。

问题
渐进类型中静态与动态代码交互会造成显著且难以预测的性能下降,用户不清楚添加哪些标注会引发或消除开销。
方法
提出静态开销语义来预测开销,并高效推断所有可推断类型分配组合的开销,再转化为具体标注建议与解释。
评估
在 Herder 中实现对 Reticulated Python 程序做静态性能分析,并在 15 个 Python 程序上评估推荐类型分配的性能与安全性。
原文摘要(Abstract)

Gradual typing allows programmers to use both static and dynamic typing in a single program. However, a well-known problem with sound gradual typing is that the interactions between static and dynamic code can cause significant performance degradation. These performance pitfalls are hard to predict and resolve, and discourage users from using gradual typing features. For example, when migrating to a more statically typed program, often adding a type annotation will trigger a slowdown that can be resolved by adding more annotations elsewhere, but since it is not clear where the additional annotations must be added, the easier solution is to simply remove the annotation. To address these problems, we develop: (1) a static cost semantics that accurately predicts the overhead of static-dynamic interactions in a gradually typed program, (2) a technique for efficiently inferring such costs for all combinations of inferrable type assignments in a program, and (3) a method for translating the results of this analysis into specific recommendations and explanations that can help programmers understand, debug, and optimize the performance of gradually typed programs. We have implemented our approach in Herder, a tool for statically analyzing the performance of different typing configurations for Reticulated Python programs. An evaluation on 15 Python programs shows that Herder can use this analysis to accurately and efficiently recommend type assignments that optimize the performance of these programs without sacrificing the safety guarantees provided by static typing.

链接与引用

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

BibTeX
@article{paperbot286,
  title = {Casts and costs: harmonizing safety and performance in gradual typing},
  author = {John Peter Campora and Sheng Chen and Eric Walkingshaw},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {ICFP},
  year = {2018},
  doi = {10.1145/3236793}
}