可以将文章内容翻译成中文,广告屏蔽插件可能会导致该功能失效(如失效，请关闭广告屏蔽插件后再试):

问题:

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?

回答1:

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.

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.

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").

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

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).

For instance I can define:

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

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:

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

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

回答2:

Here is an example of a type paramerised by some value:

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 ∷ []

It's a type of lists with every element less or equal n. The general intuition is: if some property holds for every inhabitant of a type, then you can abstract it into parameter. There is a mechanical rule also: "The first index can be turned into a new parameter if each constructor has the same variable on the first index position (in the result type)." This quote is from *, you should read it.