43

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

2 Answers 2

53

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.

5
  • 3
    Is there any advantage other than readability to declaring parameters as parameters (e.g. left of the colon) as opposed to as index? Can the type checker always recover the information which of the indices is a parameter? Apr 2, 2017 at 9:54
  • Ah, this is also treated here: people.inf.elte.hu/divip/AgdaTutorial/… Apr 2, 2017 at 9:58
  • 3
    @SebastianGraf Yes, putting parameters on the left affects the shape of the eliminators generated by Coq, as well as the type-checking for depedent pattern-matching. It is "better" to put parameters on the left, as it indicates to Coq that the type is "uniform" in the choice of those parameters, which simplifies things for you down the road.
    – Ptival
    Sep 30, 2017 at 20:17
  • What about this definition? Inductive OnlyBool: Set -> Type := C: OnlyBool bool. Is OnlyBool parametrized or indexed?
    – 12412316
    May 26, 2020 at 7:00
  • 1
    @user3584499 that's clearly an index, since you get to choose its value in the C constructor.
    – Ptival
    May 30, 2020 at 15:55
1

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.