We present Decalf, a directed, effectful cost-aware logical framework for studying quantitative aspects of functional programs with effects. Like Calf, the language is based on an internal phase distinction between the behavior of a program and its cost measured by an effect. Decalf extends Calf by accommodating other effects, such as probabilistic choice, which requires a reformulation of Calf's approach to cost analysis: rather than rely on a separable notion of cost, here a cost bound is simply another program. Formally, every type is equipped with an intrinsic preorder, allowing effectful programs to be compared for cost inequality. 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 cost ordering among terms that restricts in the behavioral phase to extensional equality. This formulation is then applied to illustrative examples, including pure and effectful sorting algorithms. Finally, Decalf is semantically justified via a model in the topos of augmented simplicial sets.

翻译：我们提出Decalf，这是一种有向的、带效应的成本感知逻辑框架，用于研究带有效应的函数式程序的量化特性。与Calf类似，该语言基于程序行为与其由效应度量的成本之间的内在阶段区分。Decalf扩展了Calf，以容纳其他效应（如概率选择），这需要对Calf的成本分析方法进行重新表述：不再依赖可分离的成本概念，而是将成本界视为另一个程序。形式上，每个类型都配备了内在的预序关系，使得带效应程序能够在成本不等式下进行比较。这种方法替代了提取成本递推关系的标准方法，并可直接推广到高阶的带效应程序。研究过程首先引入Decalf类型系统，该系统基于项之间的内在成本序关系，该关系在行为阶段被限制为外延相等。随后将这一表述应用于示例说明，包括纯排序算法和带效应的排序算法。最后，通过在增强单纯集层中的模型为Decalf提供语义证明。