一句话：提出类型论中替换、依赖消去与效应不相容的 no-go 定理，并给出依赖 CBPV 演算 ∂CBPV 以调和三者。
论文指出，在类型论中替换、依赖消去与效应之间存在根本性张力，并将其凝练为一个 no-go 定理，称为类型论的“火三角”。为解除该限制，作者提出 ∂CBPV：将 call-by-push-value（CBPV）这一通用效应演算扩展到依赖类型。通过把 call-by-name 和 call-by-value 的经典分解推广到 ∂CBPV，论文解释了为何在效应存在时，call-by-name 必须限制依赖消去，而 call-by-value 必须限制替换。最后，作者给出从 ∂CBPV 到 Martin-Löf 类型论的多种带效应语法翻译（reader、weaning、forcing），以说明该演算足以解释多种效应。
There is a critical tension between substitution, dependent elimination and effects in type theory. In this paper, we crystallize this tension in the form of a no-go theorem that constitutes the fire triangle of type theory. To release this tension, we propose ∂CBPV, an extension of call-by-push-value (CBPV) —a general calculus of effects—to dependent types. Then, by extending to ∂CBPV the well-known decompositions of call-by-name and call-by-value into CBPV, we show why, in presence of effects, dependent elimination must be restricted in call-by-name, and substitution must be restricted in call-by-value. To justify ∂CBPV and show that it is general enough to interpret many kinds of effects, we define various effectful syntactic translations from ∂CBPV to Martin-Löf type theory: the reader, weaning and forcing translations.
@article{paperbot522,
title = {The fire triangle: how to mix substitution, dependent elimination, and effects},
author = {Pierre-Marie Pédrot and Nicolas Tabareau},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371126}
}