Was ist abhängiges Tippen?

Question

Kann mir jemand das abhängige Tippen erklären?Ich habe wenig Erfahrung mit Haskell, Cayenne, Epigram oder anderen funktionalen Sprachen. Je einfacher die Begriffe sind, die Sie verwenden können, desto mehr werde ich es zu schätzen wissen!

Answer 1

Bedenken Sie:In allen anständigen Programmiersprachen kann man Funktionen schreiben, z.B.

def f(arg) = result

Hier, f nimmt einen Wert an arg und berechnet einen Wert result.Es ist eine Funktion von Werten zu Werten.

In einigen Sprachen können Sie nun polymorphe (auch generische) Werte definieren:

def empty<T> = new List<T>()

Hier, empty braucht einen Typ T und berechnet einen Wert.Es ist eine Funktion von Typen zu Werten.

Normalerweise können Sie auch generische Typdefinitionen haben:

type Matrix<T> = List<List<T>>

Diese Definition nimmt einen Typ an und gibt einen Typ zurück.Es kann als Funktion von Typ zu Typ betrachtet werden.

So viel zu dem, was gewöhnliche Sprachen bieten.Eine Sprache heißt abhängig typisiert, wenn sie auch die 4. Möglichkeit bietet, nämlich Funktionen von Werten zu Typen zu definieren.Oder mit anderen Worten: Parametrisieren einer Typdefinition über einen Wert:

type BoundedInt(n) = {i:Int | i<=n}

Einige Mainstream-Sprachen haben eine gefälschte Form davon, die nicht zu verwechseln ist.Z.B.In C++ können Vorlagen Werte als Parameter annehmen, bei der Anwendung müssen sie jedoch Konstanten zur Kompilierungszeit sein.Nicht so in einer wirklich abhängig typisierten Sprache.Ich könnte zum Beispiel den obigen Typ so verwenden:

def min(i : Int, j : Int) : BoundedInt(j) =
  if i < j then i else j

Hier der Ergebnistyp der Funktion kommt darauf an auf den tatsächlichen Argumentwert j, daher die Terminologie.

Answer 2

Wenn Sie C ++ kennen, ist es einfach, ein motivierendes Beispiel zu liefern:

Nehmen wir an, wir haben einen Container -Typ und zwei Fälle davon

typedef std::map<int,int> IIMap;
IIMap foo;
IIMap bar;

und betrachten Sie dieses Code-Fragment (Sie können annehmen, dass Foo nicht leer ist):

IIMap::iterator i = foo.begin();
bar.erase(i);

Dies ist offensichtlicher Müll (und beschädigt wahrscheinlich die Datenstrukturen), aber er wird einwandfrei einkunden, da "Iterator in Foo" und "Iterator in die Balken" der gleiche Typ sind. IIMap::iterator, obwohl sie semantisch völlig inkompatibel sind.

Das Problem ist, dass ein Iterator -Typ nicht nur vom Container abhängen sollte Typ Aber in der Tat auf dem Behälter Objekt, dh es sollte ein "nicht statischer Mitgliedstyp" sein:

foo.iterator i = foo.begin();
bar.erase(i);  // ERROR: bar.iterator argument expected

Ein solches Merkmal, die Fähigkeit, einen Typ (foo.iterator) auszudrücken, der von einem Begriff (FOO) abhängt, ist genau das, was abhängige Typisierung bedeutet.

Der Grund, warum Sie diese Funktion nicht oft sehen, ist, dass sie eine große Dose Würmer öffnet sind äquivalent (liefert immer zur Laufzeit den gleichen Wert). Infolgedessen vergleichen Sie Wikipedia's Liste der abhängig typisierten Sprachen mit Liste der Theoremprovers Sie können eine verdächtige Ähnlichkeit bemerken. ;-)

Answer 3

Abhängige Typen ermöglichen einen größeren Satz von Logikfehler eliminiert werden bei Zeit kompilieren. Um dies zu veranschaulichen, berücksichtigen Sie die folgende Spezifikation zur Funktion f:

Funktion f muss nur nehmen eben Ganzzahlen als Eingabe.

Ohne abhängige Typen könnten Sie so etwas tun:

def f(n: Integer) := {
  if  n mod 2 != 0 then 
    throw RuntimeException
  else
    // do something with n
}

