Subtyping delimited continuations
Subtyping delimited continuations
复制标题
子类型化分隔延续
DOI：
10.1145/2034773.2034786
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Dariusz Biernacki
中科院分区：
文献类型：
--
作者：
Marek Materzok;Dariusz Biernacki
我们提出了一个类型系统，该系统具有对一流的划界连续性的亚型，该连续性通过维护Metacontext中的上下文类型来概括Danvy和Filinski的类型系统，以进行轮班和重置。我们通过考虑可以访问MetAcontext中任意上下文的控制运算符来利用这种概括。我们使用亚型来控制该表达式实际需要的信息级别，尤其是将纯表达迫使纯表达式变成有效的表达式。对于这种类型的系统，我们证明了强烈的声音性和评估的终止，并提出了一种正确的类型重建算法。我们还介绍了两个针对shift0和reset0的CPS翻译：一个针对未型lambda cyculus的CPS翻译，另一个针对类型为定向的 - 针对简单的lambda cyculus。后一种翻译保留了特异性，并且具有选择性，因为它可以将纯表达式保持直接样式。
We present a type system with subtyping for first-class delimited continuations that generalizes Danvy and Filinski's type system for shift and reset by maintaining explicit information about the types of contexts in the metacontext. We exploit this generalization by considering the control operators known as shift0 and reset0 that can access arbitrary contexts in the metacontext. We use subtyping to control the level of information about the metacontext the expression actually requires and in particular to coerce pure expressions into effectful ones. For this type system we prove strong type soundness and termination of evaluation and we present a provably correct type reconstruction algorithm. We also introduce two CPS translations for shift0 and reset0: one targeting the untyped lambda calculus, and another - type-directed - targeting the simply-typed lambda calculus. The latter translation preserves typability and is selective in that it keeps pure expressions in direct style.