Quais são as diferenças e as conseqüências do uso de parâmetros e índices de tipo?

Nas teorias de tipos, como as de Coq, podemos definir um tipo com parâmetros, como este:

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

Como alternativa, podemos definir um tipo com um índice, assim:

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

Minhas perguntas são:

• São fundamentalmente diferentes ou fundamentalmente iguais?
• Quais são as consequências de usar um sobre o outro?
• Quando é preferível usar um sobre o outro?

ListP te ListI tsão isomórficos: eles têm exatamente os mesmos construtores.

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

No entanto, Coq gera diferentes princípios de indução.

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

O princípio de indução de ListIrequer que a propriedade seja paramétrica no tipo de elemento ( P : forall T, ListI T -> Prop) enquanto o princípio de indução de ListPpode ser instanciado em qualquer tipo t( P : ListP t -> Prop). Esta é uma fraqueza do front-end da Coq, na medida em que não é inteligente em relação a tipos recursivos não uniformes; você pode definir manualmente o mesmo princípio de indução (o typechecker o aceita, o que não surpreende, pois é ListP_indtransformado pelo óbvio isomorfismo entre ListPe ListI).

A forma paramétrica ListPé mais simples e fácil de usar pronta para uso. O ListIformulário pode generalizar para recursão não uniforme, onde os parâmetros nas chamadas recursivas não são os originais. Consulte Polimorfismo e tipos de dados indutivos para obter um exemplo.

Eu também achei o seguinte bastante útil, especialmente os comentários:

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

O motivo é que o tipo de identidade Id AMN é "parametrizado" por A e M, mas "indexado" por N. Essa terminologia expressa a diferença entre "uma família de tipos definidos indutivamente" (onde os argumentos da família são chamados parâmetros) e "uma família de tipos definida indutivamente" (onde os argumentos são chamados de índices). Os parâmetros vêm antes do 'mu' (para cada escolha de parâmetros, existe um tipo indutivo). Os índices estão "in the loop" - você está definindo simultaneamente toda a família de tipos de uma só vez, para que diferentes instâncias da família possam se referir uma à outra. Como conseqüência, os índices podem ocorrer de maneira não uniforme (por exemplo, no tipo de resultado de construtores), enquanto os parâmetros são fixados de uma vez por todas.