类型参数和指数之间的区别？

Question

我是依赖类型的新手,我对这两者之间的区别感到困惑.看来人们通常说一个类型是由其他类型的参数,并通过一定的价值索引.但是,依赖类型语言中的类型和术语之间没有区别吗？参数和指数之间的区别是否基本？你能告诉我在编程和定理证明中它们的含义不同的例子吗？

Answer 1

当您看到一系列类型时,您可能想知道它所具有的每个参数是参数还是索引.

参数仅表示该类型在某种程度上是通用的,并且关于所提供的参数具有参数化的行为.

这意味着,例如,是该类型List T将具有相同的形状,无论哪个T你考虑:nil,cons t0 nil,cons t1 (cons t2 nil)等的选择T不仅影响其值可以被塞紧t0,t1,t2.

另一方面,指数可能会影响您在类型中找到的居民!这就是为什么我们说他们索引一个类型的家族,也就是说,每个索引都告诉你你正在看哪个类型(在类型族中)(在这个意义上,参数是一个退化的情况,其中所有索引都指向到同一组"形状").

例如,类型系列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的指数.当你收到一些x类型F T n,看看什么T是不会透露任何关于x.但看着n会告诉你:

• 这x必须是C1或C3当n是0
• 这x必须是C2在n为1
• 这x肯定是从矛盾中产生的

同样,如果你收到一个y类型F T 0,你知道你只需要对C1和进行模式匹配C3.