Hallo allerseits!
Trotz der Fremdartigkeit und einer gewissen Abstraktion des heute behandelten Themas hoffen wir, dass es Ihr Wochenende abwechslungsreich gestalten kann. Am Ende des Beitrags platzieren wir drei Links des Autors, damit Sie sich mit der abhängigen Eingabe in Idris, F * und JavaScript vertraut machen können
Manchmal scheint es, als hätten sich die Programmiersprachen seit den 60er Jahren nicht viel geändert. Wenn sie mir davon erzählen, erinnere ich mich oft daran, wie viele coole Tools und Funktionen uns jetzt zur Verfügung stehen und wie sie unser Leben vereinfachen. Nebenbei: Dies sind integrierte Debugger, Komponententests, statische Analysatoren und coole IDEs sowie typisierte Arrays und vieles mehr. Die Entwicklung von Sprachen ist ein langer und fortschrittlicher Prozess, und es gibt keine solchen „Silberkugeln“, mit denen sich die Entwicklung von Sprachen ein für alle Mal ändern würde.
Heute möchte ich Ihnen über eine der letzten Phasen dieses laufenden Prozesses berichten. Die Technologie, über die wir sprechen, wird noch aktiv erforscht, aber alles deutet darauf hin, dass sie bald in den gängigen Sprachen Fuß fassen wird. Und unsere Geschichte beginnt mit einem der grundlegendsten Konzepte der Informatik: mit
Typen .
Welt der Typen
Tippen ist eines der Dinge, die so untrennbar mit unserem Denken verbunden sind, dass wir kaum über das Konzept der Typen als solche nachdenken? Warum ist 1 ein
int , aber wenn Sie diesen Wert nur in Anführungszeichen setzen - und er wird zu einer
string ? Was ist im Wesentlichen ein "Typ"? Wie so oft bei der Programmierung hängt die Antwort vom Wortlaut der Frage ab.
Typen sind vielfältig. In einigen Typsystemen gibt es sehr klare Grenzen zwischen Typen und Werten. 3, 2 und 1 sind also
integer Werte, aber
integer ist kein Wert. Dieses Konstrukt ist in die Sprache "eingebettet" und unterscheidet sich grundlegend von der Bedeutung. Tatsächlich ist ein solcher Unterschied jedoch nicht notwendig und kann uns nur einschränken.
Wenn Sie die Typen freigeben und in eine andere Wertekategorie umwandeln, eröffnen sich eine Reihe erstaunlicher Möglichkeiten. Werte können gespeichert, konvertiert und an Funktionen übergeben werden. Auf diese Weise wäre es möglich, eine Funktion zu erstellen, die einen Typ als Parameter verwendet und verallgemeinerte Funktionen erstellt: solche, die mit vielen Typen ohne Überlastung arbeiten können. Sie können ein Array von Werten eines bestimmten Typs haben, anstatt wie in C seltsame Zeigerarithmetik und Typumwandlung durchzuführen. Sie können auch neue Typen sammeln, während das Programm ausgeführt wird, und Funktionen wie die automatische JSON-Deserialisierung bereitstellen. Aber selbst wenn Sie Typen als Werte behandeln, können Sie nicht alles tun, was Typen mit Werten tun können. Wenn Sie also mit Benutzerinstanzen arbeiten, können Sie beispielsweise deren Namen vergleichen, deren Alter oder Kennung überprüfen usw.
if user.name == "Marin" && user.age < 65 { print("You can't retire yet!") }
Wenn Sie jedoch versuchen, dasselbe mit dem
User zu tun, können Sie nur Typnamen und möglicherweise Eigenschaftsnamen vergleichen. Da dies ein Typ und keine Instanz ist, können Sie die Werte seiner Eigenschaften nicht überprüfen.
if typeof(user) == User { print("Well, it's a user. That's all I know") }
Wie cool wäre es, wenn wir eine Funktion hätten, die nur eine nicht leere Benutzerliste empfangen kann? Oder eine Funktion, die eine E-Mail-Adresse nur akzeptiert, wenn sie im richtigen Format aufgezeichnet wird? Für diese Zwecke benötigen Sie die Typen "Nicht leeres Array" oder "E-Mail-Adresse". In diesem Fall ist es ein wertabhängiger Typ, d.h. über
abhängigen Typ . In gängigen Sprachen ist dies nicht möglich.
Damit Typen verwendet werden können, muss der Compiler sie überprüfen. Wenn Sie behaupten, dass die Variable eine Ganzzahl enthält, ist es besser, wenn keine
string darin enthalten ist, da der Compiler sonst schwört. Im Prinzip ist das gut, weil es uns nicht erlaubt zu werben. Das Überprüfen von Typen ist ganz einfach: Wenn eine Funktion eine
integer zurückgibt und wir versuchen,
"Marin" darin zurückzugeben, ist dies ein Fehler.
Bei abhängigen Typen werden die Dinge jedoch komplizierter. Das Problem ist, wenn genau der Compiler die Typen überprüft. Wie kann er sicherstellen, dass das Array genau drei Werte enthält, wenn das Programm noch nicht einmal ausgeführt wird? Wie kann sichergestellt werden, dass eine Ganzzahl größer als 3 ist, wenn sie noch nicht einmal zugewiesen ist? Das ist
Magie ... oder mit anderen Worten
Mathematik . Wenn mathematisch bewiesen werden kann, dass der Satz von Zahlen immer größer als 3 ist, kann der Compiler dies überprüfen.
Mathe im Studio!
Die mathematische Induktion wird verwendet, um Beweise zu formulieren. Die Induktion ermöglicht es uns, die Wahrheit einer Aussage bedingungslos zu bestätigen. Zum Beispiel wollen wir beweisen, dass die folgende mathematische Formel für jede positive Zahl gilt:
1 + 2 + 3 + ... + x = x * (x + 1) / 2
Es gibt unendlich viele mögliche x, daher würde es sehr lange dauern, bis wir alle Zahlen manuell überprüft haben. Zum Glück ist dies nicht notwendig. Wir müssen nur zwei Dinge beweisen:
- Diese Aussage wird für den ersten Tag eingehalten. (Normalerweise ist es 0 oder 1)
- Wenn diese Aussage für die Zahl
n , gilt sie für die nächste Zahl n + 1
Da die Aussage sowohl für die erste als auch für alle folgenden Zahlen eingehalten wird, wissen wir, dass sie für alle möglichen Zahlen gilt.
Dies zu beweisen ist nicht schwierig:
1 = 1 * (1 + 1) / 2 1 = 1
Jetzt müssen wir auch beweisen, dass die Aussage für alle anderen Zahlen gilt. Nehmen Sie dazu an, dass es für eine Zahl n funktioniert, und stellen Sie dann sicher, dass es auch für n + 1 funktioniert.
Angenommen, der folgende Ausdruck ist wahr:
1 + 2 + 3 + ... + n = n * (n + 1) / 2
Überprüfen Sie es für
n + 1 :
(1 + 2 + 3 + ... + n) + (n + 1) = (n + 1) * ((n + 1) + 1) / 2
Somit können wir
"(1 + 2 + 3 + ... + n)" obige Gleichheit ersetzen:
(n * (n + 1) / 2) + (n + 1) = (n + 1) * ((n + 2) / 2)
und vereinfachen
(n + 1) * (n/2 + 1) = (n + 1) * (n/2 + 1)
Da beide Teile des Ausdrucks gleich sind, haben wir sichergestellt, dass diese Aussage wahr ist. Dies ist eine der Möglichkeiten, wie Sie die Richtigkeit von Aussagen überprüfen können, ohne jeden Fall manuell zu berechnen, und auf der Grundlage dieses Prinzips funktionieren abhängige Typen. Sie schreiben eine mathematische Aussage, um sicherzustellen, dass die Typarbeit wahr ist.
Das Schöne an diesem Ansatz liegt in der Tatsache, dass jeder mathematische Beweis in Form eines Computerprogramms ausgestellt werden kann - und genau das brauchen wir!
Zurück zur Programmierung
Wir haben also festgestellt, dass einige Dinge zuerst bewiesen werden können und dann zu bestimmten Werten übergehen. Um dies in einer Programmiersprache zu tun, benötigen Sie eine Möglichkeit, diese Anweisungen in Code auszudrücken, der in das Typsystem selbst geschrieben wird, dh das Typsystem muss verbessert werden.
Betrachten Sie ein Beispiel. Hier haben wir eine Append-Funktion, die zwei Arrays verwendet und kombiniert. In der Regel sieht die Signatur einer solchen Funktion ungefähr so aus:
append: (arr1: Array, arr2: Array) -> Array
Wenn wir uns jedoch nur die Signatur ansehen, können wir nicht sicher sein, ob die Implementierung korrekt ist. Die Tatsache, dass die Funktion ein Array zurückgibt, bedeutet nicht, dass sie etwas getan hat. Eine Möglichkeit, das Ergebnis zu überprüfen, besteht darin, sicherzustellen, dass die Länge des resultierenden Arrays gleich der Summe der Längen der Parameterarrays ist.
newArray = append([1], [2, 3]) assert(length(newArray) == 3)
Aber warum sollten Sie dies zur Laufzeit überprüfen, wenn Sie eine Einschränkung erstellen können, die zur Kompilierungszeit überprüft wird:
append: (arr1: Array, arr2: Array) -> newArray: Array where length(newArray) == length(arr1) + length(arr2)
Wir erklären, dass
append eine Funktion ist, die zwei
Array Argumente
newArray und ein neues
Array Argument zurückgibt, das wir
newArray genannt
newArray . Nur dieses Mal fügen wir eine Einschränkung hinzu, dass die Länge des neuen Arrays der Summe der Längen aller Argumente der Funktion entsprechen sollte. Die Anweisung, die wir oben zur Laufzeit hatten, wird zur Kompilierungszeit in Typ konvertiert.
Der obige Code bezieht sich auf die Welt der Typen, nicht auf Werte,
== Zeichen
== gibt einen Vergleich der zurückgegebenen
length an und nicht deren Wert. Damit ein solcher Mechanismus funktioniert, muss uns die zurückgegebene Typlänge einige Informationen über die tatsächliche Anzahl geben.
Um den Betrieb eines solchen Mechanismus sicherzustellen, müssen Sie sicherstellen, dass jede Nummer von einem separaten Typ ist. Ein Typ kann nur einen Wert enthalten: 1. Gleiches gilt für Zwei, Drei und alle anderen Zahlen. Natürlich ist eine solche Arbeit sehr anstrengend, aber für diese Arbeit haben wir Programmierung. Sie können einen Compiler schreiben, der dies für uns erledigt.
Anschließend können Sie separate Typen für Arrays erstellen, die 1, 2, 3 und eine andere Anzahl von Elementen enthalten.
ArrayOfOne ,
ArrayOfTwo usw.
Somit ist es möglich, eine Funktionslänge zu definieren, die einen der oben genannten Arten von Arrays verwendet und einen abhängigen Rückgabetyp von
One für
ArrayOfOne ,
Two für
ArrayOfTwo usw. hat. für jede Nummer.
Nachdem wir nun einen separaten Typ für eine bestimmte Länge des Arrays haben, können wir (zur Kompilierungszeit) überprüfen, ob beide Arrays gleich lang sind. Vergleichen Sie dazu ihre Typen. Und da Typen dieselben Werte wie alle anderen haben, können Sie ihnen Operationen zuweisen. Sie können die Hinzufügung von zwei bestimmten Typen bestimmen, indem
ArrayOfOne ArrayOfTwo , dass die Summe von
ArrayOfOne und
ArrayOfTwo gleich
ArrayOfThree .
Das sind alle Informationen, die der Compiler benötigt, um sicherzustellen, dass der von Ihnen geschriebene Code korrekt ist.
Angenommen, wir möchten eine Variable vom Typ
ArrayOfThree :
result: ArrayOfThree = append([1], [2, 3])
Der Compiler kann feststellen, dass [1] nur einen Wert hat, sodass Sie den Typ
ArrayOfOne zuweisen
ArrayOfOne . Es kann auch
ArrayOfTwo [2, 3] zuweisen.
Der Compiler weiß, dass der Ergebnistyp gleich der Summe der Typen des ersten und zweiten Arguments sein muss. Er weiß auch, dass ArrayOfOne + ArrayOfTwo gleich ArrayOfThree ist, dh er weiß, dass der gesamte Ausdruck auf der rechten Seite der Identität vom Typ ArrayOfThree ist. Es stimmt mit dem Ausdruck auf der linken Seite überein, und der Compiler ist zufrieden.
Wenn wir folgendes geschrieben haben:
result: ArrayOfTwo = append([1], [2, 3])
dann wäre der Compiler völlig unzufrieden, da er wissen würde, dass der Typ falsch ist.
Abhängiges Tippen ist sehr cool
In diesem Fall ist es einfach unmöglich, eine große Anzahl von Fehlern zuzulassen. Durch abhängige Typisierung können Fehler pro Einheit, Zugriffe auf nicht vorhandene Array-Indizes, Nullzeiger-Ausnahmen, Endlosschleifen und fehlerhafter Code vermieden werden.
Mit abhängigen Typen können Sie fast alles ausdrücken. Die Fakultätsfunktion akzeptiert nur natürliche Zahlen, die
login akzeptiert keine leeren Zeilen, die Funktion
removeLast akzeptiert nur nicht leere Arrays. Darüber hinaus wird dies alles überprüft, bevor Sie das Programm starten.
Das Problem bei Laufzeitprüfungen besteht darin, dass sie fehlschlagen, wenn das Programm bereits ausgeführt wird. Dies ist normal, wenn das Programm nur von Ihnen, nicht aber vom Benutzer ausgeführt wird. Abhängige Typen ermöglichen es Ihnen, solche Überprüfungen auf die Ebene der Typen zu bringen, sodass ein Fehler dieser Art während der Programmausführung unmöglich wird.
Ich denke, abhängiges Tippen ist die Zukunft der gängigen Programmiersprachen, und ich kann es kaum erwarten, darauf zu warten!
→
Idris→
F *→
Hinzufügen abhängiger Typen zu JavaScript