Dominic Orchard
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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.
Supplemental Material
Available for Download
zip
icfp19main-p84-p-aux.zip (1.6 MB)
Appendix
- Samson Abramsky. 1993. Computational interpretations of linear logic. Theoretical computer science 111, 1-2 (1993), 3–57. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Robert Atkey and James Wood. 2018. Context Constrained Computation. In Workshop on Type-Driven Development, colocated with ICFP 2018.Google Scholar
- Andrew Barber and Gordon Plotkin. 1996. Dual intuitionistic linear logic. University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science.Google Scholar
- 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.Google Scholar
- 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 Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Gavin M. Bierman and Valeria CV de Paiva. 2000. On an intuitionistic modal logic. Studia Logica 65, 3 (2000), 383–416.Google ScholarCross Ref
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Iliano Cervesato and Frank Pfenning. 2002. A linear logical framework. Information and Computation 179, 1 (2002), 19–75. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Nils Anders Danielsson. 2008. Lightweight semiformal time complexity analysis for purely functional data structures. In ACM SIGPLAN Notices, Vol. 43. ACM, 133–144. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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 Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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 Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Soichiro Fujii, Shinya Katsumata, and Paul-André Melliès. 2016. Towards a formal theory of graded monads. In FOSSACS. Springer, 513–530.Google Scholar
- 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 Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Simon J. Gay and Vasco Thudichum Vasconcelos. 2010. Linear type theory for asynchronous session types. J. Funct. Program. 20, 1 (2010), 19–50. Google ScholarDigital Library
- Dan R. Ghica and Alex I. Smith. 2014. Bounded linear types in a resource semiring. In Programming Languages and Systems. Springer, 331–350. Google ScholarDigital Library
- Jean-Yves Girard. 1987. Linear logic. Theoretical computer science 50, 1 (1987), 1–101. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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).Google Scholar
- 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. Google ScholarDigital Library
- Simon Peyton Jones. 2003. Haskell 98 language and libraries: the revised report. Cambridge University Press.Google Scholar
- Shin-ya Katsumata. 2014. Parametric effect monads and semantics of effect systems. In Proceedings of POPL 2014. ACM, 633–645. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- Nicholas D Matsakis and Felix S Klock II. 2014. The Rust Language. In ACM SIGAda Ada Letters, Vol. 34. ACM, 103–104. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Conor McBride. 2016. I got Plenty o’ Nuttin’. In A List of Successes That Can Change the World. Springer, 207–233.Google Scholar
- Conor McBride and James McKinna. 2004. The view from the left. Journal of functional programming 14, 1 (2004), 69–111. Google ScholarDigital Library
- 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.Google Scholar
- Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. 1997. The Definition of Standard ML: revised. MIT press. Google ScholarDigital Library
- J Garrett Morris. 2016. The best of both worlds: linear functional programming without compromise. In ACM SIGPLAN Notices, Vol. 51. ACM, 448–461.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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).Google Scholar
- 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.5391Google Scholar
- Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2013. Coeffects: Unified Static Analysis of Context-Dependence. In ICALP (2). 385–397. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Frank Pfenning and Rowan Davies. 2001. A judgmental reconstruction of modal logic. Mathematical structures in computer science 11, 4 (2001), 511–540. Google ScholarDigital Library
- Jeff Polakow. 2015. Embedding a Full Linear Lambda Calculus in Haskell. SIGPLAN Not. 50, 12, 177–188. Google ScholarDigital Library
- Dag Prawitz. 1965. Natural Deduction: A proof-theoretical study. Stockholm Studies in Philosophy. Almqvist & Wiksell, Stockholm 3 (1965).Google Scholar
- A.L. Smirnov. 2008. Graded monads and rings of polynomials. Journal of Mathematical Sciences 151, 3 (2008), 3032–3051.Google ScholarCross Ref
- K. Terui. 2001. Light Affine Lambda Calculus and Polytime Strong Normalization. In LICS ’01. IEEE Computer Society, 209–220.Google Scholar
- Jesse A Tov and Riccardo Pucella. 2010. Stateful contracts for affine types. In European Symposium on Programming. Springer, 550–569. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Philip Wadler. 1990. Linear types can change the world. In IFIP TC, Vol. 2. 347–359.Google Scholar
- Philip Wadler. 1992. There’s no substitute for linear logic. In 8th International Workshop on the Mathematical Foundations of Programming Semantics.Google Scholar
- 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. Google Scholar
- David Walker. 2005. Substructural type systems. Advanced Topics in Types and Programming Languages (2005), 3–44.Google Scholar
- Hongwei Xi. 2003. Applied type system. In International Workshop on Types for Proofs and Programs. Springer, 394–408.Google Scholar
- 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. Google ScholarDigital Library
Index Terms
- Quantitative program reasoning with graded modal types
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 programmingSession 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