Document Open Access Logo

Towards Modular Compilation Using Higher-Order Effects

Author Jaro S. Reinders

PDF
Thumbnail PDF

File

OASIcs.EVCS.2023.22.pdf
  • Filesize: 0.5 MB
  • 9 pages

Document Identifiers

Author Details

Jaro S. Reinders
  • Delft University of Technology, The Netherlands

Cite AsGet BibTex

Jaro S. Reinders. Towards Modular Compilation Using Higher-Order Effects. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 22:1-22:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/OASIcs.EVCS.2023.22

Abstract

Compilers transform a human readable source language into machine readable target language. Nanopass compilers simplify this approach by breaking up this transformation into small steps that are more understandable, maintainable, and extensible. We propose a semantics-driven variant of the nanopass compiler architecture exploring the use a effects and handlers to model the intermediate languages and the transformation passes, respectively. Our approach is fully typed and ensures that all cases in the compiler are covered. Additionally, by using an effect system we abstract over the control flow of the intermediate language making the compiler even more flexible. We apply this approach to a minimal compiler from a language with arithmetic and let-bound variables to a string of pretty printed X86 instructions. In the future, we hope to extend this work to compile a larger and more complicated language and we envision a formal verification framework from compilers written in this style.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
  • Software and its engineering → Compilers
Keywords
  • algebraic effects and handlers
  • higher-order effects
  • monadic semantics
  • modularity
  • compilation
  • nanopass

Metrics

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

Supplementary Materials

References

  1. Casper Bach Poulsen and Cas van der Rest. Hefty algebras: Modular elaboration of higher-order algebraic effects. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571255.
  2. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of agda - a functional language with dependent types. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 73-78, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  3. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. SIGPLAN Not., 43(9):143-156, September 2008. URL: https://doi.org/10.1145/1411203.1411226.
  4. 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. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  5. Lennart C.L. Kats and Eelco Visser. The spoofax language workbench: Rules for declarative specification of languages and ides. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '10, pages 444-463, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1869459.1869497.
  6. Andrew W. Keep and R. Kent Dybvig. A nanopass framework for commercial compiler development. SIGPLAN Not., 48(9):343-350, September 2013. URL: https://doi.org/10.1145/2544174.2500618.
  7. E. Moggi. Computational lambda-calculus and monads. In [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pages 14-23, 1989. URL: https://doi.org/10.1109/LICS.1989.39155.
  8. Thijs Molendijk. Dynamix: A domain-specific language for dynamic semantics. Master’s thesis, Delft University of Technology, 2022. URL: http://resolver.tudelft.nl/uuid:8653ab24-a782-41f0-aefc-6b1c8d9a37d5.
  9. Gordon Plotkin and John Power. Adequacy for algebraic effects. In Furio Honsell and Marino Miculan, editors, Foundations of Software Science and Computation Structures, pages 1-24, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  10. Gordon Plotkin and Matija Pretnar. Handlers of algebraic effects. In Giuseppe Castagna, editor, Programming Languages and Systems, pages 80-94, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  11. Dipanwita Sarkar, Oscar Waddell, and R. Kent Dybvig. A nanopass infrastructure for compiler education. In Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP '04, pages 201-212, New York, NY, USA, 2004. Association for Computing Machinery. URL: https://doi.org/10.1145/1016850.1016878.
  12. Jeff Smits and Eelco Visser. Gradually typing strategies. In Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, pages 1-15, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3426425.3426928.
  13. Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, and Eelco Visser. Scopes as types. Proc. ACM Program. Lang., 2(OOPSLA), October 2018. URL: https://doi.org/10.1145/3276484.
  14. Vlad Vergu, Pierre Neron, and Eelco Visser. DynSem: A DSL for Dynamic Semantics Specification. In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications (RTA 2015), volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 365-378, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.RTA.2015.365.
  15. Vlad Vergu and Eelco Visser. Specializing a meta-interpreter: Jit compilation of dynsem specifications on the graal vm. In Proceedings of the 15th International Conference on Managed Languages & Runtimes, ManLang '18, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3237009.3237018.
  16. Eelco Visser. Stratego: A language for program transformation based on rewriting strategies system description of stratego 0.5. In Aart Middeldorp, editor, Rewriting Techniques and Applications, pages 357-361, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  17. Philip Wadler. Comprehending monads. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming, LFP '90, pages 61-78, New York, NY, USA, 1990. Association for Computing Machinery. URL: https://doi.org/10.1145/91556.91592.
  18. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: Representing recursive and impure programs in coq. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371119.
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