类型参数和索引之间的区别？答案

【问题标题】：Difference between type parameters and indices?类型参数和索引之间的区别？
【发布时间】：2014-08-27 07:48:33
【问题描述】：

我是依赖类型的新手，对两者之间的区别感到困惑。似乎人们通常会说一个类型由另一种类型参数化并且由某个值索引。但是在依赖类型语言中，类型和术语之间不是没有区别吗？参数和指数之间的区别是基本的吗？你能告诉我在编程和定理证明中它们的含义不同的例子吗？

【问题讨论】：

相关类：stackoverflow.com/questions/8962873/…

标签： coq agda dependent-type type-theory idris

【解决方案1】：

当您看到一系列类型时，您可能想知道它的每个参数是 parameters 还是 indices。

参数只是表示该类型有点通用，并且就提供的参数而言，其行为参数化。

这意味着，例如，List T 类型将具有相同的形状，无论您考虑哪个 T：nil、cons t0 nil、cons t1 (cons t2 nil) 等。T 的选择仅影响可以为t0、t1、t2 插入哪些值。

另一方面，

指数可能会影响您可能在该类型中找到的居民！这就是为什么我们说它们 index 是一个类型族，也就是说，每个索引都会告诉您正在查看的类型（在类型族中）（从这个意义上说，参数是所有索引都指向同一组“形状”的退化情况）。

例如，类型族Fin n 或大小有限集n 包含非常不同的结构，具体取决于您选择的n。

索引0 索引一个空集。索引1 索引具有一个元素的集合。

从这个意义上说，指数价值的知识可能携带着重要的信息！通常，您可以通过查看索引来了解可能使用或未使用的构造函数。这就是依赖类型语言中的模式匹配如何消除不可行的模式，并从模式的触发中提取信息。

这就是为什么，当你定义归纳族时，通常你可以为整个类型定义参数，但是你必须为每个构造函数指定索引（因为你可以为每个构造函数指定它所在的索引在）。

例如我可以定义：

F (T : Type) : ℕ → Type
C1 : F T 0
C2 : F T 1
C3 : F T 0

这里，T 是一个参数，而 0 和 1 是索引。当您收到一些F T n 类型的x 时，查看T 是什么不会透露任何关于x 的信息。但是看看n会告诉你：

当n 是0 时，x 必须是 C1 或 C3
当n 是1 时x 必须是C2
x 肯定是从矛盾中伪造出来的，否则

同样，如果您收到F T 0 类型的y，您知道您只需要与C1 和C3 进行模式匹配。

【讨论】：

除了将参数声明为参数（例如，冒号左侧）而不是索引的可读性之外，还有其他优势吗？类型检查器能否始终恢复哪些索引是参数的信息？
啊，这里也处理一下：people.inf.elte.hu/divip/AgdaTutorial/…
@SebastianGraf 是的，将参数放在左侧会影响 Coq 生成的消除器的形状，以及依赖模式匹配的类型检查。将参数放在左侧“更好”，因为它向 Coq 表明在选择这些参数时类型是“统一的”，这可以为您简化后续工作。
这个定义怎么样？ Inductive OnlyBool: Set -> Type := C: OnlyBool bool. OnlyBool 是参数化的还是索引的？
@user3584499 这显然是一个索引，因为您可以在 C 构造函数中选择它的值。

【解决方案2】：

这是一个由某个值参数化的类型的示例：

open import Data.Nat

infixr 4 _∷_

data ≤List (n : ℕ) : Set where
  []  : ≤List n
  _∷_ : {m : ℕ} -> m ≤ n -> ≤List n -> ≤List n

1≤3 : 1 ≤ 3
1≤3 = s≤s z≤n

3≤3 : 3 ≤ 3
3≤3 = s≤s (s≤s (s≤s z≤n))

example : ≤List 3
example = 3≤3 ∷ 1≤3 ∷ []

这是一种列表类型，每个元素都小于或等于n。一般的直觉是：如果某个类型的每个居民都拥有某个属性，那么您可以将其抽象为参数。还有一个机械规则：“如果每个构造函数在第一个索引位置（在结果类型中）具有相同的变量，则可以将第一个索引转换为新参数。” 这句话来自*，你应该阅读它。

http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Parameters_vs_Indices.html

【讨论】：