Document Open Access Logo

Type Theory as a Language Workbench

Authors Jan de Muijnck-Hughes , Guillaume Allais , Edwin Brady

PDF
Thumbnail PDF

File

OASIcs.EVCS.2023.9.pdf
  • Filesize: 0.62 MB
  • 13 pages

Document Identifiers

Author Details

Jan de Muijnck-Hughes
  • University of Glasgow, UK
Guillaume Allais
  • University of St Andrews, UK
Edwin Brady
  • University of St Andrews, UK

Funding

Jan {de Muijnck-Hughes} is funded by EPSRC grants: Border Patrol (EP/N028201/1) and AppControl (EP/V000462/1). Guillaume Allais and Edwin Brady are funded by EPSRC grant: Programming as Conversation: Type-Driven Development in Action (EP/T007265/1).

Cite As Get BibTex

Jan de Muijnck-Hughes, Guillaume Allais, and Edwin Brady. Type Theory as a Language Workbench. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 9:1-9:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/OASIcs.EVCS.2023.9

Abstract

Language Workbenches offer language designers an expressive environment in which to create their Domain Specific Languages (DSLs). Similarly, research into mechanised meta-theory has shown how dependently typed languages provide expressive environments to formalise and study DSLs and their meta-theoretical properties. But can we claim that dependently typed languages qualify as language workbenches? We argue yes!
We have developed an exemplar DSL called Vélo that showcases not only dependently typed techniques to realise and manipulate  Intermediate Representations (IRs), but that dependently typed languages make fine language workbenches. Vélo is a simple verified language with well-typed holes and comes with a complete compiler pipeline: parser, elaborator, REPL, evaluator, and compiler passes. Specifically, we describe our design choices for well-typed IR design that includes support for well-typed holes, how CSE is achieved in a well-typed setting, and how the mechanised type-soundness proof for Vélo is the source of the evaluator.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Software and its engineering → Software verification
  • Software and its engineering → Functional languages
  • Software and its engineering → Formal language definitions
  • Software and its engineering → Domain specific languages
  • Theory of computation → Lambda calculus
  • Software and its engineering → Compilers
  • Theory of computation → Invariants
Keywords
  • dependent types
  • language workbenches
  • idris2
  • dsl
  • edsl
  • intrinsically scoped
  • well typed
  • co-De Bruijn

Metrics

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

Supplementary Materials

