pith. sign in

arxiv: 2307.05938 · v4 · pith:PGPAEV3Dnew · submitted 2023-07-12 · 💻 cs.PL

Decalf: A Directed, Effectful Cost-Aware Logical Framework

Harrison Grodin (1) , Yue Niu (2) , Jonathan Sterling (3) , Robert Harper (1) ((1) Carnegie Mellon University , (2) National Institute of Informatics , (3) University of Cambridge) This is my paper

Pith reviewed 2026-05-24 08:11 UTC · model grok-4.3

classification 💻 cs.PL
keywords cost-aware programminglogical frameworkseffectful computationdirected typespreordersphase distinctionquantitative program analysis
0
0 comments X

The pith

Every type is equipped with an intrinsic preorder allowing effectful programs to be compared for cost inequality.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Decalf reformulates cost analysis so that a cost bound is simply another program, rather than a separate recurrence. This is achieved by equipping every type with an intrinsic preorder that compares programs on cost while restricting to equality in the behavioral phase. The framework handles effects like probabilistic choice uniformly and applies the approach to both pure and effectful sorting algorithms. A semantic model in the topos of augmented simplicial sets justifies the system.

Core claim

The central discovery is that by introducing an intrinsic cost ordering among terms that restricts to extensional equality in the behavioral phase, cost bounds for effectful programs can be expressed directly as programs. This eliminates the need for a separable notion of cost and extends the analysis to higher-order effectful programs without additional machinery.

What carries the argument

The intrinsic preorder on every type, which supports cost inequality comparisons and enforces the phase distinction between behavior and cost.

Load-bearing premise

The phase distinction between behavioral equality and cost preorder can be maintained uniformly across arbitrary effects without requiring a separable cost component.

What would settle it

Finding an effect where defining the preorder forces either loss of the behavioral phase distinction or the reintroduction of a separate cost measure.

Figures

