Document Open Access Logo

A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Pearl)

Authors Jan de Muijnck-Hughes , Edwin Brady , Wim Vanderbauwhede

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.20.pdf
  • Filesize: 0.57 MB
  • 31 pages

Document Identifiers

Author Details

Jan de Muijnck-Hughes
  • University of Glasgow, United Kingdom
Edwin Brady
  • University of St Andrews, United Kingdom
Wim Vanderbauwhede
  • University of Glasgow, United Kingdom

Funding

This work was funded by EPSRC projects: Border Patrol: Improving Smart Device Security through Type-Aware Systems Design (http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/N028201/1); and Type-Driven Verification of Communicating Systems - http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/N024222/1.

Acknowledgements

The authors would like to thank the anonymous reviewers for their excellent reviews that served to better the work.

Cite AsGet BibTex

Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede. A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Pearl). In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 20:1-20:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.20

Abstract

Idris' Effects library demonstrates how to embed resource dependent algebraic effect handlers into a dependently typed host language, providing run-time and compile-time based reasoning on type-level resources. Building upon this work, Resources is a framework for realising Embedded Domain Specific Languages (EDSLs) with type systems that contain domain specific substructural properties. Differing from Effects, Resources allows a language’s substructural properties to be encoded within type-level resources that are associated with language variables. Such an association allows for multiple effect instances to be reasoned about autonomically and without explicit type-level declaration. Type-level predicates are used as proof that the language’s substructural properties hold. Several exemplar EDSLs are presented that illustrates our framework’s operation and how dependent types provide correctness-by-construction guarantees that substructural properties of written programs hold.

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
  • Software and its engineering → Language features
  • Software and its engineering → Domain specific languages
  • Software and its engineering → System modeling languages
Keywords
  • Dependent Types
  • Algebraic Effect Handlers
  • Domain-Specific Languages
  • Embedded Domain Specific Languages
  • Idris
  • Substructural Type-Systems

Metrics

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

Supplementary Materials

