research-article

Open access

Quantitative program reasoning with graded modal types

Authors:

Dominic Orchard,

Vilem-Benjamin Liepelt,

Harley Eades IIIAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue ICFP

Article No.: 110, Pages 1 - 30

https://doi.org/10.1145/3341714

Published: 26 July 2019 Publication History

Abstract

In programming, some data acts as a resource (e.g., file handles, channels) subject to usage constraints. This poses a challenge to software correctness as most languages are agnostic to constraints on data. The approach of linear types provides a partial remedy, delineating data into resources to be used but never copied or discarded, and unconstrained values. Bounded Linear Logic provides a more fine-grained approach, quantifying non-linear use via an indexed-family of modalities. Recent work on coeffect types generalises this idea to graded comonads, providing type systems which can capture various program properties. Here, we propose the umbrella notion of graded modal types, encompassing coeffect types and dual notions of type-based effect reasoning via graded monads. In combination with linear and indexed types, we show that graded modal types provide an expressive type theory for quantitative program reasoning, advancing the reach of type systems to capture and verify a broader set of program properties. We demonstrate this approach via a type system embodied in a fully-fledged functional language called Granule, exploring various examples.

Supplementary Material

Auxiliary Archive (icfp19main-p84-p-aux.zip)

Appendix

Download
1.57 MB

WEBM File (a110-orchard.webm)

Download
103.37 MB

References

[1]

Samson Abramsky. 1993. Computational interpretations of linear logic. Theoretical computer science 111, 1-2 (1993), 3–57.

Digital Library

[2]

Michael Arntzenius and Neelakantan R. Krishnaswami. 2016. Datafun: a functional Datalog. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016. 214–227.

Digital Library

[3]

Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. 56–65.

Digital Library

[4]

Robert Atkey and James Wood. 2018. Context Constrained Computation. In Workshop on Type-Driven Development, colocated with ICFP 2018.

[5]

Andrew Barber and Gordon Plotkin. 1996. Dual intuitionistic linear logic. University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science.

[6]

Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The SMT-LIB Standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England), Vol. 13. 14.

[7]

P. Nick Benton, Gavin M. Bierman, and Valeria de Paiva. 1998. Computational Types from a Logical Perspective. J. Funct. Program. 8, 2 (1998), 177–193. http://journals.cambridge.org/action/displayAbstract?aid=44159

Digital Library

[8]

Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R Newton, Simon Peyton Jones, and Arnaud Spiwack. 2017. Linear Haskell: Practical linearity in a higher-order polymorphic language. Proceedings of the ACM on Programming Languages 2, POPL (2017), 5.

Digital Library

[9]

Gavin M. Bierman and Valeria CV de Paiva. 2000. On an intuitionistic modal logic. Studia Logica 65, 3 (2000), 383–416.

[10]

Flavien Breuvart and Michele Pagani. 2015. Modelling coeffects in the relational semantics of linear logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[11]

Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A core quantitative coeffect calculus. In European Symposium on Programming Languages and Systems. Springer, 351–370.

Digital Library

[12]

TH Brus, Marko CJD van Eekelen, MO Van Leer, and Marinus J Plasmeijer. 1987. Clean—a language for functional graph rewriting. In Conference on Functional Programming Languages and Computer Architecture. Springer, 364–384.

Digital Library

[13]

Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings. 222–236.

Digital Library

[14]

Iliano Cervesato and Frank Pfenning. 2002. A linear logical framework. Information and Computation 179, 1 (2002), 19–75.

Digital Library

[15]

Ugo Dal Lago and Marco Gaboardi. 2011. Linear dependent types and relative completeness. In Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on. IEEE, 133–142.

Digital Library

[16]

Nils Anders Danielsson. 2008. Lightweight semiformal time complexity analysis for purely functional data structures. In ACM SIGPLAN Notices, Vol. 43. ACM, 133–144.

Digital Library

[17]

Arthur Azevedo De Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu. 2014. Really Natural Linear Indexed Type Checking. In Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages. ACM, 5.

Digital Library

[18]

Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. 2017. A semantic account of metric preservation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 545–556. http://dl.acm.org/citation.cfm?id=3009890

Digital Library

[19]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340.

Digital Library

[20]

Joshua Dunfield and Neelakantan R Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rank polymorphism. In ACM SIGPLAN Notices, Vol. 48. ACM, 429–442.

Digital Library

[21]

Joshua Dunfield and Neelakantan R. Krishnaswami. 2019. Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. PACMPL 3, POPL (2019), 9:1–9:28. https://dl.acm.org/citation.cfm? id=3290322

Digital Library

[22]