Figures reproduced from arXiv: 2307.05938 by (2) National Institute of Informatics, (3) University of Cambridge), Harrison Grodin (1), Jonathan Sterling (3), Robert Harper (1) ((1) Carnegie Mellon University, Yue Niu (2).

Figure 1
Figure 1. Figure 1: Recursive implementation of the doubling function on natural numbers, instrumented with one cost [PITH_FULL_IMAGE:figures/full_fig_p011_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Recursive implementation of the list insertion, the auxiliary function of insertion sort, instrumented [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 4
Figure 4. Figure 4: Specification of the branch and fail primitives for finitary nondeterministic branching, which form a semilattice. The laws for interactions with the step primitive are included. Note that fail is the nullary correspondent to branch, so just as branch/step pushes cost into all two branches, fail/step pushes cost into all zero branches. The laws for interactions with computation type primitives are omitted … view at source ↗
Figure 5
Figure 5. Figure 5: Quicksort algorithm [Hoare 1961, 1962], where the choose auxiliary function chooses a pivot nondeter￾ministically. As in Figs. 2 and 3, the cost instrumentation tracks one unit of cost per comparison. 3.2 Effectful Algorithms Treating cost bounds as program inequalities, we can extend decalf with various computational effects and prove bounds on effectful programs. 3.2.1 Nondeterminism First, we consider t… view at source ↗
Figure 6
Figure 6. Figure 6: The usual implementation of list index lookup, instrumented with one cost per recursive call. If the [PITH_FULL_IMAGE:figures/full_fig_p014_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Specification of the flip primitive for finitary probabilistic choice, which forms a convex space. The law for interaction with the step primitive is included. Like in [PITH_FULL_IMAGE:figures/full_fig_p015_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Implementation of sublist, an algorithm to compute a random sublist of an input list, where one unit of cost is incurred for each ::-node in the output list. bernoulli : F(1) bernoulli = flip½ (ret(★), step1 (ret(★))) binomial : nat → F(1) binomial zero = ret(★) binomial (suc(𝑛)) = bind★ ← bernoulli in binomial 𝑛 [PITH_FULL_IMAGE:figures/full_fig_p015_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Implementation of the Bernoulli and binomial cost distributions with [PITH_FULL_IMAGE:figures/full_fig_p015_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Specification of the get and set primitives for single-cell global state [Plotkin and Power 2002] with a fixed state type 𝑆 : tp+ . The laws for interaction with the step primitive are included. Like in [PITH_FULL_IMAGE:figures/full_fig_p016_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Implementation of the twice function which takes a suspended computation as input, runs it twice, and adds the results. No cost is instrumented explicitly, but 𝑒 may incur cost (and/or other effects). Example 3.10 (State-dependent cost). For this example, let state type 𝑆 = nat. Recall the double function from Example 3.1, and consider the program 𝑒 ≔ get(𝑛. bind𝑛 ′ ← double 𝑛 in set(𝑛 ′ ; ret(𝑛))) that d… view at source ↗
Figure 12
Figure 12. Figure 12: Implementation of the map function on lists, which applies a suspended function elementwise to an input list. No cost is instrumented explicitly, but the applications of 𝑓 may incur cost (and/or other effects). If some properties about input 𝑒 are known, though, we may be able to simplify. For example, if 𝑒;ret(★) ≤ step1 (ret(★)), we can prove that twice 𝑒;ret(★) ≤ step2 (ret(★)). In other words, if we k… view at source ↗
Figure 13
Figure 13. Figure 13: Quotient inductive type defining cost structure [PITH_FULL_IMAGE:figures/full_fig_p024_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Sum types in decalf. nat : tp+ zero : tm+ (nat) suc : tm+ (nat) → tm+ (nat) rec : (𝑛 : tm+ (nat)) → (𝑃 : tm+ (nat) → Jdg) → 𝑃 (zero) → ( (𝑛 : tm+ (nat)) → 𝑃 (𝑛) → 𝑃 (suc(𝑛))) → 𝑃 (𝑛) rec/𝛽zero : {𝑃, 𝑒0, 𝑒1} rec(zero; 𝑃; 𝑒0; 𝑒1) = 𝑒0 rec/𝛽suc : {𝑛, 𝑃, 𝑒0, 𝑒1} rec(suc(𝑛); 𝑃; 𝑒0; 𝑒1) = 𝑒1 (𝑛) (rec(𝑛; 𝑃; 𝑒0; 𝑒1)) list : tp+ → tp+ [] : {𝐴} tm+ (list(𝐴)) :: : {𝐴} tm+ (𝐴) → tm+ (list(𝐴)) → tm+ (list(𝐴)) rec : {𝐴… view at source ↗
Figure 15
Figure 15. Figure 15: Inductive types in decalf. Proc. ACM Program. Lang., Vol. 8, No. POPL, Article 10. Publication date: January 2024 [PITH_FULL_IMAGE:figures/full_fig_p029_15.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper presents Decalf, a directed effectful cost-aware logical framework extending Calf. It equips every type with an intrinsic preorder so that effectful programs (including those using probabilistic choice) can be compared directly for cost inequality; cost bounds are expressed as programs rather than via a separable cost component. The preorder restricts to behavioral equality in the extensional phase. The development defines the type system, applies it to pure and effectful sorting algorithms, and provides semantic justification via a model in the topos of augmented simplicial sets.

Significance. If the model validates the claimed preorders and inequalities, the work supplies a uniform, streamlined method for cost reasoning about higher-order effectful programs that avoids isolating separate cost recurrences. The intrinsic-preorder formulation and its semantic grounding in augmented simplicial sets constitute a technically interesting reformulation of prior Calf-style analysis.

minor comments (2)
  1. [Abstract] The abstract states that the model 'semantically justifies' the development but does not indicate which specific theorem (e.g., soundness of the preorder interpretation for probabilistic choice) is proved in the semantics section.
  2. Notation for the phase distinction (behavioral vs. cost preorder) is introduced without an early, compact summary of how the two phases interact in the presence of arbitrary effects.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of Decalf and for recommending minor revision. The recognition of the uniform method for cost reasoning and the semantic grounding in augmented simplicial sets is appreciated.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained via external semantics

full rationale

The paper introduces Decalf as a new type system definition equipping every type with an intrinsic preorder that restricts to behavioral equality in the extensional phase, with cost bounds expressed directly as programs rather than a separable component. This reformulation is applied to examples and justified by a model in the topos of augmented simplicial sets, an external category. No equations, fitted parameters, or predictions within the paper reduce claimed cost inequalities to quantities defined by construction from the paper's own inputs; the central construction does not rely on self-citation chains or ansatzes that collapse to prior fitted results.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The framework rests on standard type-theoretic and categorical axioms plus the novel decision to internalize cost as a preorder on every type rather than a separate monad; no free parameters or invented physical entities are introduced.

axioms (2)
  • domain assumption The phase distinction between behavioral equality and cost preorder can be maintained uniformly for arbitrary effects.
    Invoked when reformulating Calf so that cost bounds become ordinary programs; this is the load-bearing modeling choice.
  • standard math Augmented simplicial sets form a topos in which the required intrinsic preorders can be interpreted.
    Used for the semantic justification; standard background in categorical logic.

pith-pipeline@v0.9.0 · 5755 in / 1454 out tokens · 28493 ms · 2026-05-24T08:11:02.477572+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

41 extracted references · 41 canonical work pages · 2 internal anchors

  1. [1]

    Séminaire de Géométrie Algébrique du Bois-Marie 1963–1964 (SGA 4), Dirigé par M

    Springer-Verlag, Berlin. Séminaire de Géométrie Algébrique du Bois-Marie 1963–1964 (SGA 4), Dirigé par M. Artin, A. Grothendieck, et J.-L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne et B. Saint-Donat. Steve Awodey, Nicola Gambino, and Sina Hazratpour

    work page 1963

  2. [2]

    Kripke-Joyal forcing for type theory and uniform fibrations. (2021). arXiv:2110.14576 [math.LO] Unpublished manuscript. Lars Birkedal and Aleš Bizjak

    work page arXiv 2021

  3. [3]

    Higher Structures 4 (Feb

    Localization in Homotopy Type Theory. Higher Structures 4 (Feb. 2020), 1–32. Issue

    work page 2020

  4. [4]

    Cahiers de Topologie et Géométrie Différentielle Catégoriques 20, 3 (1979), 231–279

    Sur les modèles de la géométrie différentielle synthétique. Cahiers de Topologie et Géométrie Différentielle Catégoriques 20, 3 (1979), 231–279. http://eudml.org/doc/91216 Marcelo P. Fiore

    work page 1979

  5. [5]

    Mathematical Structures in Computer Science 7, 5 (Oct

    An Enrichment Theorem for an Axiomatisation of Categories of Domains and Continuous Functions. Mathematical Structures in Computer Science 7, 5 (Oct. 1997), 591–618. https://doi.org/10.1017/S0960129597002429 Marcelo P. Fiore, Andrew M. Pitts, and S. C. Steenkamp

    work page doi:10.1017/s0960129597002429 1997

  6. [6]

    Quotients, inductive types, and quotient inductive types. (2021). arXiv:2101.02994 [cs.LO] Marcelo P. Fiore and Giuseppe Rosolini

    work page arXiv 2021

  7. [7]

    The category of cpos from a synthetic viewpoint. In Thirteenth Annual Conference on Mathematical Foundations of Progamming Semantics, MFPS 1997, Carnegie Mellon University, Pittsburgh, PA, USA, March 23-26, 1997 (Electronic Notes in Theoretical Computer Science, Vol

    work page 1997

  8. [8]

    Brookes and Michael W

    , Stephen D. Brookes and Michael W. Mislove (Eds.). Elsevier, 133–150. https://doi.org/10.1016/S1571-0661(05)80165-3 Marcelo P. Fiore and Giuseppe Rosolini

    work page doi:10.1016/s1571-0661(05)80165-3

  9. [9]

    Theoretical Computer Science 264, 2 (Aug

    Domains in H. Theoretical Computer Science 264, 2 (Aug. 2001), 171–193. https://doi.org/10.1016/S0304-3975(00)00221-8 Daniel Gratzer and Jonathan Sterling

    work page doi:10.1016/s0304-3975(00)00221-8 2001

  10. [10]

    Syntactic categories for dependent type theory: sketching and adequacy. (2020). arXiv:2012.10783 [cs.LO] Unpublished manuscript. Harrison Grodin and Robert Harper

    work page arXiv 2020

  11. [11]

    Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 23:1–23:6

    , Paolo Baldan and Valeria de Paiva (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 23:1–23:6. https://doi.org/10.4230/LIPIcs.CALCO.2023.23 Harrison Grodin, Yue Niu, Jonathan Sterling, and Robert Harper

    work page doi:10.4230/lipics.calco.2023.23 2023

  12. [12]

    https://doi.org/10.1145/3580425 Proc

    agda-calf v2.0.0. https://doi.org/10.1145/3580425 Proc. ACM Program. Lang., Vol. 8, No. POPL, Article

    work page doi:10.1145/3580425

  13. [13]

    In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

    Higher-Order Modules and the Phase Distinction. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . Association for Computing Machinery, San Francisco, California, USA, 341–354. https://doi.org/10.1145/96709.96744 C. A. R. Hoare

    work page doi:10.1145/96709.96744

  14. [14]

    Algorithm 64: Quicksort. Commun. ACM 4, 7 (July 1961),

    work page 1961

  15. [15]

    https://doi.org/10.1145/366622.366644 C. A. R. Hoare

    work page doi:10.1145/366622.366644

  16. [16]

    Quicksort. Comput. J. 5, 1 (Jan. 1962), 10–16. https://doi.org/10.1093/comjnl/5.1.10 Martin Hofmann

    work page doi:10.1093/comjnl/5.1.10 1962

  17. [17]

    Proceed- ings of the ACM on Programming Languages 3, POPL (Jan

    Constructing Quotient Inductive-inductive Types. Proceed- ings of the ACM on Programming Languages 3, POPL (Jan. 2019), 2:1–2:24. https://doi.org/10.1145/3290315 G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner

    work page doi:10.1145/3290315 2019

  18. [18]

    Proceedings of the ACM on Programming Languages 4, POPL (Dec

    Recurrence Extraction for Functional Programs through Call-by-Push-Value. Proceedings of the ACM on Programming Languages 4, POPL (Dec. 2019). https: //doi.org/10.1145/3371083 Paul Blain Levy

    work page doi:10.1145/3371083 2019

  19. [19]

    Electronic Notes in Theoretical Computer Science 276 (2011), 263–289

    2-Dimensional Directed Type Theory. Electronic Notes in Theoretical Computer Science 276 (2011), 263–289. https://doi.org/10.1016/j.entcs.2011.09.026 Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII). Maria Emilia Maietti

    work page doi:10.1016/j.entcs.2011.09.026 2011

  20. [20]

    Mathematical Structures in Computer Science 15, 6 (2005), 1089–1149

    Modular correspondence between dependent type theories and categories including pretopoi and topoi. Mathematical Structures in Computer Science 15, 6 (2005), 1089–1149. https://doi.org/10.1017/S0960129505004962 Per Martin-Löf

    work page doi:10.1017/s0960129505004962 2005

  21. [21]

    iv+91 pages

    Bibliopolis. iv+91 pages. Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper. 2022a. A Cost-Aware Logical Framework. Proceedings of the ACM on Programming Languages 6, POPL (Jan. 2022). https://doi.org/10.1145/3498670 arXiv:2107.04663 [cs.PL] Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper. 2022b. agda-calf. https://doi.org/10.1...

    work page doi:10.1145/3498670 2022

  22. [22]

    Proceedings of the ACM on Programming Languages 4, POPL (Dec

    The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects. Proceedings of the ACM on Programming Languages 4, POPL (Dec. 2019). https://doi.org/10.1145/3371126 Wesley Phoa

    work page doi:10.1145/3371126 2019

  23. [23]

    Monadic Refinements for Relational Cost Analysis. Proc. ACM Program. Lang. 2, POPL, Article 36 (dec 2017), 32 pages. https://doi.org/10.1145/3158124 Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann

    work page doi:10.1145/3158124 2017

  24. [24]

    Proceedings of the ACM on Programming Languages 5, POPL (Jan

    A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis. Proceedings of the ACM on Programming Languages 5, POPL (Jan. 2021). https://doi.org/10.1145/3434308 Emily Riehl and Michael Shulman

    work page doi:10.1145/3434308 2021

  25. [25]

    Higher Structures 1 (2017), 147–224

    A type theory for synthetic ∞-categories. Higher Structures 1 (2017), 147–224. Issue

    work page 2017

  26. [26]

    arXiv:1705.07442 [math.CT] https://journals.mq.edu.au/index.php/higher_structures/article/view/36 Egbert Rijke

    work page arXiv

  27. [27]

    Classifying Types. Ph. D. Dissertation. Carnegie Mellon University. arXiv:1906.09435 Egbert Rijke, Michael Shulman, and Bas Spitters

    work page internal anchor Pith review Pith/arXiv arXiv 1906

  28. [28]

    Logical Methods in Computer Science 16 (Jan

    Modalities in homotopy type theory. Logical Methods in Computer Science 16 (Jan. 2020). Issue

    work page 2020

  29. [29]

    https://doi.org/10.23638/LMCS-16(1:2)2020 arXiv:1706.07526 [math.CT] Jonathan Sterling

    work page doi:10.23638/lmcs-16(1:2)2020 2020

  30. [30]

    First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory . Ph. D. Dissertation. Carnegie Mellon University. https://doi.org/10.5281/zenodo.6990769 Version 1.1, revised May

    work page doi:10.5281/zenodo.6990769

  31. [31]

    Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 31:1–31:25

    , Herman Geuvers (Ed.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 31:1–31:25. https://doi.org/10.4230/LIPIcs.FSCD.2019.31 arXiv:1904.08562 [cs.LO] Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer

    work page doi:10.4230/lipics.fscd.2019.31 2019

  32. [32]

    A Cubical Language for Bishop Sets.Logical Methods in Computer Science 18 (March 2022). Issue

    work page 2022

  33. [33]

    https://doi.org/10.46298/lmcs-18(1:43)2022 arXiv:2003.01491 [cs.LO] Jonathan Sterling and Robert Harper

    work page doi:10.46298/lmcs-18(1:43)2022 2022

  34. [34]

    Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. J. ACM 68, 6 (Oct. 2021). https://doi.org/10.1145/3474834 arXiv:2010.08599 [cs.PL] Taichi Uemura

    work page doi:10.1145/3474834 2021

  35. [35]

    Abstract and Concrete Type Theories . Ph. D. Dissertation. Universiteit van Amsterdam, Amsterdam. https://www.illc.uva.nl/cms/Research/Publications/Dissertations/DS-2021-09.text.pdf Taichi Uemura

    work page 2021

  36. [36]

    Mathematical Structures in Computer Science (2023), 1–46

    A general framework for the semantics of type theory. Mathematical Structures in Computer Science (2023), 1–46. https://doi.org/10.1017/S0960129523000208 Matthijs Vákár

    work page doi:10.1017/s0960129523000208 2023

  37. [37]

    In Search of Effectful Dependent Types . Ph. D. Dissertation. University of Oxford. https://doi.org/10. 48550/arXiv.1706.07997 arXiv:1706.07997 [cs.LO] Proc. ACM Program. Lang., Vol. 8, No. POPL, Article

    work page internal anchor Pith review Pith/arXiv arXiv

  38. [38]

    Definition B.1 (Phoa principle)

    10:30 Harrison Grodin, Yue Niu, Jonathan Sterling, and Robert Harper B Extended discussion of topos-theoretic semantics B.1 The Phoa Principle and the Specialization Order So far we have assumed very little about the interval objectI; many of our results depend on further assumptions, which can be organized into a single axiom due to Phoa [Phoa 1991], sta...

    work page 1991

  39. [39]

    We finally observe that this fact corresponds under both 𝑁 : Preord ↩→ Pr(∆ ) and 𝑁⊥ : Preord ↩→ Pr(∆ ⊥) to the Phoa principle in Pr(∆ ) and Pr(∆ ⊥) respectively

    × [ 1] spanned by pairs of the form (𝑖 ≤ 𝑗). We finally observe that this fact corresponds under both 𝑁 : Preord ↩→ Pr(∆ ) and 𝑁⊥ : Preord ↩→ Pr(∆ ⊥) to the Phoa principle in Pr(∆ ) and Pr(∆ ⊥) respectively. □ 14We write ¶ext ∨ − for the closed modality associated to the proposition ¶ext [Rijke et al. 2020]. Proc. ACM Program. Lang., Vol. 8, No. POPL, Article

    work page 2020

  40. [40]

    ACM Program

    Decalf: A Directed, Effectful Cost-Aware Logical Framework 10:35 Received 2023-07-11; accepted 2023-11-07 Proc. ACM Program. Lang., Vol. 8, No. POPL, Article

    work page 2023

  41. [41]

    Publication date: January 2024

    work page 2024