Document Open Access Logo

Idris 2: Quantitative Type Theory in Practice

Author Edwin Brady

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2021.9.pdf
  • Filesize: 0.89 MB
  • 26 pages

Document Identifiers

Author Details

Edwin Brady
  • School of Computer Science, University of St Andrews, Scotland, UK

Funding

This work was funded by EPSRC grant EP/T007265/1.

Acknowledgements

This work has benefitted from the many contributions to the Idris 2 project from the community. I am also grateful to the anonymous referees for their helpful feedback.

Cite As Get BibTex

Edwin Brady. Idris 2: Quantitative Type Theory in Practice. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 9:1-9:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ECOOP.2021.9

Abstract

Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent programming, where the state of a communication channel changes throughout program execution. As yet, however, there has not been a full-scale programming language with which to experiment with these ideas. Idris 2 is a new version of the dependently typed language Idris, with a new core language based on QTT, supporting linear and dependent types. In this paper, we introduce Idris 2, and describe how QTT has influenced its design. We give examples of the benefits of QTT in practice including: expressing which data is erased at run time, at the type level; and, resource tracking in the type system leading to type-safe concurrent programming with session types.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Functional languages
Keywords
  • Dependent types
  • linear types
  • concurrency

Metrics

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

Supplementary Materials

References

  1. J Aldrich, J Sunshine, D Saini, and Z Sparks. Typestate-oriented programming. In Proceedings of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications, pages 1015-1012, 2009. URL: http://dl.acm.org/citation.cfm?id=1640073.
  2. Guillaume Allais, James Chapman, Conor McBride, and James McKinna. Type-and-Scope Safe Programs and their Proofs. In CPP, pages 195-207, 2017. Google Scholar
  3. Robert Atkey. Parameterised notions of computation. Journal of Functional Programming, 19(3-4):335, 2009. URL: https://doi.org/10.1017/S095679680900728X.
  4. Robert Atkey. The syntax and semantics of quantitative type theory. In LICS 2018, 2018. URL: https://doi.org/10.1145/3209108.3209189.
  5. L. Augustsson and M. Carlsson. An exercise in dependent types: A well-typed interpreter. In In Workshop on Dependent Types in Programming, Gothenburg. Citeseer, 1999. URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2895.
  6. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. Linear Haskell: Practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang., 2(POPL):5:1-5:29, December 2017. URL: https://doi.org/10.1145/3158093.
  7. Edwin Brady. Practical Implementation of a Dependently Typed Functional Programming Language. PhD thesis, University of Durham, 2005. Google Scholar
  8. Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23:552-593, September 2013. Google Scholar
  9. Edwin Brady. Resource-dependent algebraic effects. In Jurriaan Hage and Jay McCarthy, editors, Trends in Functional Programming (TFP '14), volume 8843 of LNCS. Springer, 2014. Google Scholar
  10. 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.
  11. Edwin Brady. Type-driven development of concurrent communicating systems. Computer Science, 18(3), 2017. Google Scholar
  12. Edwin Brady, Conor McBride, and James McKinna. Inductive families need not store their indices. In Types for Proofs and Programs (TYPES 2003), volume 3085 of Lecture Notes in Computer Science, pages 115-129. Springer, 2003. Google Scholar
  13. Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie C. Weirich. A graded dependent type system with a usage-aware semantics (extended version). In arXiv:2011.04070 [cs], January 2021. arXiv: 2011.04070. URL: http://arxiv.org/abs/2011.04070.
  14. Nils Anders Danielsson. Total parser combinators. In International Conference on Functional Programming (ICFP 2010), 2010. URL: https://doi.org/10.1145/1932681.1863585.
  15. 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.
  16. Edsko de Vries, Rinus Plasmeijer, and David M Abrahamson. Uniqueness Typing Simplified. In Implementation and Application of Functional Languages, pages 201 - -218, 2008. Google Scholar
  17. Robert Ennals, Richard Sharp, and Alan Mycroft. Linear types for packet processing. In David Schmidt, editor, Programming Languages and Systems, pages 204-218, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  18. Simon Fowler, Sam Lindley, J Garrett Morris, and Sara Decova. Exceptional Asynchronous Session Types: Session Types without Tiers. In Principles of Programming Languages (POPL 2019), 2019. Google Scholar
  19. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '13, page 357, 2013. URL: https://doi.org/10.1145/2429069.2429113.
  20. Adam Gundry. Type Inference, Haskell and Dependent Types. PhD Thesis, University of Strathclyde, 2013. URL: https://personal.cis.strath.ac.uk/adam.gundry/thesis/thesis-2013-07-24.pdf.
  21. Kohei Honda. Types for dyadic interaction. In CONCUR 1993 (International Conference on Concurrency Theory). Springer, 1993. Google Scholar
  22. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Principles of Programming Languages (POPL 2008), 2008. Google Scholar
  23. Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. Session Types for Rust. In WGP 2015 (Workshop on Generic Programming). ACM, 2015. Google Scholar
  24. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Rustbelt: Securing the foundations of the rust programming language. Proc. ACM Program. Lang., 2(POPL), 2017. URL: https://doi.org/10.1145/3158154.
  25. András Kovács. Fast elaboration for dependent type theories, 2019. Talk at EU Types WG Meeting. Google Scholar
  26. Neelakantan R Krishnaswami, Pierre Pradic, and Nick Benton. Integrating Dependent and Linear Types. In Principles of Programming Languages (POPL 2015), 2015. Google Scholar
  27. Conor McBride. Kleisli arrows of outrageous fortune, 2011. Google Scholar
  28. Conor McBride. How to Keep Your Neighbours in Order. In International Conference on Functional Programming (ICFP 2014), 2014. Google Scholar
  29. Conor McBride. I got plenty o' nuttin'. In A List of Successes that Can Change the World, 2016. Google Scholar
  30. Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 1992. URL: http://www.sciencedirect.com/science/article/pii/074771719290011R.
  31. Nathan Mishra-Linger and Tim Sheard. Erasure and polymorphism in pure type systems. In Roberto M. Amadio, editor, Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, volume 4962 of Lecture Notes in Computer Science, pages 350-364. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_25.
  32. Benjamin Moon, Harley Eades III, and Dominic Orchard. Graded Modal Dependent Type Theory. In ESOP 2021, 2020. arXiv: 2010.13163. URL: http://arxiv.org/abs/2010.13163.
  33. J Garrett Morris. The Best of Both Worlds: Linear Functional Programming Without Compromise. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming - ICFP 2016, pages 448-461, 2016. URL: https://doi.org/10.1145/2951913.2951925.
  34. Aleksander Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: Dependent types for imperative programs. In International Conference on Functional Programming (ICFP 2008), pages 229 - -240, 2008. URL: https://doi.org/10.1145/1411204.1411237.
  35. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007. URL: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf.
  36. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang., 3(ICFP), 2019. URL: https://doi.org/10.1145/3341714.
  37. Simon Peyton Jones. Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In Engineering theories of software construction, Marktoberdorf Summer School, pages 47 - -96, 2001. Google Scholar
  38. Nadia Polikarpova, Ivan Kuraj, and Armando Solar-lezama. Program Synthesis from Polymorphic Refinement Types. PLDI, 2016. ISBN: 9781450342612. Google Scholar
  39. A. H. Robinson and C. Cherry. Results of a prototype television bandwidth compression scheme. Proceedings of the IEEE, 55(3):356-364, 1967. URL: https://doi.org/10.1109/PROC.1967.5493.
  40. Rui Shi and Hongwei Xi. A linear type system for multicore programming in ATS. Science of Computer Programming, 78(8):1176-1192, 2013. URL: https://doi.org/10.1016/j.scico.2012.09.005.
  41. Matúš Tejiščák. A dependently typed calculus with pattern matching and erasure inference. Proc. ACM Program. Lang., 4(ICFP):91:1-91:29, 2020. URL: https://doi.org/10.1145/3408973.
  42. Matúš Tejiščák. Erasure in Dependently Typed Programming. PhD thesis, University of St Andrews, 2020. Google Scholar
  43. Peter Thiemann and Vasco T. Vasconcelos. Label-dependent session types. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371135.
  44. Jesse a. Tov and Riccardo Pucella. Practical affine types. In Principles of Programming Languages, pages 447 - -458, 2011. URL: https://doi.org/10.1145/1925844.1926436.
  45. Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, pages 347-359. North Holland, 1990. Google Scholar
  46. Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg. A role for dependent types in Haskell. Proc. ACM Program. Lang., 3(ICFP):101:1-101:29, 2019. URL: https://doi.org/10.1145/3341705.
  47. Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and Richard A. Eisenberg. A specification for dependent types in Haskell. Proc. ACM Program. Lang., 1(ICFP):31:1-31:29, 2017. URL: https://doi.org/10.1145/3110275.
  48. Roger Wolff, Jonathan Aldrich, Ronald Garcia, Roger Wolff, and Jonathan Aldrich. Foundations of Typestate-Oriented Programming. Transactions on Programming Languages and Systems, 36(4):1-44, 2014. Google Scholar
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 About DROPS Imprint Privacy Contact