Universal programming languages are an old dream. There is the computability sense of Turing-universal; Landin and others have advocated syntactically universal languages, a path leading to extensible syntax, e.g., macros. A stronger kind of universality would reduce the need for domain-specific languages—they could be replaced by ‘active libraries’ providing and safety requirements. Experience suggests that much domain-specific optimization can be realized by staging, i.e., doing computations at compile time to produce an efficient run-time. Rudimentary computability arguments show that languages with a ‘Turing-complete kernel’ can be both stage-universal and safety-universal. But making this approach practical requires compilers that find optimal programs, and this is a hard problem. Guaranteed Optimization is a proof technique for constructing compilers that find optimal programs within a decidable approximation of program equivalence. This gives us compilers whose kernels possess intuitive closure properties akin to, but stronger than, languages with explicit staging, and can meet the ‘Turing-complete kernel’ requirement to be stage- and safety-universal. To show this technique is practical we demonstrate a prototype compiler that finds optimal programs in the presence of heap operations; the proof of this is tedious but automated. The proof ensures that any code ‘lying in the kernel’ is evaluated and erased at compile-time. This opens several interesting directions for active libraries. One is staging: we can synthesize fast implementation code at compile-time by putting code-generators in the kernel. To achieve domain-specific safety checking we propose ‘proof embeddings’ in which proofs are intermingled with code and the optimizer does double-duty as a theorem prover. Proofs lying in the kernel are checked and erased at compile-time, yielding code that is both fast and safe.
Cited By
- Lifflander J and Krishnamoorthy S (2017). Cache locality optimization for recursive programs, ACM SIGPLAN Notices, 52:6, (1-16), Online publication date: 14-Sep-2017.
- Mathuriya A, Luo Y, Clay R, Benali A, Shulenburger L and Kim J Embracing a new era of highly efficient and productive quantum Monte Carlo simulations Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, (1-12)
- Lifflander J and Krishnamoorthy S Cache locality optimization for recursive programs Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, (1-16)
- Yallop J Staging generic programming Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, (85-96)
- Teodorescu L, Dumitrel V and Potolea R Moving computations from run-time to compile-time Proceedings of the 11th ACM Conference on Computing Frontiers, (1-10)
- Gammie P (2013). Synchronous digital circuits as functional programs, ACM Computing Surveys, 46:2, (1-27), Online publication date: 1-Nov-2013.
- Hong S, Chafi H, Sedlar E and Olukotun K Green-Marl Proceedings of the seventeenth international conference on Architectural Support for Programming Languages and Operating Systems, (349-362)
- Hong S, Chafi H, Sedlar E and Olukotun K (2012). Green-Marl, ACM SIGARCH Computer Architecture News, 40:1, (349-362), Online publication date: 18-Apr-2012.
- Hong S, Chafi H, Sedlar E and Olukotun K (2012). Green-Marl, ACM SIGPLAN Notices, 47:4, (349-362), Online publication date: 1-Jun-2012.
- Willcock J, Newton R and Lumsdaine A Avalanche Proceedings of the 1st ACM SIGPLAN workshop on Functional high-performance computing, (15-26)
- Rompf T and Odersky M (2012). Lightweight modular staging, Communications of the ACM, 55:6, (121-130), Online publication date: 1-Jun-2012.
- Rompf T and Odersky M (2010). Lightweight modular staging, ACM SIGPLAN Notices, 46:2, (127-136), Online publication date: 26-Jan-2011.
- Tang X and Järvi J Generic flow-sensitive optimizing transformations in C++ with concepts Proceedings of the 2010 ACM Symposium on Applied Computing, (2111-2118)
- Rompf T and Odersky M Lightweight modular staging Proceedings of the ninth international conference on Generative programming and component engineering, (127-136)
- Chafi H, DeVito Z, Moors A, Rompf T, Sujeeth A, Hanrahan P, Odersky M and Olukotun K Language virtualization for heterogeneous parallel computing Proceedings of the ACM international conference on Object oriented programming systems languages and applications, (835-847)
- Chafi H, DeVito Z, Moors A, Rompf T, Sujeeth A, Hanrahan P, Odersky M and Olukotun K (2010). Language virtualization for heterogeneous parallel computing, ACM SIGPLAN Notices, 45:10, (835-847), Online publication date: 17-Oct-2010.
- Tang X and Järvi J Concept-based optimization Proceedings of the 2007 Symposium on Library-Centric Software Design, (97-108)
- Gibbons J Datatype-generic programming Proceedings of the 2006 international conference on Datatype-generic programming, (1-71)
- Carette J and Kiselyov O Multi-stage programming with functors and monads Proceedings of the 4th international conference on Generative Programming and Component Engineering, (256-274)
Index Terms
- Active libraries and universal languages
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 ...
A framework for extensible languages
GPCE '13: Proceedings of the 12th international conference on Generative programming: concepts & experiencesExtensible programming languages such as SugarJ or Racket enable programmers to introduce customary language features as extensions of the base language. Traditionally, systems that support language extensions are either (i) agnostic to the base ...