依赖类型的效应处理
编程语言
2016-03-15 v1
摘要
我们将Levy的按推送值调用(CBPV)分析从简单类型论扩展到依赖类型论(DTT)，以研究计算效应与依赖类型之间的相互作用。我们定义了依赖类型化CBPV的朴素系统dCBPV-，以及带有依赖函数的克莱斯利扩展原理的扩展系统dCBPV+。我们在一系列效应存在的情况下，从语法、范畴语义、具体模型和操作语义的角度研究了这些系统。我们观察到，尽管若要对DTT进行良定义的按值调用(CBV)和按名调用(CBN)翻译需要dCBPV+的表达能力，但在某些效应存在时，它是不如dCBPV-直观的系统。事实上，为了能够构造具体模型并在操作语义中保持主体归约性质，我们被迫施加某些子类型条件，其理念是计算的类型随着某些效应的执行可能变得更为（而非更不）具体。
引用
@article{arxiv.1603.04298,
title = {An Effectful Treatment of Dependent Types},
author = {Matthijs Vákár},
journal= {arXiv preprint arXiv:1603.04298},
year = {2016}
}
备注
arXiv admin note: substantial text overlap with arXiv:1512.08009