Staging with control: type-safe multi-stage programming with control
Staging with control: type-safe multi-stage programming with control
复制标题
带控制的分段：带控制的类型安全多阶段编程
DOI：
10.1145/3136040.3136049
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Junpei Oishi and Yukiyoshi Kameyama
中科院分区：
文献类型：
--
作者：
Yoko Sogabe;Tsutomu Maruyama;Masayuki Suzuki and Maruyama Tsutomu;Takahisa Watanabe and Yukiyoshi Kameyama;Junpei Oishi and Yukiyoshi Kameyama
分段允许程序员编写特定于域的自定义代码生成器。理想情况下，一个用于staging的编程语言提供了所有必要的功能，并在同一时间，静态保证生成的代码的安全属性，包括良好的类型和良好的范围。我们解决这个经典的问题，语言与控制运算符，允许代码优化的模块化和紧凑的方式。具体来说，我们设计了一个阶段性的编程语言，表达控制操作符shift0和reset0，让我们表达，例如，多层let插入，同时保持良好的类型性和作用域的静态保证。为了这个目的，我们扩展了我们以前的工作，精致的环境分类器，介绍了分期语言的状态。我们表明，我们的语言是表达足够的表达有趣的代码生成技术，类型系统享有类型健全。我们还提到了一个类型推理算法，我们的语言在合理的限制。
Staging allows a programmer to write domain-specific, custom code generators. Ideally, a programming language for staging provides all necessary features for staging, and at the same time, gives static guarantee for the safety properties of generated code including well typedness and well scopedness. We address this classic problem for the language with control operators, which allow code optimizations in a modular and compact way. Specifically, we design a staged programming language with the expressive control operators shift0 and reset0, which let us express, for instance, multi-layer let-insertion, while keeping the static guarantee of well typedness and well scopedness. For this purpose, we extend our earlier work on refined environment classifiers which were introduced for the staging language with state. We show that our language is expressive enough to express interesting code generation techniques, and that the type system enjoys type soundness. We also mention a type inference algorithm for our language under reasonable restriction.