The Duality of λ-Abstraction

conference
category theory
classical logic
continuations
control effects
control operators
curry-howard
denotational semantics
duality
equational theory
lambda-calculus
Authors
Affiliations

Vikraman Choudhury

Università di Bologna, Bologna, Italy

Simon J. Gay

University of Glasgow, Glasgow, UK

Published

January 7, 2025

Doi

10.1145/3704848

Abstract

In this paper, we develop and study the following perspective – just as higher-order functions give exponentials, higher-order continuations give coexponentials. From this, we design a language that combines exponentials and coexponentials, producing a duality of lambda abstraction.

We formalise this language by giving an extension of a call-by-value simply-typed lambda-calculus with covalues, coabstraction, and coapplication. We develop the semantics of this language using the axiomatic structure of continuations, which we use to produce an equational theory, that gives a complete axiomatisation of control effects. We give a computational interpretation to this language using speculative execution and backtracking, and use this to derive the classical control operators and computational interpretation of classical logic, and encode common patterns of control flow using continuations. By dualising functional completeness, we further develop duals of first-order arrow languages using coexponentials. Finally, we discuss the implementation of this duality as control operators in programming, and develop some applications.

Keywords

category theory, classical logic, continuations, control effects, control operators, curry-howard, denotational semantics, duality, equational theory, lambda-calculus

Back to top

Citation

BibTeX citation:
@inproceedings{choudhury2025,
  author = {Choudhury, Vikraman and J. Gay, Simon},
  title = {The {Duality} of {λ-Abstraction}},
  booktitle = {Proceedings of the ACM on Programming Languages, Volume
    9, Number POPL},
  date = {2025},
  url = {https://doi.org/10.1145/3704848},
  doi = {10.1145/3704848},
  langid = {en},
  abstract = {In this paper, we develop and study the following
    perspective -\/- just as higher-order functions give exponentials,
    higher-order continuations give coexponentials. From this, we design
    a language that combines exponentials and coexponentials, producing
    a duality of lambda abstraction. We formalise this language by
    giving an extension of a call-by-value simply-typed lambda-calculus
    with covalues, coabstraction, and coapplication. We develop the
    semantics of this language using the axiomatic structure of
    continuations, which we use to produce an equational theory, that
    gives a complete axiomatisation of control effects. We give a
    computational interpretation to this language using speculative
    execution and backtracking, and use this to derive the classical
    control operators and computational interpretation of classical
    logic, and encode common patterns of control flow using
    continuations. By dualising functional completeness, we further
    develop duals of first-order arrow languages using coexponentials.
    Finally, we discuss the implementation of this duality as control
    operators in programming, and develop some applications.}
}
For attribution, please cite this work as:
Choudhury, Vikraman, and Simon J. Gay. 2025. “The Duality of λ-Abstraction.” Proceedings of the ACM on Programming Languages, Volume 9, Number POPL, accepted. https://doi.org/10.1145/3704848.