References

  1. Robert Atkey. Parameterised notions of computation. J. Funct. Program., 19(3-4):335-376, 2009. URL: https://doi.org/10.1017/S095679680900728X.
  2. Robert Atkey. Syntax and semantics of quantitative type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 56-65. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209189.
  3. Lennart Augustsson and Magnus Carlsson. An Exercise in Dependent Types: A Well-Typed Interpreter. In In Workshop on Dependent Types in Programming, Gothenburg, 1999. Google Scholar
  4. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. Linear haskell: practical linearity in a higher-order polymorphic language. PACMPL, 2(POPL):5:1-5:29, 2018. URL: https://doi.org/10.1145/3158093.
  5. Kevin Bierhoff and Jonathan Aldrich. Modular typestate checking of aliased objects. In Richard P. Gabriel, David F. Bacon, Cristina Videira Lopes, and Guy L. Steele Jr., editors, Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada, pages 301-320. ACM, 2007. URL: https://doi.org/10.1145/1297027.1297050.
  6. Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. A theory of design-by-contract for distributed multiparty interactions. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, pages 162-176, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_12.
  7. Johannes Borgström, Juan Chen, and Nikhil Swamy. Verifying stateful programs with substructural state and hoare types. In Ranjit Jhala and Wouter Swierstra, editors, Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011, pages 15-26. ACM, 2011. URL: https://doi.org/10.1145/1929529.1929532.
  8. Johannes Borgström, Andrew D. Gordon, and Riccardo Pucella. Roles, stacks, histories: A triple for hoare. J. Funct. Program., 21(2):159-207, 2011. URL: https://doi.org/10.1017/S0956796810000134.
  9. Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program., 23(5):552-593, 2013. URL: https://doi.org/10.1017/S095679681300018X.
  10. Edwin Brady. Programming and reasoning with algebraic effects and dependent types. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 133-144. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500581.
  11. Edwin Brady. Resource-dependent algebraic effects. In Jurriaan Hage and Jay McCarthy, editors, Trends in Functional Programming - 15th International Symposium, TFP 2014, Soesterberg, The Netherlands, May 26-28, 2014. Revised Selected Papers, volume 8843 of Lecture Notes in Computer Science, pages 18-33. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-14675-1_2.
  12. Edwin Brady. State Machines All The Way Down: An Architecture for Dependently Typed Applications. Unpublished Draft., 2016. Google Scholar
  13. Edwin Brady. Type-Driven Devlopment with Idris. Manning, 1st edition, 2016. Google Scholar
  14. Edwin Brady. Type-driven development of concurrent communicating systems. Computer Science (AGH), 18(3), 2017. URL: https://doi.org/10.7494/csci.2017.18.3.1413.
  15. Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. Affine refinement types for secure distributed programming. ACM Trans. Program. Lang. Syst., 37(4):11:1-11:66, 2015. URL: https://doi.org/10.1145/2743018.
  16. Luís Caires and João Costa Seco. The type discipline of behavioral separation. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 275-286. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429103.
  17. Elias Castegren and Tobias Wrigstad. Reference capabilities for concurrency control. In Shriram Krishnamurthi and Benjamin S. Lerner, editors, 30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy, volume 56 of LIPIcs, pages 5:1-5:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.5.
  18. N.G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. Google Scholar
  19. Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede. Value-dependent session design in a dependently typed language. In Francisco Martins and Dominic Orchard, editors, Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES@ETAPS 2019, Prague, Czech Republic, 7th April 2019, volume 291 of EPTCS, pages 47-59, 2019. URL: https://doi.org/10.4204/EPTCS.291.5.
  20. Jan de Muijnck-Hughes and Wim Vanderbauwhede. A typing discipline for hardware interfaces. In Alastair F. Donaldson, editor, 33rd European Conference on Object-Oriented Programming, ECOOP 2019, July 15-19, 2019, London, United Kingdom, volume 134 of LIPIcs, pages 6:1-6:27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2019.6.
  21. Edsko de Vries, Rinus Plasmeijer, and David M. Abrahamson. Uniqueness typing simplified. In Olaf Chitil, Zoltán Horváth, and Viktória Zsók, editors, Implementation and Application of Functional Languages, 19th International Workshop, IFL 2007, Freiburg, Germany, September 27-29, 2007. Revised Selected Papers, volume 5083 of Lecture Notes in Computer Science, pages 201-218. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-85373-2_12.
  22. Robert DeLine and Manuel Fähndrich. Typestates for objects. In Martin Odersky, editor, ECOOP 2004 - Object-Oriented Programming, 18th European Conference, Oslo, Norway, June 14-18, 2004, Proceedings, volume 3086 of Lecture Notes in Computer Science, pages 465-490. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24851-4_21.
  23. Ewen Denney. Refinement types for specification. In David Gries and Willem P. de Roever, editors, Programming Concepts and Methods, IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET '98) 8-12 June 1998, Shelter Island, New York, USA, volume 125 of IFIP Conference Proceedings, pages 148-166. Chapman & Hall, 1998. Google Scholar
  24. Richard A. Eisenberg. Dependent types in haskell: Theory and practice. CoRR, abs/1610.07978, 2016. URL: http://arxiv.org/abs/1610.07978.
  25. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay A. McCarthy, and Sam Tobin-Hochstadt. A programmable programming language. Commun. ACM, 61(3):62-71, 2018. URL: https://doi.org/10.1145/3127323.
  26. Martin Fowler. Domain-Specific Languages. Addison-Wesley Signature Series. Addison-Wesley Professional, 1 edition, October 2010. Google Scholar
  27. Timothy S. Freeman and Frank Pfenning. Refinement types for ML. In David S. Wise, editor, Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, pages 268-277. ACM, 1991. URL: https://doi.org/10.1145/113445.113468.
  28. Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. Uniqueness and reference immutability for safe parallelism. In Gary T. Leavens and Matthew B. Dwyer, editors, Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012, pages 21-40. ACM, 2012. URL: https://doi.org/10.1145/2384616.2384619.
  29. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, 1969. URL: https://doi.org/10.1145/363235.363259.
  30. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  31. Raymond Hu and Nobuko Yoshida. Explicit connection actions in multiparty session types. In Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, pages 116-133, 2017. URL: https://doi.org/10.1007/978-3-662-54494-5_7.
  32. Wei Huang, Werner Dietl, Ana Milanova, and Michael D. Ernst. Inference and checking of object ownership. In James Noble, editor, ECOOP 2012 - Object-Oriented Programming - 26th European Conference, Beijing, China, June 11-16, 2012. Proceedings, volume 7313 of Lecture Notes in Computer Science, pages 181-206. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31057-7_9.
  33. Ohad Kammar, Sam Lindley, and Nicolas Oury. Handlers in action. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 145-158. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500590.
  34. Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, and Deepak Garg. Superficially substructural types. In Peter Thiemann and Robby Bruce Findler, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pages 41-54. ACM, 2012. URL: https://doi.org/10.1145/2364527.2364536.
  35. Amit A. Levy, Michael P. Andersen, Bradford Campbell, David E. Culler, Prabal Dutta, Branden Ghena, Philip Levis, and Pat Pannuto. Ownership is theft: experiences building an embedded OS in rust. In Shan Lu, editor, Proceedings of the 8th Workshop on Programming Languages and Operating Systems, PLOS 2015, Monterey, California, USA, October 4, 2015, pages 21-26. ACM, 2015. URL: https://doi.org/10.1145/2818302.2818306.
  36. Nicholas D. Matsakis and Felix S. Klock II. The rust language. In Michael Feldman and S. Tucker Taft, editors, Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, HILT 2014, Portland, Oregon, USA, October 18-21, 2014, pages 103-104. ACM, 2014. URL: https://doi.org/10.1145/2663171.2663188.
  37. Conor McBride. I got plenty o' nuttin'. In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella, editors, A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pages 207-233. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_12.
  38. Conor McBride and James McKinna. The view from the left. J. Funct. Program., 14(1):69-111, 2004. URL: https://doi.org/10.1017/S0956796803004829.
  39. Filipe Militão, Jonathan Aldrich, and Luís Caires. Substructural typestates. In Nils Anders Danielsson and Bart Jacobs, editors, Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, PLPV 2014, January 21, 2014, San Diego, California, USA, Co-located with POPL '14, pages 15-26. ACM, 2014. URL: https://doi.org/10.1145/2541568.2541574.
  40. Robin Milner. The Space and Motion of Communicating Agents. Cambridge University Press, 2009. Google Scholar
  41. Andrey Mokhov. Algebraic graphs with class (functional pearl). In Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, Oxford, United Kingdom, September 7-8, 2017, pages 2-13, 2017. URL: https://doi.org/10.1145/3122955.3122956.
  42. Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: dependent types for imperative programs. In Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pages 229-240, 2008. URL: https://doi.org/10.1145/1411204.1411237.
  43. Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. J. Funct. Program., 18(5-6):865-911, 2008. URL: https://doi.org/10.1017/S0956796808006953.
  44. Ulf Norell. Dependently typed programming in agda. In Andrew Kennedy and Amal Ahmed, editors, Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, pages 1-2. ACM, 2009. URL: https://doi.org/10.1145/1481861.1481862.
  45. Peter W. O'Hearn. Separation logic. Commun. ACM, 62(2):86-95, 2019. URL: https://doi.org/10.1145/3211968.
  46. Dominic A. Orchard and Tomas Petricek. Embedding effect systems in haskell. In Wouter Swierstra, editor, Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014, pages 13-24. ACM, 2014. URL: https://doi.org/10.1145/2633357.2633368.
  47. Johan Östlund and Tobias Wrigstad. Multiple aggregate entry points for ownership types. In James Noble, editor, ECOOP 2012 - Object-Oriented Programming - 26th European Conference, Beijing, China, June 11-16, 2012. Proceedings, volume 7313 of Lecture Notes in Computer Science, pages 156-180. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31057-7_8.
  48. Jennifer Paykin. Linear/non-Linear Types for Embedded Domain-Specific Languages. PhD thesis, University of Pennsylvania, 2018. Publicly Accessible Penn Dissertations. 2752. URL: https://repository.upenn.edu/edissertations/2752.
  49. Jennifer Paykin and Steve Zdancewic. The linearity monad. In Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, Oxford, United Kingdom, September 7-8, 2017, pages 117-132, 2017. URL: https://doi.org/10.1145/3122955.3122965.
  50. Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic effects. In Giuseppe Castagna, editor, Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5502 of Lecture Notes in Computer Science, pages 80-94. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_7.
  51. Jon Postel. Transmission control protocol. RFC, 793:1-91, 1981. URL: https://doi.org/10.17487/RFC0793.
  52. Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. Intrinsically-typed definitional interpreters for linear, session-typed languages. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 284-298. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373818.
  53. Michele Sevegnani and Muffy Calder. Bigrapher: Rewriting and analysis engine for bigraphs. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, pages 494-501, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_27.
  54. Michele Sevegnani, Milan Kabác, Muffy Calder, and Julie A. McCann. Modelling and verification of large-scale sensor network infrastructures. In 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018, pages 71-81, 2018. URL: https://doi.org/10.1109/ICECCS2018.2018.00016.
  55. Rui Shi and Hongwei Xi. A linear type system for multicore programming in ATS. Sci. Comput. Program., 78(8):1176-1192, 2013. URL: https://doi.org/10.1016/j.scico.2012.09.005.
  56. Robert E. Strom. Mechanisms for compile-time enforcement of security. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983, pages 276-284, 1983. URL: https://doi.org/10.1145/567067.567093.
  57. Nikhil Swamy, Juan Chen, and Ravi Chugh. Enforcing stateful authorization and information flow policies in fine. In Andrew D. Gordon, editor, Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6012 of Lecture Notes in Computer Science, pages 529-549. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-11957-6_28.
  58. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. Secure distributed programming with value-dependent types. J. Funct. Program., 23(4):402-451, 2013. URL: https://doi.org/10.1017/S0956796813000142.
  59. Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. Verifying higher-order programs with the dijkstra monad. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pages 387-398, 2013. URL: https://doi.org/10.1145/2491956.2491978.
  60. Wouter Swierstra. A hoare logic for the state monad. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pages 440-451, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_30.
  61. Bernardo Toninho and Nobuko Yoshida. Certifying data in multiparty session types. J. Log. Algebraic Methods Program., 90:61-83, 2017. URL: https://doi.org/10.1016/j.jlamp.2016.11.005.
  62. Jesse A. Tov and Riccardo Pucella. Practical affine types. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 447-458, 2011. URL: https://doi.org/10.1145/1926385.1926436.
  63. Philip Wadler. Linear types can change the world! In Manfred Broy, editor, Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990, page 561. North-Holland, 1990. Google Scholar
  64. Philip Wadler. Is there a use for linear logic? In Charles Consel and Olivier Danvy, editors, Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'91, Yale University, New Haven, Connecticut, USA, June 17-19, 1991, pages 255-273. ACM, 1991. URL: https://doi.org/10.1145/115865.115894.
  65. David Walker. Advanced Topic in Types and Programming Languages, chapter Substructural Type Systems, pages 3-43. The MIT Press, 2004. Google Scholar
  66. Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and Richard A. Eisenberg. A specification for dependent types in haskell. PACMPL, 1(ICFP):31:1-31:29, 2017. URL: https://doi.org/10.1145/3110275.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact