GADT遇见子类型化
摘要：广义抽象数据类型（GADT）现在被认为是很好理解的，但是将它们添加到具有子类型概念的语言中会带来一些意外。GADT参数是协变的意味着什么？答案非常微妙。它涉及子类型关系的细粒度属性，引发了有趣的设计问题。我们允许在GADT定义中使用协变注释，研究它们的准确性，并提供了一个检查它们的完备性算法。我们的工作可以应用于具有明确子类型的实际ML-like语言（如OCaml），也可以应用于具有一般子类型约束的语言。
作者：Gabriel Scherer (INRIA Rocquencourt), Didier R''emy (INRIA Rocquencourt)
论文ID：1210.5935
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-10-23