Staged Compilation with Module Functors
Article No.: 260, Pages 693 - 727
Abstract
Multi-stage programming has been used in a wide variety of domains to eliminate the tension between abstraction and performance. However, the interaction of multi-stage programming features with features for programming-in-the-large remains understudied, hindering the full integration of multi-stage programming support into existing languages, and limiting the effective use of staging in large programs. We take steps to remedy the situation by studying the extension of MacoCaml, a recent OCaml extension that supports compile-time code generation via macros and quotations, with module functors, the key mechanism in OCaml for assembling program components into larger units. We discuss design choices related to evaluation order, formalize our calculus via elaboration, and show that the design enjoys key metatheoretical properties: syntactic type soundness, elaboration soundness, and phase distinction. We believe that this study lays a foundation for the continued exploration and implementation of the OCaml macro system.
References
[1]
Andrew W. Appel and David B. MacQueen. 1994. Separate Compilation for Standard ML. In Proceedings of the ACM SIGPLAN’94 Conference on Programming Language Design and Implementation (PLDI), Orlando, Florida, USA, June 20-24, 1994, Vivek Sarkar, Barbara G. Ryder, and Mary Lou Soffa (Eds.). ACM, 13–23. https://doi.org/10.1145/178243.178245
[2]
Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy. 2003. Implementing multi-stage languages using ASTs, gensym, and reflection. In International Conference on Generative Programming and Component Engineering. 57–76.
[3]
Jacques Carette, Mustafa Elsheikh, and W. Spencer Smith. 2011. A generative geometric kernel. In Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2011, Austin, TX, USA, January 24-25, 2011, Siau-Cheng Khoo and Jeremy G. Siek (Eds.). ACM, 53–62. https://doi.org/10.1145/1929501.1929510
[4]
Jacques Carette and Oleg Kiselyov. 2005. Multi-stage Programming with Functors and Monads: Eliminating Abstraction Overhead from Generic Code. In Generative Programming and Component Engineering, 4th International Conference, GPCE 2005, Tallinn, Estonia, September 29 - October 1, 2005, Proceedings, Robert Glück and Michael R. Lowry (Eds.) (Lecture Notes in Computer Science, Vol. 3676). Springer, 256–274. https://doi.org/10.1007/11561347_18
[5]
Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. 2009. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. J. Funct. Program., 19, 5 (2009), 509–543. https://doi.org/10.1017/S0956796809007205
[6]
Karl Crary, Robert Harper, and Sidd Puri. 1999. What is a Recursive Module? In Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, May 1-4, 1999, Barbara G. Ryder and Benjamin G. Zorn (Eds.). ACM, 50–63. https://doi.org/10.1145/301618.301641
[7]
Rowan Davies. 1996. A Temporal-Logic Approach to Binding-Time Analysis. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. IEEE Computer Society, 184–195. https://doi.org/10.1109/LICS.1996.561317
[8]
Rowan Davies and Frank Pfenning. 1996. A Modal Analysis of Staged Computation. In Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, Hans-Juergen Boehm and Guy L. Steele Jr. (Eds.). ACM Press, 258–270. https://doi.org/10.1145/237721.237788
[9]
Daniel de Rauglaudre. 2007. Camlp5 - Reference Manual.
[10]
Derek R. Dreyer, Robert Harper, and Karl Crary. 2001. Toward a Practical Type Theory for Recursive Modules. School of Computer Science, Carnegie Mellon University.
[11]
Martin Elsman. 1999. Static Interpretation of Modules. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, September 27-29, 1999, Didier Rémy and Peter Lee (Eds.). ACM, 208–219. https://doi.org/10.1145/317636.317800
[12]
Matthew Flatt. 2002. Composable and Compilable Macros: You Want It When? In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02). Association for Computing Machinery, New York, NY, USA. 72–83. isbn:1581134878 https://doi.org/10.1145/581478.581486
[13]
Steven E. Ganz, Amr Sabry, and Walid Taha. 2001. Macros as Multi-Stage Computations: Type-Safe, Generative, Binding Macros in MacroML. In Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP ’01), Firenze (Florence), Italy, September 3-5, 2001, Benjamin C. Pierce (Ed.). ACM, 74–85. https://doi.org/10.1145/507635.507646
[14]
Robert Harper, John C Mitchell, and Eugenio Moggi. 1989. Higher-order modules and the phase distinction. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 341–354.
[15]
Robert Harper and Christopher A. Stone. 2000. A type-theoretic interpretation of standard ML. In Proof, Language, and Interaction, Essays in Honour of Robin Milner, Gordon D. Plotkin, Colin Stirling, and Mads Tofte (Eds.). The MIT Press, 341–388.
[16]
Jun Inoue, Oleg Kiselyov, and Yukiyoshi Kameyama. 2016. Staging beyond Terms: Prospects and Challenges. In Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM ’16). Association for Computing Machinery, New York, NY, USA. 103–108. isbn:9781450340977 https://doi.org/10.1145/2847538.2847548
[17]
Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka. 2022. Mœ bius: metaprogramming using contextual types: the stage where system f can pattern match on itself. Proc. ACM Program. Lang., 6, POPL (2022), 1–27. https://doi.org/10.1145/3498700
[18]
Oleg Kiselyov. 2014. The Design and Implementation of BER MetaOCaml. In Functional and Logic Programming, Michael Codish and Eijiro Sumii (Eds.). Springer International Publishing, Cham. 86–102. isbn:978-3-319-07151-0 https://doi.org/10.1007/978-3-319-07151-0_6
[19]
András Kovács. 2022. Staged compilation with two-level type theory. Proc. ACM Program. Lang., 6, ICFP (2022), 540–569. https://doi.org/10.1145/3547641
[20]
Xavier Leroy. 1994. Manifest types, modules, and separate compilation. In Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 109–122.
[21]
John C. Mitchell and Robert Harper. 1988. The Essence of ML. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, Jeanne Ferrante and Peter Mager (Eds.). ACM Press, 28–46. https://doi.org/10.1145/73560.73563
[22]
Yuito Murase, Yuichi Nishiwaki, and Atsushi Igarashi. 2023. Contextual Modal Type Theory with Polymorphic Contexts. In Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Thomas Wies (Ed.) (Lecture Notes in Computer Science, Vol. 13990). Springer, 281–308. https://doi.org/10.1007/978-3-031-30044-8_11
[23]
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. ACM Trans. Comput. Log., 9, 3 (2008), 23:1–23:49. https://doi.org/10.1145/1352582.1352591
[24]
Gabriel Radanne, Thomas Gazagnaire, Anil Madhavapeddy, Jeremy Yallop, Richard Mortier, Hannes Mehnert, Mindy Preston, and David J. Scott. 2019. Programming Unikernels in the Large via Functor Driven Development. CoRR, abs/1905.02529 (2019), arXiv:1905.02529. arxiv:1905.02529
[25]
Tiark Rompf and Martin Odersky. 2010. Lightweight Modular Staging: A Pragmatic Approach to Runtime Code Generation and Compiled DSLs. In Proceedings of the Ninth International Conference on Generative Programming and Component Engineering (GPCE ’10). ACM, New York, NY, USA. 127–136. isbn:978-1-4503-0154-1 https://doi.org/10.1145/1868294.1868314
[26]
Andreas Rossberg. 2018. 1ML - Core and modules united. J. Funct. Program., 28 (2018), e22. https://doi.org/10.1017/S0956796818000205
[27]
Andreas Rossberg, Claudio V. Russo, and Derek Dreyer. 2014. F-ing modules. J. Funct. Program., 24, 5 (2014), 529–607. https://doi.org/10.1017/S0956796814000264
[28]
Yuhi Sato and Yukiyoshi Kameyama. 2021. Type-Safe Generation of Modules in Applicative and Generative Styles. In Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE 2021). Association for Computing Machinery, New York, NY, USA. 184–196. isbn:9781450391122 https://doi.org/10.1145/3486609.3487209
[29]
Yuhi Sato, Yukiyoshi Kameyama, and Takahisa Watanabe. 2020. Module Generation without Regret. In Proceedings of the 2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2020). Association for Computing Machinery, New York, NY, USA. 1–13. isbn:9781450370967 https://doi.org/10.1145/3372884.3373160
[30]
Zhong Shao. 1997. An Overview of the FLINT/ML Compiler. Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC’97), Amsterdam, The Netherlands.
[31]
Zhong Shao. 1999. Transparent Modules with Fully Syntactic Signatures. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, September 27-29, 1999, Didier Rémy and Peter Lee (Eds.). ACM, 220–232. https://doi.org/10.1145/317636.317801
[32]
Tim Sheard and Simon Peyton Jones. 2002. Template Meta-Programming for Haskell. In Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell (Haskell ’02). Association for Computing Machinery, New York, NY, USA. 1–16. isbn:1581136056 https://doi.org/10.1145/581690.581691
[33]
Nicolas Stucki, Aggelos Biboudis, and Martin Odersky. 2018. A practical unification of multi-stage programming and macros. In Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2018, Boston, MA, USA, November 5-6, 2018, Eric Van Wyk and Tiark Rompf (Eds.). ACM, 14–27. https://doi.org/10.1145/3278122.3278139
[34]
Takashi Suwa and Atsushi Igarashi. 2024. An ML-Style Module System for Cross-Stage Type Abstraction in Multi-stage Programming. In Functional and Logic Programming - 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15-17, 2024, Proceedings, Jeremy Gibbons and Dale Miller (Eds.) (Lecture Notes in Computer Science, Vol. 14659). Springer, 237–272. https://doi.org/10.1007/978-981-97-2300-3_13
[35]
Kenichi Suzuki, Oleg Kiselyov, and Yukiyoshi Kameyama. 2016. Finally, safely-extensible and efficient language-integrated query. In Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Martin Erwig and Tiark Rompf (Eds.). ACM, 37–48. https://doi.org/10.1145/2847538.2847542
[36]
Don Syme. 2006. Leveraging. NET meta-programming components from F# integrated queries and interoperable heterogeneous execution. In Proceedings of the 2006 workshop on ML. 43–54.
[37]
Walid Taha. 1999. Multi-Stage Programming: Its Theory and Applications. Ph. D. Dissertation. Halmstad University, Sweden. https://urn.kb.se/resolve?urn=urn:nbn:se:hh:diva-15052
[38]
Walid Taha, Zine-El-Abidine Benaissa, and Tim Sheard. 1998. Multi-stage programming: Axiomatization and type safety. In International Colloquium on Automata, Languages, and Programming. 918–929.
[39]
Walid Taha and Patricia Johann. 2003. Staged Notational Definitions. In Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings, Frank Pfenning and Yannis Smaragdakis (Eds.) (Lecture Notes in Computer Science, Vol. 2830). Springer, 97–116. https://doi.org/10.1007/978-3-540-39815-8_6
[40]
Peter Thiemann. 1999. Interpreting Specialization in Type Theory. In Proceedings of the 1999 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, San Antonio, Texas, USA, January 22-23, 1999. Technical report BRICS-NS-99-1, Olivier Danvy (Ed.). University of Aarhus, 30–43.
[41]
Ryo Tokuda and Yukiyoshi Kameyama. 2023. Generating Programs for Polynomial Multiplication with Correctness Assurance. In Proceedings of the 2023 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, PEPM 2023, Boston, MA, USA, January 16-17, 2023, Edwin C. Brady and Jens Palsberg (Eds.). ACM, 27–40. https://doi.org/10.1145/3571786.3573017
[42]
Takahisa Watanabe and Yukiyoshi Kameyama. 2018. Program generation for ML modules (short paper). In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Los Angeles, CA, USA, January 8-9, 2018, Fritz Henglein and Hsiang-Shang Ko (Eds.). ACM, 60–66. https://doi.org/10.1145/3162072
[43]
Stephen Weeks. 2006. Whole-program compilation in MLton. In Proceedings of the 2006 Workshop on ML (ML ’06). Association for Computing Machinery, New York, NY, USA. 1. isbn:1595934839 https://doi.org/10.1145/1159876.1159877
[44]
Stefan Wehr and Manuel M. T. Chakravarty. 2008. ML Modules and Haskell Type Classes: A Constructive Comparison. In Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008. Proceedings, G. Ramalingam (Ed.) (Lecture Notes in Computer Science, Vol. 5356). Springer, 188–204. https://doi.org/10.1007/978-3-540-89330-1_14
[45]
Leo White. 2013. Extension points for OCaml. OCaml Users and Developers Workshop.
[46]
Leo White, Frédéric Bour, and Jeremy Yallop. 2014. Modular implicits. In Proceedings ML Family/OCaml Users and Developers workshops, ML/OCaml 2014, Gothenburg, Sweden, September 4-5, 2014, Oleg Kiselyov and Jacques Garrigue (Eds.) (EPTCS, Vol. 198). 22–63. https://doi.org/10.4204/EPTCS.198.2
[47]
Andrew K Wright and Matthias Felleisen. 1994. A syntactic approach to type soundness. Information and computation, 115, 1 (1994), 38–94.
[48]
Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang. 2022. Staging with Class: A Specification for Typed Template Haskell. Proc. ACM Program. Lang., 6, POPL (2022), Article 61, jan, 30 pages. https://doi.org/10.1145/3498723
[49]
Ningning Xie, Leo White, Olivier Nicole, and Jeremy Yallop. 2023. MacoCaml: Staging Composable and Compilable Macros. Proc. ACM Program. Lang., 7, ICFP (2023), Article 209, aug, 45 pages. https://doi.org/10.1145/3607851
[50]
Jeremy Yallop. 2017. Staged generic programming. Proc. ACM Program. Lang., 1, ICFP (2017), 29:1–29:29. https://doi.org/10.1145/3110273
[51]
Jeremy Yallop, David Sheets, and Anil Madhavapeddy. 2018. A modular foreign function interface. Sci. Comput. Program., 164 (2018), 82–97. https://doi.org/10.1016/J.SCICO.2017.04.002
[52]
Jeremy Yallop, Tamara von Glehn, and Ohad Kammar. 2018. Partially-static data as free extension of algebras. Proc. ACM Program. Lang., 2, ICFP (2018), 100:1–100:30. https://doi.org/10.1145/3236795
Index Terms
- Staged Compilation with Module Functors
Recommendations
Languages as libraries
PLDI '11Programming language design benefits from constructs for extending the syntax and semantics of a host language. While C's string-based macros empower programmers to introduce notational shorthands, the parser-level macros of Lisp encourage ...
Languages as libraries
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and ImplementationProgramming language design benefits from constructs for extending the syntax and semantics of a host language. While C's string-based macros empower programmers to introduce notational shorthands, the parser-level macros of Lisp encourage ...
MacoCaml: Staging Composable and Compilable Macros
We introduce MacoCaml, a new design and implementation of compile-time code generation for the OCaml language. MacoCaml features a novel combination of macros with phase separation and quotation-based staging, where macros are considered as compile-time ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2024
1031 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 August 2024
Published in PACMPL Volume 8, Issue ICFP
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- Natural Sciences and Engineering Research Council of Canada
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 86Total Downloads
- Downloads (Last 12 months)86
- Downloads (Last 6 weeks)82
Reflects downloads up to 24 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in