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.

翻译：在功能性编程语言中,通用代数数据类型(GADTs)非常有用,因为由于类型参数的统一失败,可以排除不必要地比对数据类型的模式。在依赖性类型系统中,这通常被称为索引型,特别有用,因为身份类型是其特例。然而,模式比对指数型非常复杂,因为它一般需要术语的统一。我们研究了一种简化的索引型(所谓的简化索引型),我们明确指定了构建者的选择过程,我们讨论了其明确性、局限性和属性。