Decalf: A Directed, Effectful Cost-Aware Logical Framework

TL;DR

Decalf is a logical framework for analyzing the cost of effectful functional programs, extending previous work to include probabilistic effects and higher-order effects.

Contribution

It introduces a new intrinsic cost ordering for effectful programs, providing a streamlined approach to cost analysis that extends to higher-order effects.

Findings

Decalf can compare effectful programs for cost inequality.

The framework applies to probabilistic and sorting algorithms.

Semantic justification is provided via a topos model.

Abstract

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.