Recovering purity with comonads and capabilities

Abstract

In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to extend it to permit capturing pure expressions with types. Our key observation is that, just as the pure simply-typed lambda calculus can be extended to support effects with a monadic type discipline, an impure typed lambda calculus can be extended to support purity with a comonadic type discipline.

We establish the correctness of our type system via a simple denotational model, which we call the capability space model. Our model formalises the intuition common to systems programmers that the ability to perform effects should be controlled via access to a permission or capability, and that a program is capability-safe if it performs no effects that it does not have a runtime capability for. We then identify the axiomatic categorical structure that the capability space model validates, and use these axioms to give a categorical semantics for our comonadic type system. We then give an equational theory (substitution and the call-by-value β and η laws) for the imperative lambda calculus, and show its soundness relative to this semantics.

Finally, we give a translation of the pure simply-typed lambda calculus into our comonadic imperative calculus, and show that any two terms which are βη-equal in the STLC are equal in the equational theory of the comonadic calculus, establishing that pure programs can be mapped in an equation-preserving way into our imperative calculus.

Citation

BibTeX citation:

@inproceedings{choudhury2020,
  author = {Choudhury, Vikraman and Krishnaswami, Neel},
  title = {Recovering Purity with Comonads and Capabilities},
  booktitle = {Proceedings of the ACM on Programming Languages},
  date = {2020},
  url = {https://doi.org/10.1145/3408993},
  doi = {10.1145/3408993},
  langid = {en},
  abstract = {In this paper, we take a pervasively effectful (in the
    style of ML) typed lambda calculus, and show how to extend it to
    permit capturing pure expressions with types. Our key observation is
    that, just as the pure simply-typed lambda calculus can be extended
    to support effects with a monadic type discipline, an impure typed
    lambda calculus can be extended to support purity with a comonadic
    type discipline. We establish the correctness of our type system via
    a simple denotational model, which we call the capability space
    model. Our model formalises the intuition common to systems
    programmers that the ability to perform effects should be controlled
    via access to a permission or capability, and that a program is
    capability-safe if it performs no effects that it does not have a
    runtime capability for. We then identify the axiomatic categorical
    structure that the capability space model validates, and use these
    axioms to give a categorical semantics for our comonadic type
    system. We then give an equational theory (substitution and the
    call-by-value β and η laws) for the imperative lambda calculus, and
    show its soundness relative to this semantics. Finally, we give a
    translation of the pure simply-typed lambda calculus into our
    comonadic imperative calculus, and show that any two terms which are
    βη-equal in the STLC are equal in the equational theory of the
    comonadic calculus, establishing that pure programs can be mapped in
    an equation-preserving way into our imperative calculus.}
}

For attribution, please cite this work as:

Choudhury, Vikraman, and Neel Krishnaswami. 2020. “Recovering Purity with Comonads and Capabilities.” Proceedings of the ACM on Programming Languages, accepted. https://doi.org/10.1145/3408993.