Decalf: A Directed, Effectful Cost-Aware Logical Framework
Provides a foundational framework for quantitative reasoning about effectful programs, addressing a known bottleneck in cost analysis for non-separable effects.
Decalf is a cost-aware logical framework for functional programs with effects, extending Calf to handle effects like probabilistic choice by treating cost bounds as programs. It uses an intrinsic preorder for cost inequality, enabling streamlined cost analysis of higher-order effectful programs, demonstrated on sorting algorithms.
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.