Differenza tra parametri tipo e indici?

Question

Sono nuovo ai tipi dipendenti e sono confuso circa la differenza tra i due. Sembra che la gente di solito dica che un tipo è parametrizzato da un altro tipo e indicizzato da un certo valore. Ma non c'è alcuna distinzione tra tipi e termini in un linguaggio tipizzato in modo dipendente? La distinzione tra parametri e indici è fondamentale? Puoi mostrarmi esempi che mostrano differenze nei loro significati sia nella programmazione che nella dimostrazione del teorema?

Answer 1

Quando si vede una famiglia di tipi, si può chiedere se ciascuna delle argomentazioni di cui dispone si parametri o indici.

---

Parametri sono puramente indicativi che il tipo è piuttosto generica, e si comporta parametricamente quanto riguarda l'argomento fornito.

Che cosa questo significa per esempio, è che il tipo di List T avrà le stesse forme, indipendentemente da quale T si considera: nil, cons t0 nil, cons t1 (cons t2 nil), ecc La scelta di T influenza solo i valori che possono essere inseriti per t0, t1 , t2.

---

Indici d'altra parte possono influenzare cui abitanti si può trovare nel tipo! Ecco perché diciamo che indice una famiglia di tipi, ovvero, ogni indice indica quale dei tipi (all'interno della famiglia di tipi) si sta guardando (in questo senso, un parametro è un caso degenerato in cui tutti gli indici puntano allo stesso insieme di "forme").

Ad esempio, la famiglia di tipi Fin n o gruppi di dimensioni finiti n contiene strutture molto diverse a seconda della scelta di n.

L'indice 0 indica un set vuoto. L'indice 1 indica un set con un elemento.

In questo senso, la conoscenza del valore dell'indice può portare informazioni importanti! Di solito, puoi imparare quali costruttori possono o non sono stati usati guardando un indice. È così che l'abbinamento di modelli in linguaggi tipizzati in modo indipendente può eliminare schemi non fattibili ed estrarre informazioni dall'attivazione di un pattern.

---

Questo è il motivo per cui, quando si definiscono le famiglie induttivi, di solito è possibile definire i parametri per l'intero tipo, ma è necessario specificare gli indici per ogni costruttore (da quando si è permesso di specificare, per ogni costruttore, che indice vive in).

Per esempio posso definire:

F (T : Type) : ℕ → Type 
C1 : F T 0 
C2 : F T 1 
C3 : F T 0 

Qui, T è un parametro, mentre 0 e 1 sono indici. Quando si riceve alcun x di tipo F T n, guardando ciò che T non verrà rivelato nulla su x. Ma guardando n vi dirà:

• che x deve essere C1 o C3 quando n è 0
• che x deve essere C2 quando n è 1
• che x deve essere stato forgiato da una contraddizione altrimenti

Analogamente, se si riceve un di tipo F T 0, si è a conoscenza del fatto che è necessario solo il confronto di modelli con C1 e C3.

Answer 2

Ecco un esempio di un tipo paramerised da un certo valore:

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 ∷ [] 

E 'un tipo di liste con ogni elemento minore o uguale n. L'intuizione generale è: se alcune proprietà valgono per ogni abitante di un tipo, allora è possibile astrarlo in parametro. Esiste anche una regola meccanica: "Il primo indice può essere trasformato in un nuovo parametro se ogni costruttore ha la stessa variabile nella prima posizione dell'indice (nel tipo di risultato)." Questa citazione è da *, dovresti leggerlo.

• http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Parameters_vs_Indices.html