What are the difference between and consequences of using type parameters and type indexes?

Question

In type theories, like Coq's, we can define a type with parameters, like this:

Inductive ListP (Element : Type) : Type
  := NilP  : ListP Element
   | ConsP : Element -> ListP Element -> ListP Element.

Alternatively, we can define a type with an index, like this:

Inductive ListI : Type -> Type
  := NilI  : forall t, ListI t
   | ConsI : forall t, t -> ListI t -> ListI t.

My questions are:

• Are these fundamentally different or fundamentally the same?
• What are the consequences of using one over the other?
• When is it preferable to use one over the other?

Answer 1

ListP t and ListI t are isomorphic: they have exactly the same constructors.

<prompt>Coq < 12 || 0 < </prompt>Check (NilP, NilI). 
(NilP, NilI)
     : (forall t : Type, ListP t) *
       (forall t : Type, ListI t)

<prompt>Coq < 13 || 0 < </prompt>Check (ConsP, ConsI). 
(ConsP, ConsI)
     : (forall t : Type, t -> ListP t -> ListP t) *
       (forall t : Type, t -> ListI t -> ListI t)

However Coq generates different induction principles.

<prompt>Coq < 14 || 0 < </prompt>Check (ListP_ind, ListI_ind). 
(ListP_ind, ListI_ind)
     : (forall (t : Type) (P : ListP t -> Prop),
        P (NilP t) ->
        (forall (t0 : t) (l : ListP t), P l -> P (ConsP t t0 l)) ->
        forall l : ListP t, P l) *
       (forall P : forall T : Type, ListI T -> Prop,
        (forall t : Type, P t (NilI t)) ->
        (forall (t : Type) (t0 : t) (l : ListI t),
         P t l -> P t (ConsI t t0 l)) ->
        forall (T : Type) (l : ListI T), P T l)

The induction principle of ListI requires the property to be parameteric in the element type (P : forall T, ListI T -> Prop) whereas the induction principle of ListP can be instantiated at any type t (P : ListP t -> Prop). This is a weakness of Coq's front-end, in that it is not smart about non-uniform recursive types; you can manually define the same induction principle (the typechecker accepts it, which is unsurprising given that it is ListP_ind transformed by the obvious isomorphism between ListP and ListI).

The parametric form ListP is simpler and easier to use out of the box. The ListI form can generalize to non-uniform recursion, where the parameters in the recursive calls are not the original. See Polymorphism and Inductive datatypes for an example.

Answer 2

I've also found the following quite useful, especially the comments:

http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/

The reason is that the identity type Id A M N is “parametrized” by A and M, but “indexed” by N. This terminology expresses the difference between “a family of inductively defined types” (where the arguments of the family are called parameters) and “an inductively defined family of types” (where the arguments are called indices). Parameters come before the ‘mu’ (for each choice of parameters, there is an inductive type). Indices are “in the loop”—you are simultaneously defining the whole family of types at once, so different instances of the family can refer to each other. As a consequence, indices can occur non-uniformly (e.g. in the result type of constructors), whereas parameters are fixed once and for all.