Hier kann der Compiler nicht erkennen, ob n ist in der Tat sogar, das heißt aus der Sicht des Compilers, der folgende Ausdruck ist in Ordnung:

f(1)    // compiles OK despite being a logic error!

Dieses Programm würde zur Laufzeit ausgeführt und dann eine Ausnahme ausführen, dh Ihr Programm hat einen logischen Fehler.

Abhängige Typen ermöglichen es Ihnen, viel ausdrucksvoller zu sein und Ihnen so etwas zu schreiben:

def f(n: {n: Integer | n mod 2 == 0}) := {
  // do something with n
}

Hier n ist von abhängiger Art {n: Integer | n mod 2 == 0}. Es könnte helfen, dies laut zu lesen

n ist ein Mitglied einer Reihe von ganzen Zahlen, so dass jede ganze Zahl durch 2 teilbar ist.

In diesem Fall würde der Compiler zum Kompilieren eines Logikfehlers erkennen, an dem Sie eine ungerade Nummer an übergeben haben f und würde verhindern, dass das Programm überhaupt ausgeführt wird:

f(1)    // compiler error

---

Hier ist ein illustratives Beispiel mit Scala Pfadabhängige Typen Wie wir versuchen könnten, Funktionen implementieren f Befriedigung einer solchen Anforderung:

case class Integer(v: Int) {
  object IsEven { require(v % 2 == 0) }
  object IsOdd { require(v % 2 != 0) }
}

def f(n: Integer)(implicit proof: n.IsEven.type) =  { 
  // do something with n safe in the knowledge it is even
}

val `42` = Integer(42)
implicit val proof42IsEven = `42`.IsEven

val `1` = Integer(1)
implicit val proof1IsOdd = `1`.IsOdd

f(`42`) // OK
f(`1`)  // compile-time error

Der Schlüssel ist zu bemerken, wie Wert n erscheint in der Art von Wert proof nämlich n.IsEven.type:

def f(n: Integer)(implicit proof: n.IsEven.type)
      ^                           ^
      |                           |
    value                       value

Wir sagen Typ n.IsEven.type abhängig von der Wert n Daher der Begriff Abhängige Typen.

Answer 4

Zitieren der Buchtypen und Programmiersprachen (30.5):

Ein Großteil dieses Buches befasste sich mit der formalisierenden Abstraktionsmechanismen verschiedener Art. In dem einfach typisierten Lambda-Kalkulus formalisierten wir den Betrieb, einen Begriff zu nehmen und eine Untermut zu abstrahieren, was eine Funktion erbringt, die später durch die Anwendung unterschiedlicher Begriffe instanziiert werden kann. Im SystemF, Wir haben den Betrieb eines Begriffs und der Zusammenfassung eines Typs in Betracht gezogen, was einen Begriff ergibt, der durch Anwenden auf verschiedene Typen instanziiert werden kann. Imλω, Wir haben die Mechanismen der einfach typisierten Lambda-Kalkulus „One Level Up“ rekapituliert, wobei wir einen Typ einnehmen und einen Subtempression abstrahieren, um einen Typbetreiber zu erhalten, der später durch Anwenden auf verschiedene Typen instanziiert werden kann. Eine bequeme Denkweise an all diese Formen der Abstraktion liegt in Bezug auf Familien von Ausdrücken, die durch andere Ausdrücke indiziert sind. Eine gewöhnliche Lambda -Abstraktion λx:T1.t2 ist eine Familie von Begriffen [x -> s]t1 nach Begriffen indiziert s. In ähnlicher Weise eine Typ -Abstraktion λX::K1.t2 ist eine Familie von Begriffen, die nach Typen indiziert sind, und ein Typbetreiber ist eine Familie von Typen, die nach Typen indiziert sind.

• λx:T1.t2 Familie der Begriffe, die durch Begriffe indiziert sind

• λX::K1.t2 Familie der Begriffe, die nach Typen indiziert sind

• λX::K1.T2 Familie der Typen, die nach Typen indiziert sind

Wenn man sich diese Liste ansieht, ist klar, dass es eine Möglichkeit gibt, die wir noch nicht berücksichtigt haben: Familien von Typen, die nach Begriffen indiziert sind. Diese Form der Abstraktion wurde auch unter der Rubrik abhängiger Typen ausführlich untersucht.