Closed type families with overlapping equations
Closed type families with overlapping equations
复制标题
具有重叠方程的闭型族
DOI：
10.1145/2535838.2535856
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Stephanie Weirich
中科院分区：
文献类型：
--
作者：
R. Eisenberg;Dimitrios Vytiniotis;Simon Peyton Jones;Stephanie Weirich
开放的类型级函数是Haskell最近的一项创新，它将Haskell推向依赖类型的表达性，同时保留了实用编程语言的外观和感觉。本文展示了如何进一步增加可表达性，通过添加闭型函数，其方程可以重叠，并且可以在开放型宇宙上具有非线性模式。尽管这些特性在实践中很有用且易于实现，但它们在某些方面超越了传统的依赖类型理论，并且具有微妙的元理论。
Open, type-level functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still further, by adding closed type functions whose equations may overlap, and may have non-linear patterns over an open type universe. Although practically useful and simple to implement, these features go beyond conventional dependent type theory in some respects, and have a subtle metatheory.