Sind durch Werte parametrisierte Generika die gleichen wie abhängige Typen?

Question

Ich habe über abhängige Typen gelesen und ich habe eine Frage, um sicherzustellen, dass ich nicht etwas falsch verstehe. Die Wikipedia page on dependent types startet damit:

In der Informatik und Logik ist ein abhängiger Typ ein Typ, dessen Definition von einem Wert abhängt. Ein "Paar Ganzzahlen" ist ein Typ. Ein "Paar von ganzen Zahlen, wobei die zweite größer als die erste ist" ist aufgrund der Abhängigkeit von dem Wert ein abhängiger Typ.

---

glaube, ich habe eine Sprache, wo ich eine Zahl in einem Bereich darstellen kann:

struct Int<Min, Max> 

beispielsweise der Typ Int<0, 10> eine ganze Zahl zwischen 0 und einschließlich 10 exklusiv.

Als Bonus, nehme ich an generische Varianz vorstellen:

struct Int<in Min, out Max> 

Zum Beispiel Instanzen von Typen wie Int<3, 10> und Int<0, 8> können Variablen von Int<0, 10> Typ zugeordnet werden.

Int<Min1 + Min2, Max1 + Max2> operator+(Int<Min1, Max1> op1, Int<Min2, Max2> op2); 

Also, das Hinzufügen eines Int<0, 10> und ein erzeugen würde ein Ergebnis vom Typ Int<3, 14>:

Nun ist die Additionsoperation auf diese Art eine Signatur wie diese haben könnte.

In einem solchen Typ-System, konnten wir auch bestellt haben Paare, wie zB:

struct OrderedPair<Min, Mid, Max> 
{ 
    Int<Min, Mid> SmallerNumber; 
    Int<Mid, Max> LargerNumber; 
} 

Und so weiter.

---

Ist das anders als abhängige Typisierung? Wenn das so ist, wie?

Answer 1

Dies ist eine eingeschränkte Form der abhängigen Typisierung, bei der Typen von Werten abhängen können, die jedoch zum Zeitpunkt der Kompilierung verfügbar sein müssen.

In einer vollständig abhängigen typisierten Sprache wie Idris können Typen auch von Laufzeitwerten abhängen - um einen solchen Wert zu erstellen, benötigen Sie einen proof im Bereich, in dem der Wert den Typ bewohnt. Eine Möglichkeit, einen Beweis zu erhalten, ist mit einem einfachen Test (Pseudo-Code):

m = user_input(); 
n = user_input(); 

// Type error: n is not guaranteed to be in range. 
x = Int<0, m>(n); 

if (n >= 0 && n <= m) { 
    // Accepted: proofs of n >= 0 and n <= m in scope. 
    x = Int<0, m>(n); 
} 

So können Sie Ihr Beispiel in (sagen wir) C++ implementieren, sondern eine Int<Min, Max> Konstruktion erfordert eine dynamische Kontrolle im Konstruktor; Wenn C++ volle abhängige Typen hatte, konnte man nicht einmal den Konstruktor ohne irgendeine Form der Überprüfung (statisch oder dynamisch) aufrufen.