轻松实现应答类型修改：类型化定界控制算子的 Prompt 传递风格翻译
编程语言
2016-06-22 v1 计算机科学中的逻辑
摘要
定界控制算子的显著特征是它们能够在计算过程中修改应答类型。这一特征（简称 ATM）使得人们能够紧凑而优雅地表达各种有趣的程序（如类型化 printf），但同时也使得将这些算子嵌入标准函数式语言变得困难。在本文中，我们提出了一种将带有 ATM 的定界控制算子 shift 和 reset 类型化翻译为不带 ATM 的多 prompt shift 和 reset 熟悉语言的方法，这使我们无需修改类型系统即可在标准语言中使用 ATM。我们的翻译推广了 Kiselyov 的类型化 printf 直接风格实现，后者使用两个 prompt 来模拟应答类型的修改，并在计算过程中传递它们。我们证明了我们的翻译保持类型。由于朴素的 prompt 传递风格翻译即使对于纯项也会生成并传递许多 prompt，我们展示了一种仅在需要时生成 prompt 的优化翻译，该翻译同样保持类型。最后，我们给出了一种在构造上保持类型的 tagless-final 风格实现。
引用
@article{arxiv.1606.06379,
title = {Answer-Type Modification without Tears: Prompt-Passing Style Translation for Typed Delimited-Control Operators},
author = {Ikuo Kobori and Yukiyoshi Kameyama and Oleg Kiselyov},
journal= {arXiv preprint arXiv:1606.06379},
year = {2016}
}
备注
In Proceedings WoC 2015, arXiv:1606.05839