Joshua Dunfield and Frank Pfenning. 2004. Tridirectional Typechecking. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’04). ACM, New York, NY, USA, 281–292.

Digital Library

[23]

Soichiro Fujii, Shinya Katsumata, and Paul-André Melliès. 2016. Towards a formal theory of graded monads. In FOSSACS. Springer, 513–530.

[24]

Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C Pierce. 2013. Linear dependent types for differential privacy. In POPL. 357–370. http://dl.acm.org/citation.cfm?id=2429113

Digital Library

[25]

Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining effects and coeffects via grading. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016. 476–489.

Digital Library

[26]

Simon J. Gay and Vasco Thudichum Vasconcelos. 2010. Linear type theory for asynchronous session types. J. Funct. Program. 20, 1 (2010), 19–50.

Digital Library

[27]

Dan R. Ghica and Alex I. Smith. 2014. Bounded linear types in a resource semiring. In Programming Languages and Systems. Springer, 331–350.

Digital Library

[28]

Jean-Yves Girard. 1987. Linear logic. Theoretical computer science 50, 1 (1987), 1–101.

Digital Library

[29]

Jean-Yves Girard, Andre Scedrov, and Philip J Scott. 1992. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical computer science 97, 1 (1992), 1–66.

Digital Library

[30]

Joshua S Hodas. 1994. Logic Programming in Intutionistic Linear Logic: Theory, Design and Implementation. PhD Thesis, University of Pennsylvania, Department of Computer and Information Science (1994).

[31]

Futoshi Iwama, Atsushi Igarashi, and Naoki Kobayashi. 2006. Resource usage analysis for a functional language with exceptions. In Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation (PEPM). ACM, 38–47.

Digital Library

[32]

Simon Peyton Jones. 2003. Haskell 98 language and libraries: the revised report. Cambridge University Press.

[33]

Shin-ya Katsumata. 2014. Parametric effect monads and semantics of effect systems. In Proceedings of POPL 2014. ACM, 633–645.

Digital Library

[34]

Shin-ya Katsumata. 2018. A Double Category Theoretic Analysis of Graded Linear Exponential Comonads. In International Conference on Foundations of Software Science and Computation Structures. Springer, 110–127.

[35]

Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). ACM, New York, NY, USA, 17–30.

Digital Library

[36]

Nicholas D Matsakis and Felix S Klock II. 2014. The Rust Language. In ACM SIGAda Ada Letters, Vol. 34. ACM, 103–104.

Digital Library

[37]

Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. 2010. Lightweight linear types in System F ◦ . In Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Madrid, Spain, January 23, 2010. 77–88.

Digital Library

[38]

Conor McBride. 2016. I got Plenty o’ Nuttin’. In A List of Successes That Can Change the World. Springer, 207–233.

[39]

Conor McBride and James McKinna. 2004. The view from the left. Journal of functional programming 14, 1 (2004), 69–111.

Digital Library

[40]

Stefan Milius, Dirk Pattinson, and Lutz Schröder. 2015. Generic trace semantics and graded monads. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[41]

Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. 1997. The Definition of Standard ML: revised. MIT press.

Digital Library

[42]

J Garrett Morris. 2016. The best of both worlds: linear functional programming without compromise. In ACM SIGPLAN Notices, Vol. 51. ACM, 448–461.

Digital Library

[43]

Alan Mycroft, Dominic Orchard, and Tomas Petricek. 2016. Effect systems revisited – control-flow algebra and semantics. In Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays. Springer, 1–32.

Digital Library

[44]

Dominic Orchard and Vilem-Benjamin Liepelt. 2017. Gram: A linear functional language with graded modal (extended abstract). In Workshop on Trends in Linear Logic and Applications (TLLA).

[45]

Dominic A. Orchard, Tomas Petricek, and Alan Mycroft. 2014. The semantic marriage of monads and effects. CoRR abs/1401.5391 (2014). http://arxiv.org/abs/1401.5391

[46]

Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2013. Coeffects: Unified Static Analysis of Context-Dependence. In ICALP (2). 385–397.

Digital Library

[47]

Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2014. Coeffects: a calculus of context-dependent computation. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming. ACM, 123–135.

Digital Library

[48]

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006. Simple unification-based type inference for GADTs. In ACM SIGPLAN Notices, Vol. 41. ACM, 50–61.

Digital Library

[49]

Frank Pfenning and Rowan Davies. 2001. A judgmental reconstruction of modal logic. Mathematical structures in computer science 11, 4 (2001), 511–540.

Digital Library

[50]

Jeff Polakow. 2015. Embedding a Full Linear Lambda Calculus in Haskell. SIGPLAN Not. 50, 12, 177–188.

