索引类型的更简单编码
A simpler encoding of indexed types
摘要：
在函数式程序设计语言中，广义代数数据类型（GADT）非常有用，因为它们上不必要的模式匹配可以通过类型参数的统一失败来排除。在依赖类型系统中，这通常被称为索引类型，它特别有用，因为标识类型是它的特殊情况。然而，索引类型上的模式匹配非常复杂，因为它通常需要术语统一。我们研究了索引类型的简化版本（称为更简单的索引类型），其中我们显式地指定了构造函数的选择过程，并讨论了它的表达能力，限制和属性。
英文摘要：
In functional programming languages, generalized algebraic data types (GADTs) are very useful as the unnecessary pattern matching over them can be ruled out by the failure of unification of type arguments. In dependent type systems, this is usually called indexed types and it's particularly useful as the identity type is a special case of it. However, pattern matching over indexed types is very complicated as it requires term unification in general. We study a simplified version of indexed types (called simpler indexed types) where we explicitly specify the selection process of constructors, and we discuss its expressiveness, limitations, and properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
