类型参数和索引之间的区别? [英] Difference between type parameters and indices?

问题描述

我对依赖类型是陌生的，并且对两者之间的区别感到困惑.似乎人们通常会说一种类型是由另一种类型参数化，而由某些值索引.但是，在依赖类型的语言中，类型和术语之间是否没有区别?参数和索引之间的区别是根本的吗?能否给我展示一些示例，这些示例在编程和定理证明中都表现出不同的含义?

I am new to dependent types and am confused about the difference between the two. It seems people usually say a type is parameterized by another type and indexed by some value. But isn't there no distinction between types and terms in a dependently typed language? Is the distinction between parameters and indices fundamental? Can you show me examples showing difference in their meanings in both programming and theorem proving?

推荐答案

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

When you see a family of types, you may wonder whether each of the arguments it has are parameters or indices.

参数仅表示该类型在某种程度上是通用的，并且对于所提供的参数，其表现为参数.

Parameters are merely indicative that the type is somewhat generic, and behaves parametrically with regards to the argument supplied.

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

What this means for instance, is that the type List T will have the same shapes regardless of which T you consider: nil, cons t0 nil, cons t1 (cons t2 nil), etc. The choice of T only affects which values can be plugged for t0, t1, t2.

指数可能会影响您在类型中找到哪些居民！这就是为什么我们说它们 index 一类类型，也就是说，每个索引都告诉您正在查看的是哪种类型(在该类类型之内)(从这个意义上讲，参数是一个所有索引都指向同一组形状"的简并情况.

Indices on the other hand may affect which inhabitants you may find in the type! That's why we say they index a family of types, that is, each index tells you which one of the types (within the family of types) you are looking at (in that sense, a parameter is a degenerate case where all the indices point to the same set of "shapes").

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

For instance, the type family Fin n or finite sets of size n contains very different structures depending on your choice of n.

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

The index 0 indices an empty set. The index 1 indices a set with one element.

从这个意义上讲，对索引价值的了解可能会携带重要的信息！通常，您可以通过查看索引来了解使用或不使用哪些构造函数.这样，依赖类型语言中的模式匹配就可以消除不可行的模式，并从触发模式中提取信息.

In that sense, the knowledge of the value of the index may carry important information! Usually, you can learn which constructors may or may not have been used by looking at an index. That's how pattern-matching in dependently-typed languages can eliminate non-feasible patterns, and extract information out of the triggering of a pattern.

这就是为什么在定义归纳族时，通常可以为整个类型定义参数，但是必须为每个构造函数指定索引(因为允许为每个构造函数指定其存在的索引)在).

This is why, when you define inductive families, usually you can define the parameters for the entire type, but you have to specify the indices for each constructor (since you are allowed to specify, for each constructor, what indices it lives at).

例如，我可以定义:

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会告诉你:

Here, T is a parameter, while 0 and 1 are indices. When you receive some x of type F T n, looking at what T is will not reveal anything about x. But looking at n will tell you:

• 当n为0
时，x必须为C1或C3
• 当n为1
时，x必须为C2
• 否则必须从矛盾中伪造出x

• that x must be C1 or C3 when n is 0
• that x must be C2 when n is 1
• that x must have been forged from a contradiction otherwise

类似地，如果收到类型为F T 0的y，则知道只需要与C1和C3进行模式匹配.

Similarly, if you receive a y of type F T 0, you know that you need only pattern-match against C1 and C3.

这篇关于类型参数和索引之间的区别?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！