依值类型与效应的框架

我们将 Levy 的按值调用推入值 (CBPV) 推广到依值类型论，以更好地理解如何将依值类型与效应相结合。我们定义了 CBPV 的依值类型扩展 dCBPV-，并表明它具有非常自然的小步操作语义，该语义满足主语归约以及（取决于存在的效应）确定性和强归一化，以及优雅的范畴语义——令人惊讶的是，它并不比简单类型语义更复杂。我们拥有从 Moggi 的单子元语言的依值类型版本和按名调用 (CBN) 依值类型论到 dCBPV- 的完全且忠实的翻译，这些翻译产生了预期的操作行为。然而，结果表明 dCBPV- 不足以编码按值调用 (CBV) 依值类型论或 CBN 依值类型论中正连接词的强（依值）消去规则。为了修补这个问题，我们讨论了第二个更具表达力的系统 dCBPV+，它额外具有依值函数的 Kleisli 扩展原理。我们获得了依值类型论到 dCBPV+ 的所需的 CBV 和 CBN 翻译。它也具有自然的范畴语义和操作语义。然而，根据我们考虑的效应，我们可能会失去类型唯一性，因为随着某些效应的执行，计算的类型可能会变得更加具体。这个想法可以使用子类型化的概念被巧妙地形式化。我们希望本文的理论框架一方面至少为如何理解计算效应与依值类型之间关系这一基本类型论问题提供部分答案。另一方面，我们希望它能为实现用于认证效应式编程的优雅的完全成熟语言的最终目标迈出一小步。