7
$\begingroup$

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?
$\endgroup$
6
$\begingroup$

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.

$\endgroup$
  • 3
    $\begingroup$ That makes sense. So the rule of thumb is that indices can be used for anything, parameters can only be used when the same value is used in the conclusion of all constructors, but parameters are preferable because they make induction simpler. $\endgroup$ – Warbo Jan 30 '14 at 18:21
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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