We present decalf, a \textbf{d}irected, \textbf{e}ffectful \textbf{c}ost-\textbf{a}ware \textbf{l}ogical \textbf{f}ramework for studying quantitative aspects of functional programs with effects. Like \textbf{calf}, the language is based on a formal \emph{phase distinction} between the \emph{extension} and the \emph{intension} of a program, its pure \emph{behavior} as distinct from its \emph{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 \emph{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 \emph{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 recurrence that bounds the cost in a manner that 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.