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

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?

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

Coq Check (NilP, NilI). 
(NilP, NilI)
     : (forall t : Type, ListP t) *
       (forall t : Type, ListI t)

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

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

StackExchange Computer Science Q#20100, answer score: 8