Document Open Access Logo

Galois Connecting Call-by-Value and Call-by-Name

Authors Dylan McDermott , Alan Mycroft

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2022.32.pdf
  • Filesize: 0.86 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
  • Theory of computation → Denotational semantics
  • Theory of computation → Categorical semantics
Keywords
  • computational effect
  • evaluation order
  • call-by-push-value
  • categorical semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We establish a general framework for reasoning about the relationship between call-by-value and call-by-name.
In languages with side-effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no side-effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving these properties. The key ingredient is Levy’s call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We construct maps between the call-by-value and call-by-name interpretations of types. We then identify properties of side-effects that imply these maps form a Galois connection. These properties hold for some side-effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates call-by-value and call-by-name. We apply the reasoning principle to example side-effects including divergence and nondeterminism.

Cite As Get BibTex

Dylan McDermott and Alan Mycroft. Galois Connecting Call-by-Value and Call-by-Name. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSCD.2022.32

Author Details

Dylan McDermott
  • Reykjavik University, Iceland
Alan Mycroft
  • University of Cambridge, UK

Funding

  • McDermott, Dylan: Supported by an EPSRC studentship, and by Icelandic Research Fund project grant no. 196323-053.

References

  1. Robert Cartwright and Matthias Felleisen. Extensible denotational language specifications. In Proceedings of the International Conference on Theoretical Aspects of Computer Software, pages 244-272. Springer, 1994. URL: https://doi.org/10.1007/3-540-57887-0_99.
  2. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pages 233-243. ACM, 2000. URL: https://doi.org/10.1145/351240.351262.
  3. Andrzej Filinski. Declarative continuations and categorical duality. Master’s thesis, University of Copenhagen, 1989. Google Scholar
  4. Andrzej Filinski. Controlling Effects. PhD thesis, Carnegie Mellon University, 1996. Google Scholar
  5. Carsten Führmann. Direct models of the computational lambda-calculus. Electronic Notes in Theoretical Computer Science, 20:245-292, 1999. URL: https://doi.org/10.1016/S1571-0661(04)80078-1.
  6. Jennifer Hackett and Graham Hutton. Call-by-need is clairvoyant call-by-value. Proc. ACM Program. Lang., 3(ICFP):114:1-114:23, 2019. URL: https://doi.org/10.1145/3341718.
  7. Jun Inoue and Walid Taha. Reasoning about multi-stage programs. Journal of Functional Programming, 26(e22), 2016. URL: https://doi.org/10.1017/S0956796816000253.
  8. Anders Kock. Monads for which structures are adjoint to units. Journal of Pure and Applied Algebra, 104(1):41-59, 1995. URL: https://doi.org/10.1016/0022-4049(94)00111-U.
  9. Jakov Kučan. Retraction approach to cps transform. Higher Order Symbol. Comput., 11(2):145-175, 1998. URL: https://doi.org/10.1023/A:1010012532463.
  10. Julia L. Lawall and Olivier Danvy. Separating stages in the continuation-passing style transformation. In Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 124-136. ACM, 1993. URL: https://doi.org/10.1145/158511.158613.
  11. Paul Blain Levy. Call-by-push-value: A subsuming paradigm. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, pages 228-243. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_17.
  12. Paul Blain Levy. Adjunction models for call-by-push-value with stacks. Electronic Notes in Theoretical Computer Science, 69:248-271, 2003. CTCS'02, Category Theory and Computer Science. URL: https://doi.org/10.1016/S1571-0661(04)80568-1.
  13. Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, 19(4):377-414, 2006. URL: https://doi.org/10.1007/s10990-006-0480-6.
  14. John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-by-value, call-by-need, and the linear lambda calculus. In Proceedings of the Eleventh Annual Mathematical Foundations of Programming Semantics Conference, pages 370-392, 1995. URL: https://doi.org/10.1016/S1571-0661(04)00022-2.
  15. Dylan McDermott and Alan Mycroft. Extended call-by-push-value: Reasoning about effectful programs and evaluation order. In Luís Caires, editor, Programming Languages and Systems, pages 235-262. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_9.
  16. Dylan McDermott and Alan Mycroft. Galois connecting call-by-value and call-by-name (extended version), 2022. URL: http://arxiv.org/abs/2202.08246.
  17. Dylan McDermott and Tarmo Uustalu. What makes a strong monad? In Proceedings Ninth Workshop on Mathematically Structured Functional Programming (to appear). Open Publishing Association, 2022. Google Scholar
  18. Austin Melton, David A. Schmidt, and George E. Strecker. Galois connections and computer science applications. In Category Theory and Computer Programming, pages 299-312. Springer, 1986. URL: https://doi.org/10.1007/3-540-17162-2_130.
  19. Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi. In Rohit Parikh, editor, Logics of Programs, pages 219-224. Springer, 1985. URL: https://doi.org/10.1007/3-540-15648-8_17.
  20. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  21. Max S. New and Daniel R. Licata. Call-by-name gradual type theory. Logical Methods in Computer Science, 16, 2020. URL: https://doi.org/10.23638/LMCS-16(1:7)2020.
  22. Max S. New, Daniel R. Licata, and Amal Ahmed. Gradual type theory. Journal of Functional Programming, 31, 2021. URL: https://doi.org/10.1017/S0956796821000125.
  23. Michel Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning, pages 190-201. Springer, 1992. URL: https://doi.org/10.1007/BFb0013061.
  24. G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  25. John C. Reynolds. On the relation between direct and continuation semantics. In Proceedings of the 2nd Colloquium on Automata, Languages and Programming, pages 141-156. Springer, 1974. URL: https://doi.org/10.1007/978-3-662-21545-6_10.
  26. Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. In Proceedings of the 1992 ACM Conference on LISP and Functional Programming, pages 288-298. ACM, 1992. URL: https://doi.org/10.1145/141471.141563.
  27. Amr Sabry and Philip Wadler. A reflection on call-by-value. In Proceedings of the First ACM SIGPLAN International Conference on Functional Programming, pages 13-24. ACM, 1996. URL: https://doi.org/10.1145/232627.232631.
  28. José Espírito Santo, Luís Pinto, and Tarmo Uustalu. Plotkin’s call-by-value λ-calculus as a modal calculus. Journal of Logical and Algebraic Methods in Programming, 2022. URL: https://doi.org/10.1016/j.jlamp.2022.100775.
  29. Peter Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical Structures in Computer Science, 11(2):207-260, 2001. URL: https://doi.org/10.1017/S096012950000311X.
  30. Philip Wadler. Call-by-value is dual to call-by-name. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pages 189-201. ACM, 2003. URL: https://doi.org/10.1145/944705.944723.
  31. Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993. URL: https://doi.org/10.7551/mitpress/3054.001.0001.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact