严格性类型化（扩展版） (Typing Strictness (Extended Version))

Strictness analysis is critical to efficient implementation of languages with non-strict evaluation, mitigating much of the performance overhead of laziness. However, reasoning about strictness at the source level can be challenging and unintuitive. We propose a new definition of strictness that refines the traditional one by describing variable usage more precisely. We lay type-theoretic foundations for this definition in both call-by-name and call-by-push-value settings, drawing inspiration from the literature on type systems tracking effects and coeffects. We prove via a logical relation that the strictness attributes computed by our type systems accurately describe the use of variables at runtime, and we offer a strictness-annotation-preserving translation from the call-by-name system to the call-by-push-value one. All our results are mechanized in Rocq.

翻译：严格性分析对于非严格求值语言的高效实现至关重要，它能显著降低惰性求值带来的性能开销。然而，在源代码层面进行严格性推理可能具有挑战性且不够直观。我们提出了一种新的严格性定义，通过更精确地描述变量的使用情况，对传统定义进行了细化。我们从追踪效应和共效应的类型系统文献中汲取灵感，为按名调用和按值推送两种设定下的这一定义建立了类型理论基础。我们通过逻辑关系证明，由我们的类型系统计算出的严格性属性能够准确描述变量在运行时的使用情况，并且我们提供了一个从按名调用系统到按值推送系统的严格性标注保持的转换。我们所有的结果均在Rocq中进行了机械化验证。