Ein abhängiger Typ ist ein Typ, der von einem Wert abhängt. Ein pfadabhängiger Typ ist eine bestimmte Art eines abhängigen Typs, bei dem der Typ von einem Pfad abhängt.
Ich bin nicht sicher, ob der Begriff "Pfadabhängiger Typ" außerhalb der Scala-Gemeinschaft existiert. In jedem Fall ist die Frage, was ist ein Pfad? Für Scala ist dies in der Sprachspezifikation definiert: grundsätzlich Es ist eine Sequenz von Selektionen a.b.c... auf nicht variablen Werten.
Ein pfadabhängiger Typ ist ein Typ mit einem Pfad, z. B. a.T in
Es gibt andere Arten abhängiger Typen. In Scala ist dies beispielsweise ein ausstehender Vorschlag , dem literalbasierte Typen hinzugefügt werden können die Sprache, damit du val x: 42.type = 21 + 21 schreiben kannst.
Um ein Programm zu testen, das abhängige Typen verwendet, muss das Typsystem (und der Compiler) über die Semantik dieser Werte und ihrer Operationen Bescheid wissen. Der Scala-Compiler kennt die Semantik der Auswahl und kann entscheiden, ob zwei Pfade gleich sind oder nicht. Für das Beispiel, das literalbasierte Typen verwendet, muss der Compiler erweitert werden, um zu wissen, was die Operation + für Ganzzahl bedeutet.
Tags und Links scala dependent-type path-dependent-type