一句话：提出 Decalf，用内在前序刻画带效应函数式程序成本界的有向成本感知逻辑框架，并给出单纯集模型。
针对带效应函数式程序（如概率选择、可变状态）的成本分析，现有 calf 等成本感知类型论依赖可分离的成本记账，难以直接处理效应与高阶程序。Decalf 将成本界本身视为一个程序，并给每个类型配备内在前序：在扩展阶段退化为外延相等，在内涵阶段反映成本近似。该设计保持程序行为不受成本记账影响，并避免显式成本递归。作者通过纯排序与带效应排序、简单概率程序和高阶函数等例子展示其表达力，最后在增广单纯集拓扑斯中给出模型，证明该类型系统的合理性。
We present decalf , a d irected, e ffectful c ost- a ware l ogical f ramework for studying quantitative aspects of functional programs with effects. Like calf , the language is based on a formal phase distinction between the extension and the intension of a program, its pure behavior as distinct from its cost measured by an effectful step-counting primitive. The type theory ensures that the behavior is unaffected by the cost accounting. Unlike calf , the present language takes account of effects , such as probabilistic choice and mutable state. This extension requires a reformulation of calf ’s approach to cost accounting: rather than rely on a “separable” notion of cost, here a cost bound is simply another program . To make this formal, we equip every type with an intrinsic preorder, relaxing the precise cost accounting intrinsic to a program to a looser but nevertheless informative estimate. For example, the cost bound of a probabilistic program is itself a probabilistic program that specifies the distribution of costs. This approach serves as a streamlined alternative to the standard method of isolating a cost recurrence and readily extends to higher-order, effectful programs. The development proceeds by first introducing the decalf type system, which is based on an intrinsic ordering among terms that restricts in the extensional phase to extensional equality, but in the intensional phase reflects an approximation of the cost of a program of interest. This formulation is then applied to a number of illustrative examples, including pure and effectful sorting algorithms, simple probabilistic programs, and higher-order functions. Finally, we justify decalf via a model in the topos of augmented simplicial sets.
@article{paperbot2587,
title = {Decalf: A Directed, Effectful Cost-Aware Logical Framework},
author = {Harrison Grodin and Yue Niu and Jonathan Sterling and Robert Harper},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632852}
}