Typing Strictness (Extended Version)

TL;DR

This work defines intensional strictness, a per-use descriptive notion of how variables are utilized in non-strict languages, using strictness attributes $S$, $L$, and $?$ together with latent effects $γ$. It develops two type systems, $CBN^γ$ and $CBPV^γ$, to encode this notion and proves their soundness via a logical-relations framework, plus a γ-preserving translation between the calculi. The approach yields finer-grained guarantees about strict and lazy usage, and supports unused-variable tracking, with results mechanized in Rocq. These contributions provide a rigorous foundation for reasoning about strictness, with potential implications for compiler optimization and cross-language analysis.

Abstract

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.

Figures (4)

• Figure 1: Lazy evaluation of list sum using foldl
• Figure 2: Simple examples of variable usage
• Figure 3: Types and Syntax of $\text{CBN}^{\textcolor{burntorange}{\gamma\!}}$
• Figure 4: Strictness semilattice

Theorems & Definitions (1)

• Definition 2.1: Intensional Strictness