Unifying Analytic and Statically-Typed Quasiquotes

被引:11
|
作者
Parreaux, Lionel [1 ]
Voizard, Antoine [2 ]
Shaikhha, Amir [1 ]
Koch, Christoph E. [1 ]
机构
[1] Ecole Polytech Fed Lausanne, Lausanne, Switzerland
[2] Univ Penn, Philadelphia, PA 19104 USA
基金
瑞士国家科学基金会; 美国国家科学基金会;
关键词
quasiquotes; metaprogramming; rewriting; static typing;
D O I
10.1145/3158101
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Metaprograms are programs that manipulate (generate, analyze and evaluate) other programs. These tasks are greatly facilitated by quasiquotation, a technique to construct and deconstruct program fragments using quoted code templates expressed in the syntax of the manipulated language. We argue that two main flavors of quasiquotes have existed so far: Lisp-style quasiquotes, which can both construct and deconstruct programs but may produce code that contains type mismatches and unbound variables; and MetaML-style quasiquotes, which rely on static typing to prevent these errors, but can only construct programs. In this paper, we show how to combine the advantages of both flavors into a unified framework: we allow the construction, deconstruction and evaluation of program fragments while ensuring that generated programs are well-typed and well-scoped, a combination unseen in previous work. We formalize our approach as lambda({}), a multi-stage calculus with code pattern matching and rewriting, and prove its type safety. We also present its realization in Squid, a metaprogramming framework for Scala, leveraging Scala's expressive type system. To demonstrate the usefulness of our approach, we introduce speculative rewrite rules, a novel code transformation technique that makes decisive use of these capabilities, and we outline how it simplifies the design of some crucial query compiler optimizations.
引用
收藏
页数:33
相关论文
共 49 条