Ugo Dal Lago
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent, usage-sensitive computations, especially when combined with computational effects. From a semantic perspective, effectful and coeffectful languages have been studied mostly by means of denotational semantics and almost nothing has been done from the point of view of relational reasoning. This gap in the literature is quite surprising, since many cornerstone results — such as non-interference, metric preservation, and proof irrelevance — on concrete coeffects are inherently relational. In this paper, we fill this gap by developing a general theory and calculus of program relations for higher-order languages with combined effects and coeffects. The relational calculus builds upon the novel notion of a corelator (or comonadic lax extension) to handle coeffects relationally. Inside such a calculus, we define three notions of effectful and coeffectful program refinements: contextual approximation, logical preorder, and applicative similarity. These are the first operationally-based notions of program refinement (and, consequently, equivalence) for languages with combined effects and coeffects appearing in the literature. We show that the axiomatics of a corelator (together with the one of a relator) is precisely what is needed to prove all the aforementioned program refinements to be precongruences, this way obtaining compositional relational techniques for reasoning about combined effects and coeffects.
Supplemental Material
- Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. 1999. A Core Calculus of Dependency. In Proc. of POPL 1999. 147–160. https://doi.org/10.1145/292540.292555 Google Scholar
Digital Library
- Andreas Abel and Jean-Philippe Bernardy. 2020. A unified view of modalities in type systems. Proc. ACM Program. Lang., 4, ICFP (2020), 90:1–90:28. https://doi.org/10.1145/3408972 Google ScholarDigital Library
- S. Abramsky. 1990. The Lazy Lambda Calculus. In Research Topics in Functional Programming, D. Turner (Ed.). Addison Wesley, 65–117.Google ScholarDigital Library
- S. Abramsky and A. Jung. 1994. Domain Theory. In Handbook of Logic in Computer Science. Clarendon Press, 1–168.Google Scholar
- Amal J. Ahmed. 2006. Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In Proc. of ESOP 2006. 69–83. https://doi.org/10.1007/11693024_6 Google ScholarDigital Library
- A.W. Appel and D.A. McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23, 5 (2001), 657–683. https://doi.org/10.1145/504709.504712 Google ScholarDigital Library
- Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Proc. of LICS 2018. 56–65. https://doi.org/10.1145/3209108.3209189 Google ScholarDigital Library
- Roland Carl Backhouse, Peter J. de Bruin, Paul F. Hoogendijk, Grant Malcolm, Ed Voermans, and Jaap van der Woude. 1991. Polynomial Relators (Extended Abstract). In Proc. of (AMAST ’91 (Workshops in Computing). Springer, 303–326.Google Scholar
- H.P. Barendregt. 1984. The lambda calculus: its syntax and semantics. North-Holland.Google Scholar
- M. Barr. 1970. Relational algebras. Lect. Notes Math., 137 (1970), 39–55.Google ScholarCross Ref
- Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang., 2, POPL (2018), 57:1–57:29. https://doi.org/10.1145/3158145 Google ScholarDigital Library
- P. N. Benton and Philip Wadler. 1996. Linear Logic, Monads and the Lambda Calculus. In Proc. of LICS 1996. 420–431. https://doi.org/10.1109/LICS.1996.561458 Google ScholarCross Ref
- Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2018. Linear Haskell: practical linearity in a higher-order polymorphic language. PACMPL, 2, POPL (2018), 5:1–5:29. https://doi.org/10.1145/3158093 Google ScholarDigital Library
- Gavin M. Bierman and Valeria de Paiva. 2000. On an Intuitionistic Modal Logic. Stud Logica, 65, 3 (2000), 383–416. https://doi.org/10.1023/A:1005291931660 Google ScholarCross Ref
- A. Bizjak and L. Birkedal. 2015. Step-Indexed Logical Relations for Probability. In Proc. of FOSSACS 2015. 279–294. https://doi.org/10.1007/978-3-662-46678-0_18 Google ScholarCross Ref
- Flavien Breuvart and Michele Pagani. 2015. Modelling Coeffects in the Relational Semantics of Linear Logic. In Proc. of CSL 2015. 567–581. https://doi.org/10.4230/LIPIcs.CSL.2015.567 Google ScholarCross Ref
- Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Proc. of ESOP 2014. 351–370. https://doi.org/10.1007/978-3-642-54833-8_19 Google ScholarDigital Library
- Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. 2021. A graded dependent type system with a usage-aware semantics. Proc. ACM Program. Lang., 5, POPL (2021), 1–32. https://doi.org/10.1145/3434331 Google ScholarDigital Library
- Maria Manuel Clementino, Dirk Hofmann, and Walter Tholen. 2004. One Setting for All: Metric, Topology, Uniformity, Approach Structure. Appl. Categorical Struct., 12, 2 (2004), 127–154. https://doi.org/10.1023/B:APCS.0000018144.87456.10 Google ScholarCross Ref
- Ryan Culpepper and Andrew Cobb. 2017. Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring. In Proc. of ESOP 2017. 368–392. https://doi.org/10.1007/978-3-662-54434-1_14 Google ScholarDigital Library
- Ugo Dal Lago and Francesco Gavazzo. 2019. Effectful Normal Form Bisimulation. In Proc. of ESOP 2019. 263–292. https://doi.org/10.1007/978-3-030-17184-1_10 Google ScholarCross Ref
- Ugo Dal Lago and Francesco Gavazzo. 2019. On Bisimilarity in Lambda Calculi with Continuous Probabilistic Choice. In Proc. of MFPS 2019. 121–141. https://doi.org/10.1016/j.entcs.2019.09.007 Google ScholarDigital Library
- Ugo Dal Lago and Francesco Gavazzo. 2020. Differential Logical Relations Part II: Increments and Derivatives. In Proc. of ICTCS 2020. 101–114.Google Scholar
- Ugo Dal Lago and Francesco Gavazzo. 2021. Differential logical relations, part II increments and derivatives. Theoretical Computer Science, issn:0304-3975 https://doi.org/10.1016/j.tcs.2021.09.027 Google ScholarDigital Library
- Ugo Dal Lago and Francesco Gavazzo. 2021. Modal Reasoning = Metric Reasoning, via Lawvere. CoRR, abs/2103.03871 (2021), arxiv:2103.03871Google Scholar
- Ugo Dal Lago and Francesco Gavazzo. 2021. Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs. In Proc. of FSCD 2021 (LIPIcs, Vol. 195). 23:1–23:19. https://doi.org/10.4230/LIPIcs.FSCD.2021.23 Google ScholarCross Ref
- Ugo Dal Lago and Francesco Gavazzo. 2022. Effectful Program Distancing. Proc. ACM Program. Lang., 6, POPL (2022), https://doi.org/10.1145/3498680 Google ScholarDigital Library
- Ugo Dal Lago, Francesco Gavazzo, and Paul Blain Levy. 2017. Effectful applicative bisimilarity: Monads, relators, and Howe’s method. In Proc. of LICS 2017. 1–12. https://doi.org/10.1109/LICS.2017.8005117 Google ScholarCross Ref
- Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. 2017. Effectful Applicative Similarity for Call-by-Name Lambda Calculi. In Proc. of ICTCS 2017. 87–98.Google Scholar
- Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. 2020. Effectful applicative similarity for call-by-name lambda calculi. Theor. Comput. Sci., 813 (2020), 234–247. https://doi.org/10.1016/j.tcs.2019.12.025 Google ScholarDigital Library
- Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. 2019. Differential Logical Relations, Part I: The Simply-Typed Case. In Proc. of ICALP 2019. 111:1–111:14. https://doi.org/10.4230/LIPIcs.ICALP.2019.111 Google ScholarCross Ref
- Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. 2014. On coinductive equivalences for higher-order probabilistic functional programs. In Proc. of POPL 2014. 297–308. https://doi.org/10.1145/2535838.2535872 Google ScholarDigital Library
- A.A. de Amorim, M. Gaboardi, J. Hsu, S. Katsumata, and I. Cherigui. 2017. A semantic account of metric preservation. In Proc. of POPL 2017. 545–556. https://doi.org/10.1145/3009837.3009890 Google ScholarDigital Library
- Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata. 2019. Probabilistic Relational Reasoning via Metrics. In Proc. of LICS 2019. 1–19. https://doi.org/10.1109/LICS.2019.8785715 Google ScholarCross Ref
- Dorothy E. Denning. 1976. A Lattice Model of Secure Information Flow. Commun. ACM, 19, 5 (1976), 236–243. https://doi.org/10.1145/360051.360056 Google ScholarDigital Library
- Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining effects and coeffects via grading. In Proc. of ICFP 2016. 476–489. https://doi.org/10.1145/2951913.2951939 Google ScholarDigital Library
- Francesco Gavazzo. 2018. Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances. In Proc. of LICS 2018. 452–461. https://doi.org/10.1145/3209108.3209149 Google ScholarDigital Library
- Francesco Gavazzo. 2019. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation. University of Bologna, Italy. http://amsdottorato.unibo.it/9075/Google Scholar
- Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Proc. of ESOP 2014. 331–350. https://doi.org/10.1007/978-3-642-54833-8_18 Google ScholarDigital Library
- Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci., 50 (1987), 1–102. https://doi.org/10.1006/inco.1998.2700 Google ScholarDigital Library
- J-Y. Girard, A. Scedrov, and P.J. Scott. 1992. Bounded Linear Logic: A Modular Approach to Polynomial-Time Computability. Theor. Comput. Sci., 97 (1992), 1–66. https://doi.org/10.1016/0304-3975(92)90386-T Google ScholarDigital Library
- Joseph A. Goguen, James W. Thatcher, Eric G. Wagner, and Jesse B. Wright. 1977. Initial Algebra Semantics and Continuous Algebras. J. ACM, 24, 1 (1977), 68–95. https://doi.org/10.1145/321992.321997 Google ScholarDigital Library
- A.D. Gordon. 1994. A Tutorial on Co-induction and Functional Programming. In Workshops in Computing. Springer London, 78–95. https://doi.org/10.1007/978-1-4471-3573-9_6 Google ScholarCross Ref
- Andrew Donald Gordon. 1992. Functional programming and input/output. Ph. D. Dissertation. University of Cambridge, UK.Google Scholar
- Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. 2008. Logical relations for monadic types. Math. Struc. Comput. Sci., 18, 6 (2008), 1169–1217. https://doi.org/10.1017/S0960129508007172 Google ScholarDigital Library
- Robert Harper. 2016. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press.Google Scholar
- D. Hoffman. 2015. A cottage industry of lax extensions. Categories and General Algebraic Structures with Applications, 3, 1 (2015), 113–151.Google Scholar
- 2014. Monoidal Topology. A Categorical Approach to Order, Metric, and Topology, D. Hofmann, G.J. Seal, and W. Tholen (Eds.) (Encyclopedia of Mathematics and its Applications). Cambridge University Press.Google Scholar
- D.J. Howe. 1996. Proving Congruence of Bisimulation in Functional Programming Languages. Inf. Comput., 124, 2 (1996), 103–112. https://doi.org/10.1006/inco.1996.0008 Google ScholarDigital Library
- Martin Hyland, Gordon D. Plotkin, and John Power. 2006. Combining effects: Sum and tensor. Theor. Comput. Sci., 357, 1-3 (2006), 70–99. https://doi.org/10.1016/j.tcs.2006.03.013 Google ScholarDigital Library
- Patricia Johann, Alex Simpson, and Janis Voigtländer. 2010. A Generic Operational Metatheory for Algebraic Effects. In Proc. of LICS 2010. IEEE Computer Society, 209–218. https://doi.org/10.1109/LICS.2010.29 Google ScholarDigital Library
- Shin-ya Katsumata. 2018. A Double Category Theoretic Analysis of Graded Linear Exponential Comonads. In Proc. of FOSSACS 2018. 110–127. https://doi.org/10.1007/978-3-319-89366-2_6 Google ScholarCross Ref
- Yasuo Kawahara. 1973. Notes on the universality of relational functors. Memoirs of the Faculty of Science, Kyushu University. Series A, Mathematics, 27, 2 (1973), 275–289.Google Scholar
- Joachim Lambek. 1968. Deductive Systems and Categories I. Syntactic Calculus and Residuated Categories. Math. Syst. Theory, 2, 4 (1968), 287–318. https://doi.org/10.1007/BF01703261 Google ScholarCross Ref
- S.B. Lassen. 1998. Relational Reasoning About Contexts. In Higher Order Operational Techniques in Semantics, Andrew D. Gordon and Andrew M. Pitts (Eds.). 91–136.Google Scholar
- S.B. Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation. Dept. of Computer Science, University of Aarhus.Google Scholar
- Søren B. Lassen. 1999. Bisimulation in Untyped Lambda Calculus: Böhm Trees and Bisimulation up to Context. Electr. Notes Theor. Comput. Sci., 20 (1999), 346–374. https://doi.org/10.1016/S1571-0661(04)80083-5 Google ScholarCross Ref
- Søren B. Lassen. 2005. Eager Normal Form Bisimulation. In Proc. of LICS 2005. 345–354. https://doi.org/10.1109/LICS.2005.15 Google ScholarDigital Library
- F.W. Lawvere. 1973. Metric spaces, generalized logic, and closed categories. Rend. Sem. Mat. Fis. Milano, 43 (1973), 135–166.Google ScholarCross Ref
- P.B. Levy, J. Power, and H. Thielecke. 2003. Modelling Environments in Call-by-Value Programming Languages. Inf. Comput., 185, 2 (2003), 182–210. https://doi.org/10.1016/S0890-5401(03)00088-9 Google ScholarDigital Library
- S. MacLane. 1971. Categories for the Working Mathematician. Springer-Verlag.Google Scholar
- J. Maraist, M. Odersky, D.N. Turner, and P. Wadler. 1999. Call-by-name, Call-by-value, Call-by-need and the Linear lambda Calculus. Theor. Comput. Sci., 228, 1-2 (1999), 175–210. https://doi.org/10.1016/S0304-3975(98)00358-2 Google ScholarDigital Library
- Ian A. Mason and Carolyn L. Talcott. 1991. Equivalence in Functional Languages with Effects. J. Funct. Program., 1, 3 (1991), 287–327. https://doi.org/10.1017/S0956796800000125 Google ScholarCross Ref
- John McCarthy. 1961. A basis for a mathematical theory of computation, preliminary report. In Papers presented at the 1961 western joint IRE-AIEE-ACM computer conference, IRE-AIEE-ACM 1961 (Western), Los Angeles, California, USA, May 9-11, 1961. 225–238. https://doi.org/10.1145/1460690.1460715 Google ScholarDigital Library
- John McCarthy. 1962. Towards a Mathematical Science of Computation. In Proc. of IFIP 1962. 21–28.Google Scholar
- John McCarthy. 1963. A Basis for a Mathematical Theory of Computation). In Computer Programming and Formal Systems, P. Braffort and D. Hirschberg (Eds.) (Studies in Logic and the Foundations of Mathematics, Vol. 35). Elsevier, 33 – 70.Google Scholar
- John C. Mitchell. 1996. Foundations for programming languages. MIT Press.Google ScholarDigital Library
- Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads. In Proc. of LICS 1989. IEEE Computer Society, 14–23. https://doi.org/10.1109/LICS.1989.39155 Google ScholarCross Ref
- Eugenio Moggi. 1991. Notions of Computation and Monads. Inf. Comput., 93, 1 (1991), 55–92. https://doi.org/10.1016/0890-5401(91)90052-4 Google ScholarDigital Library
- J. Morris. 1969. Lambda Calculus Models of Programming Languages. Ph. D. Dissertation. MIT.Google Scholar
- C.-H. Luke Ong. 1993. Non-Determinism in a Functional Setting. In Proc. of LICS 1993. IEEE Computer Society, 275–286. https://doi.org/10.1109/LICS.1993.287580 Google ScholarCross Ref
- Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. 2019. Quantitative Program Reasoning with Graded Modal Types. Proc. ACM Program. Lang., 3, ICFP (2019), Article 110, 110:1–110:30 pages. https://doi.org/10.1145/3341714 Google ScholarDigital Library
- Dominic A. Orchard. 2014. Programming contextual computations. Ph. D. Dissertation. University of Cambridge, UK.Google Scholar
- Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. 2014. Coeffects: a calculus of context-dependent computation. In Proc. of ICFP 2014. 123–135. https://doi.org/10.1145/2628136.2628160 Google ScholarDigital Library
- Frank Pfenning. 2001. Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In Proc. of LICS 2001. 221–230. https://doi.org/10.1109/LICS.2001.932499 Google ScholarCross Ref
- Frank Pfenning and Rowan Davies. 2001. A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci., 11, 4 (2001), 511–540. https://doi.org/10.1017/S0960129501003322 Google ScholarDigital Library
- Frank Pfenning and Hao-Chi Wong. 1995. On a modal lambda calculus for S4. In Proc. of MFPS 1995. 515–534. https://doi.org/10.1016/S1571-0661(04)00028-3 Google ScholarCross Ref
- A.M. Pitts. 2011. Howe’s Method for Higher-Order Languages. In Advanced Topics in Bisimulation and Coinduction, D. Sangiorgi and J. Rutten (Eds.) (Cambridge Tracts in Theoretical Computer Science, Vol. 52). Cambridge University Press, 197–232.Google Scholar
- A. M. Pitts. 1997. Operationally-Based Theories of Program Equivalence. In Semantics and Logics of Computation, P. Dybjer and A. M. Pitts (Eds.). Cambridge University Press, 241–298.Google Scholar
- Gordon Plotkin. 1973. Lambda-definability and logical relations. Technical Report SAI-RM-4, School of A.I., University of EdinburghGoogle Scholar
- Gordon D. Plotkin and John Power. 2001. Adequacy for Algebraic Effects. In Proc. of FOSSACS 2001. 1–24. https://doi.org/10.1007/3-540-45315-6_1 Google ScholarCross Ref
- Gordon D. Plotkin and John Power. 2001. Semantics for Algebraic Operations. Electr. Notes Theor. Comput. Sci., 45 (2001), 332–345. https://doi.org/10.1016/S1571-0661(04)80970-8 Google ScholarCross Ref
- Gordon D. Plotkin and John Power. 2003. Algebraic Operations and Generic Effects. Applied Categorical Structures, 11, 1 (2003), 69–94. https://doi.org/10.1023/A:1023064908962 Google ScholarCross Ref
- J. Reed and B.C. Pierce. 2010. Distance makes the types grow stronger: a calculus for differential privacy. In Proc. of ICFP 2010. 157–168. https://doi.org/10.1145/1863543.1863568 Google ScholarDigital Library
- J.C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In IFIP Congress. 513–523.Google Scholar
- Richard Routley and Robert K. Meyer. 1973. The Semantics of Entailment. In Truth, Syntax and Modality, Hugues Leblanc (Ed.) (Studies in Logic and the Foundations of Mathematics, Vol. 68). Elsevier, 199 – 243.Google Scholar
- Davide Sangiorgi. 1994. The Lazy Lambda Calculus in a Concurrency Scenario. Inf. Comput., 111, 1 (1994), 120–153. https://doi.org/10.1006/inco.1994.1042 Google ScholarDigital Library
- Mícheál Ó Searcóid. 2006. Metric Spaces. Springer London.Google Scholar
- A. Simpson and N. Voorneveld. 2018. Behavioural equivalence via modalities for algebraic effects. In Proc. of ESOP 2018. 300–326. https://doi.org/10.1007/978-3-319-89884-1_11 Google ScholarCross Ref
- Alex Simpson and Niels F. W. Voorneveld. 2020. Behavioural Equivalence via Modalities for Algebraic Effects. ACM Trans. Program. Lang. Syst., 42, 1 (2020), 4:1–4:45. https://doi.org/10.1145/3363518 Google ScholarDigital Library
- Alex K. Simpson. 1994. The proof theory and semantics of intuitionistic modal logic. Ph. D. Dissertation. University of Edinburgh, UK.Google Scholar
- Alasdair Urquhart. 1972. Semantics for Relevant Logics. J. Symb. Log., 37, 1 (1972), 159–169. https://doi.org/10.2307/2272559 Google ScholarCross Ref
- Dennis M. Volpano, Cynthia E. Irvine, and Geoffrey Smith. 1996. A Sound Type System for Secure Flow Analysis. Journal of Computer Security, 4, 2/3 (1996), 167–188. https://doi.org/10.3233/JCS-1996-42-304 Google ScholarCross Ref
Index Terms
- A relational theory of effects and coeffects
Recommendations
Combining effects and coeffects via grading
ICFP '16Effects and coeffects are two general, complementary aspects of program behaviour. They roughly correspond to computations which change the execution context (effects) versus computations which make demands on the context (coeffects). Effectful ...
Combining effects and coeffects via grading
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingEffects and coeffects are two general, complementary aspects of program behaviour. They roughly correspond to computations which change the execution context (effects) versus computations which make demands on the context (coeffects). Effectful ...
Coeffects: a calculus of context-dependent computation
ICFP '14The notion of context in functional languages no longer refers just to variables in scope. Context can capture additional properties of variables (usage patterns in linear logics; caching requirements in dataflow languages) as well as additional ...
Comments