Unterschied zwischen Typparametern und Indizes?

Question

Ich bin neu bei abhängigen Typen und bin verwirrt über den Unterschied zwischen den beiden. Es scheint, dass Leute normalerweise sagen, ein Typ ist , der durch einen anderen Typ und parametrisiert wird, der durch irgendeinen Wert indiziert wird. Aber gibt es keinen Unterschied zwischen Typen und Begriffen in einer abhängig typisierten Sprache? Ist die Unterscheidung zwischen Parametern und Indizes grundlegend? Können Sie mir Beispiele zeigen, die einen Unterschied in ihrer Bedeutung sowohl in der Programmierung als auch in der Theorembeweise zeigen? Hier

Answer 1

Wenn Sie eine Familie von Typen zu sehen, können Sie sich fragen, ob jedes der Argumente es Parameter oder Indizes hat sind.

---

Parameter sind lediglich anzeigt, dass der Typ etwas generisch ist, und verhält sich parametrisch in Bezug auf das Argument geliefert.

Was dies bedeutet beispielsweise, dass der Typ List T die gleichen Formen, unabhängig davon mit T Sie betrachten: nil, cons t0 nil, cons t1 (cons t2 nil) etc. Die Wahl des T wirkt sich nur auf die Werte für t0 gesteckt werden, t1 , t2.

---

Indizes auf der anderen Seite kann sich auf die Einwohner Sie in der Art finden können! Deshalb sagen wir sie Index eine Familie von Typen, das heißt, jeder Index sagt Ihnen, welche der Typen (innerhalb der Familie der Typen) Sie betrachten (in diesem Sinne ist ein Parameter ein degenerierter Fall, in dem alle Indizes zeigen auf die gleiche Menge von "Formen").

Zum Beispiel die Typenfamilie Fin n oder endliche Mengen der Größe n enthält sehr unterschiedliche Strukturen, je nach Ihrer Wahl von n.

Der Index 0 indiziert einen leeren Satz. Der Index 1 indiziert eine Menge mit einem Element.

In diesem Sinne kann die Kenntnis des Werts des Index wichtige Informationen enthalten! Normalerweise können Sie erfahren, welche Konstruktoren möglicherweise verwendet wurden oder nicht, indem Sie einen Index betrachten. Auf diese Weise kann die Mustererkennung in abhängigkeitsgesteuerten Sprachen nicht mögliche Muster eliminieren und Informationen aus dem Auslösen eines Musters extrahieren.Diese

---

Deshalb, wenn Sie definieren induktive Familien, in der Regel können Sie die Parameter für den gesamten Typ definieren, aber Sie müssen die Indizes für jeden Konstruktor angeben (da Sie berechtigt sind, angeben, für jeden Konstrukteur, in welchen Indizes es lebt).

Zum Beispiel kann ich definieren:

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

Hier T ist ein Parameter, während 0 und 1 Indizes sind. Wenn Sie einige x des Typs F T n erhalten, was T ist, wird nichts über x verraten. Aber bei n suchen, werden Sie sagen:

• dass x sein muss C1 oder C3 wenn n0 ist
• dass x muss C2 sein, wenn n ist 1
• dass x muss aus einem Widerspruch sonst geschmiedet worden sind

Ähnlich, Wenn Sie eine y vom Typ F T 0 erhalten, wissen Sie, dass Sie nur eine Musterübereinstimmung mit C1 und C3 benötigen.

Answer 2

ist ein Beispiel für eine Art von einigem Wert paramerised:

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

Es ist eine Art von Listen mit jedem Elemente weniger oder gleich n. Die allgemeine Intuition ist: wenn irgendeine Eigenschaft für jeden Einwohner eines Typs gilt, dann können Sie sie in Parameter abstrahieren. Es gibt auch eine mechanische Regel: "Der erste Index kann in einen neuen Parameter umgewandelt werden, wenn jeder Konstruktor die gleiche Variable an der ersten Indexposition (im Ergebnistyp) hat." Dieses Zitat stammt von *, Sie sollten es lesen.

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