References

  1. Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark. POPLMark reloaded: Mechanizing proofs by logical relations. J. Funct. Program., 29:e19, 2019. URL: https://doi.org/10.1017/S0956796819000170.
  2. Guillaume Allais. Builtin types viewed as inductive families. CoRR, abs/2301.02194, 2023. URL: https://doi.org/10.48550/arXiv.2301.02194.
  3. Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program., 31:e22, 2021. URL: https://doi.org/10.1017/S0956796820000076.
  4. Nada Amin and Tiark Rompf. Type soundness proofs with definitional interpreters. SIGPLAN Not., 52(1):666-679, January 2017. URL: https://doi.org/10.1145/3093333.3009866.
  5. 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.
  6. Lennart Augustsson and Magnus Carlsson. An Exercise in Dependent Types: A Well-Typed Interpreter. In Workshop on Dependent Types in Programming, Gothenburg, 1999. Google Scholar
  7. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The PoplMark challenge. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 50-65. Springer, 2005. URL: https://doi.org/10.1007/11541868_4.
  8. Edwin C. Brady. Type-Driven Development with Idris. Manning Publications, 2017. Google Scholar
  9. Edwin C. Brady. Idris 2: Quantitative type theory in practice. In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), volume 194 of LIPIcs, pages 9:1-9:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.9.
  10. James Chapman, Roman Kireev, Chad Nester, and Philip Wadler. System F in Agda, for fun and profit. In Graham Hutton, editor, Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings, volume 11825 of Lecture Notes in Computer Science, pages 255-297. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-33636-3_10.
  11. David R. Christiansen and Edwin C. Brady. Elaborator reflection: extending idris in idris. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 284-297. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951932.
  12. Koen Claessen and John Hughes. Quickcheck: a lightweight tool for random testing of haskell programs. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000, pages 268-279. ACM, 2000. URL: https://doi.org/10.1145/351240.351266.
  13. Nicolaas Govert 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. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  14. Peter Dybjer. Inductive families. Formal Aspects Comput., 6(4):440-465, 1994. URL: https://doi.org/10.1007/BF01211308.
  15. Sebastian Erdweg, Tijs van der Storm, Markus Völter, Meinte Boersma, Remi Bosman, William R. Cook, Albert Gerritsen, Angelo Hulshout, Steven Kelly, Alex Loh, Gabriël D. P. Konat, Pedro J. Molina, Martin Palatnik, Risto Pohjonen, Eugen Schindler, Klemens Schindler, Riccardo Solmi, Vlad A. Vergu, Eelco Visser, Kevin van der Vlist, Guido Wachsmuth, and Jimi van der Woning. The state of the art in language workbenches - conclusions from the language workbench challenge. In Martin Erwig, Richard F. Paige, and Eric Van Wyk, editors, Software Language Engineering - 6th International Conference, SLE 2013, Indianapolis, IN, USA, October 26-28, 2013. Proceedings, volume 8225 of Lecture Notes in Computer Science, pages 197-217. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-02654-1_11.
  16. Paul Hudak. Building domain-specific embedded languages. ACM Computing Surveys (CSUR), 28(4es):196, 1996. Google Scholar
  17. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight java: a minimal core calculus for java and GJ. ACM Trans. Program. Lang. Syst., 23(3):396-450, 2001. URL: https://doi.org/10.1145/503502.503505.
  18. Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce. Generating good generators for inductive relations. Proc. ACM Program. Lang., 2(POPL):45:1-45:30, 2018. URL: https://doi.org/10.1145/3158133.
  19. 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.
  20. Conor McBride. Everybody’s got to be somewhere. In Robert Atkey and Sam Lindley, editors, Proceedings of the 7th Workshop on Mathematically Structured Functional Programming, MSFP@FSCD 2018, Oxford, UK, 8th July 2018, volume 275 of EPTCS, pages 53-69, 2018. URL: https://doi.org/10.4204/EPTCS.275.6.
  21. Ulf Norell. Dependently typed programming in Agda. In Pieter W. M. Koopman, Rinus Plasmeijer, and S. Doaitse Swierstra, editors, Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures, volume 5832 of Lecture Notes in Computer Science, pages 230-266. Springer, 2008. URL: https://doi.org/10.1007/978-3-642-04652-0_5.
  22. Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer. Live functional programming with typed holes. Proc. ACM Program. Lang., 3(POPL):14:1-14:32, 2019. URL: https://doi.org/10.1145/3290327.
  23. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. Programming Language Foundations, volume 2 of Software Foundations. Electronic textbook, 2020. Version 5.8, URL: http://softwarefoundations.cis.upenn.edu.
  24. 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.
  25. Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 166-180. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294101.
  26. The Coq Development Team. The coq proof assistant, January 2022. URL: https://doi.org/10.5281/zenodo.5846982.
  27. Cas van der Rest, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, and Peter Mosses. Intrinsically-typed definitional interpreters à la carte. Proc. ACM Program. Lang., 6(OOPSLA2), October 2022. URL: https://doi.org/10.1145/3563355.
  28. Guido Wachsmuth, Gabriël D. P. Konat, and Eelco Visser. Language design with the spoofax language workbench. IEEE Softw., 31(5):35-43, 2014. URL: https://doi.org/10.1109/MS.2014.100.
  29. Philip Wadler, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda, August 2022. URL: https://plfa.inf.ed.ac.uk/22.08/.
  30. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38-94, 1994. URL: https://doi.org/10.1006/inco.1994.1093.
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