An effectful way to eliminate addiction to dependence
An effectful way to eliminate addiction to dependence
复制标题
消除依赖成瘾的有效方法
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Nicolas Tabareau
中科院分区：
文献类型：
--
作者：
Pierre;Nicolas Tabareau
我们定义了类型理论的一元翻译，称为断奶翻译，它允许依赖类型理论中的大范围影响，例如异常、非终止、非确定性或写入操作。通过按推值调用分解，我们解释了为什么传统方法因类型依赖而失败，并证明了我们的方法的合理性。至关重要的是，该构造要求单子的代数域本身形成一个代数。断奶翻译适用于具有依赖消除限制版本的归纳构造微积分 (CIC) 版本。最后，我们展示了如何通过将参数化技术与断言翻译相结合来恢复完整 CIC 的翻译。这提供了 CIC 的第一个有效版本。
We define a monadic translation of type theory, called the weaning translation, that allows for a large range of effects in dependent type theory—such as exceptions, non-termination, non-determinism or writing operations. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions (CIC) with a restricted version of dependent elimination. Finally, we show how to recover a translation of full CIC by mixing parametricity techniques with the weaning translation. This provides the first effectful version of CIC.
上下文同构
DOI：
10.1145/3009837.3009898
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Levy P
通讯作者：
Levy P