Digital Library

[51]

Dag Prawitz. 1965. Natural Deduction: A proof-theoretical study. Stockholm Studies in Philosophy. Almqvist & Wiksell, Stockholm 3 (1965).

[52]

A.L. Smirnov. 2008. Graded monads and rings of polynomials. Journal of Mathematical Sciences 151, 3 (2008), 3032–3051.

[53]

K. Terui. 2001. Light Affine Lambda Calculus and Polytime Strong Normalization. In LICS ’01. IEEE Computer Society, 209–220.

[54]

Jesse A Tov and Riccardo Pucella. 2010. Stateful contracts for affine types. In European Symposium on Programming. Springer, 550–569.

Digital Library

[55]

Jesse A. Tov and Riccardo Pucella. 2011. Practical Affine Types. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). ACM, New York, NY, USA, 447–458.

Digital Library

[56]

Philip Wadler. 1990. Linear types can change the world. In IFIP TC, Vol. 2. 347–359.

[57]

Philip Wadler. 1992. There’s no substitute for linear logic. In 8th International Workshop on the Mathematical Foundations of Programming Semantics.

[58]

Philip Wadler. 1993. A Syntax for Linear Logic. In Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings. 513–529.

[59]

David Walker. 2005. Substructural type systems. Advanced Topics in Types and Programming Languages (2005), 3–44.

[60]

Hongwei Xi. 2003. Applied type system. In International Workshop on Types for Proofs and Programs. Springer, 394–408.

[61]

Nobuko Yoshida and Vasco Thudichum Vasconcelos. 2007. Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication. Electr. Notes Theor. Comput. Sci. 171, 4 (2007), 73–93.

Digital Library

Cited By

Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Rajani VBarthe GGarg D(2024)A Modal Type Theory of Expected Cost in Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36897258:OOPSLA2(389-414)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689725
Aish RFisher AOrchard DTorry JEdwards JTaeumel M(2024)Programming Languages for the Future of Design ComputationProceedings of the 2024 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3689492.3689812(241-265)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3689492.3689812
Show More Cited By

Index Terms

Quantitative program reasoning with graded modal types
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Program specifications
      2. Program verification

Recommendations

A relational theory of effects and coeffects

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 ...
Session types revisited

Session types are a formalism used to model structured communication-based programming. A binary session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session processes ...
Session types revisited
PPDP '12: Proceedings of the 14th symposium on Principles and practice of declarative programming

Session types are a formalism to model structured communication-based programming. A session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session primitives are added to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue ICFP

August 2019

1054 pages

EISSN:2475-1421

DOI:10.1145/3352468

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 July 2019

Published in PACMPL Volume 3, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Engineering and Physical Sciences Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

53
Total Citations
View Citations
1,246
Total Downloads

Downloads (Last 12 months)307
Downloads (Last 6 weeks)44

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Rajani VBarthe GGarg D(2024)A Modal Type Theory of Expected Cost in Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36897258:OOPSLA2(389-414)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689725
Aish RFisher AOrchard DTorry JEdwards JTaeumel M(2024)Programming Languages for the Future of Design ComputationProceedings of the 2024 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3689492.3689812(241-265)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3689492.3689812
Giannini PDuso GDi Stefano L(2024)Coeffects for MiniJava: Cf-MjProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686232(30-36)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686232
Lorenzen AWhite LDolan SEisenberg RLindley S(2024)Oxidizing OCaml with Modal Memory ManagementProceedings of the ACM on Programming Languages10.1145/36746428:ICFP(485-514)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674642
Atkey R(2024)Polynomial Time and Dependent TypesProceedings of the ACM on Programming Languages10.1145/36329188:POPL(2288-2317)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632918
Chen RSander I(2024)A Quantitative Type Approach to Formal Component-Based System Design2024 Forum on Specification & Design Languages (FDL)10.1109/FDL63219.2024.10673844(1-10)Online publication date: 4-Sep-2024
https://doi.org/10.1109/FDL63219.2024.10673844
Marshall DOrchard D(2024)Non-Linear Communication via Graded Modal Session TypesInformation and Computation10.1016/j.ic.2024.105234(105234)Online publication date: Nov-2024
https://doi.org/10.1016/j.ic.2024.105234
Hughes JOrchard D(2024)Program Synthesis from Graded TypesProgramming Languages and Systems10.1007/978-3-031-57262-3_4(83-112)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_4
Bianchini RDagnino FGiannini PZucca E(2023)Resource-Aware Soundness for Big-Step SemanticsProceedings of the ACM on Programming Languages10.1145/36228437:OOPSLA2(1281-1309)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622843
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents