Polymorphic type assignment and CPS conversion
Polymorphic type assignment and CPS conversion
复制标题
多态类型赋值和 CPS 转换
DOI：
10.1007/bf01019463
复制
发表时间：
1993
期刊：
影响因子：
--
通讯作者：
Mark Lillibridge
中科院分区：
文献类型：
--
作者：
R. Harper;Mark Lillibridge
Meyer 和 Wand 确定，简单类型 λ 演算中的项类型可能以直接方式与其按值调用 CPS 变换的类型相关。这种类型属性可以扩展到类似方案的连续传递原语，这些扩展的健全性由此而来。我们研究了在按值调用和按名称调用解释下将这些结果扩展到 Damas-Milner 多态类型赋值系统。假设多态 let 仅限于值，我们就获得用于按值调用解释的 CPS 变换。并且对于点名翻译没有任何限制。我们证明，完整的 Damas-Milner 语言没有按值调用 CPS 转换来验证 Meyer-Wand 类型属性，并且相当于标准按值调用转换直至操作等效。
Meyer and Wand established that the type of a term in the simply typed λ-calculus may be related in a straightforward manner to the type of its call-by-value CPS transform. This typing property may be extended to Scheme-like continuation-passing primitives, from which the soundness of these extensions follows. We study the extension of these results to the Damas-Milner polymorphic type assignment system under both the call-by-value and call-by-name interpretations. We obtain CPS transforms for the call-by-value interpretation, provided that the polymorphic let is restricted to values. and for the call-by-name interpretation with no restrictions. We prove that there is no call-by-value CPS transform for the full Damas-Milner language that validates the Meyer-Wand typing property and is equivalent to the standard call-by-value transform up to operational equivalence.