Geben Sie System-FAQs ein

Der Autor des Artikels, dessen Übersetzung wir heute veröffentlichen, sagt, dass dieser Beitrag und seine Kommentare als Inspirationsquelle für sein Schreiben gedient haben. Ihm zufolge haben IT-Spezialisten falsche Vorstellungen über Typen, verwenden falsche Terminologie und kommen bei der Erörterung typbezogener Probleme zu falschen Schlussfolgerungen. Er stellt fest, dass er kein Verteidiger des statischen Typsystems ist. Das einzige, was ihn stört, ist die korrekte Verwendung von Begriffen. Dies ermöglicht konstruktive Diskussionen. Der Autor sagt, dass er dieses Material spontan geschrieben hat, hofft aber, dass es keine Fehler enthält. Wenn er etwas verwirrt hat, bittet er ihn darüber zu informieren.



Lassen Sie uns ein für alle Mal verstehen, was bei Typsystemen Verwirrung stiftet.

Dynamische Eingabe und fehlende Eingabe

Einige Leute denken, dass ein dynamisches Typsystem dasselbe ist wie ein untypisiertes Typsystem. Das Fehlen einer Typisierung bedeutet, dass es in einem bestimmten Typensystem keinen Sinn macht, zwischen Typen zu unterscheiden. Es macht keinen Sinn, Typen zu unterscheiden, selbst wenn nur ein Typ im Typensystem vorhanden ist. Zum Beispiel:

• In Assembler ist der einzige Typ eine Bitfolge.
• In der Lambda-Rechnung ist der einzige Typ die Funktion.

Jemand könnte dies bei dieser Gelegenheit sagen: "Aber welchen Unterschied macht es - dynamisches Tippen oder mangelndes Tippen - auch eine Frage für mich." Dies ist jedoch in der Tat ein großes und wichtiges Thema. Tatsache ist, dass, wenn Sie die dynamische Typisierung mit der fehlenden Typisierung gleichsetzen, dies die automatische Übernahme der Tatsache bedeutet, dass ein dynamisches Typsystem das Gegenteil eines statischen Typsystems ist. Infolgedessen werden zwei entgegengesetzte Lager von Programmierern gebildet - das Lager der dynamischen Typisierung und das Lager der statischen Typisierung (und dies ist, wie wir im entsprechenden Abschnitt sehen werden, falsch).

Sprachen, die den Wertebereich von Variablen nicht einschränken, werden als untypisierte Sprachen bezeichnet: Sie haben keine Typen, oder, was dasselbe ist, sie haben nur einen universellen Typ, der alle Werte enthält.
_{Typ Systeme, Luca Cardelli}

Programmiersprachen haben eine interessante Funktion, mit der Sie ihre Welt grob in zwei Gruppen unterteilen können:

• Untypisierte Sprachen - Programme werden einfach ausgeführt. Dies geschieht schnell, ohne zu versuchen, die „Einheitlichkeit der Formulare“ zu überprüfen.
• Typisierte Sprachen - es wird versucht, die „Einheitlichkeit der Form“ zu überprüfen - entweder während der Kompilierung oder während der Programmausführung.

_{"Typensysteme für Programmiersprachen", Benjamin Pearce}

Dynamische und statische Eingabe

Ein dynamisches Typsystem ist ein System, in dem Typen dynamisch überprüft werden (während der Programmausführung). Ein statisches Typsystem ist ein System, in dem Typen statisch überprüft werden (während der Kompilierung oder Codeübersetzung).

Ist eines dieser Systeme das Gegenteil des anderen? Nein, das ist es nicht. Beide Systemtypen können in derselben Sprache verwendet werden. Tatsächlich verfügen die meisten statischen Typsysteme auch über dynamische Typprüfungen. Betrachten Sie als Beispiel die Validierung von Eingabe-Ausgabe-Operationen (Eingabe-Ausgabe, E / A). Stellen Sie sich vor, Sie müssen Daten lesen, die von einem Benutzer bereitgestellt wurden, der eine Nummer eingeben muss. Sie werden während der Programmausführung prüfen, ob die Nummer das Ergebnis des Parsens der entsprechenden Zeile ist (als Ergebnis des Parsens kann eine Ausnahme ausgelöst werden oder etwas wie NaN wird zurückgegeben). Wenn Sie die vom Benutzer eingegebenen Daten überprüfen und herausfinden, ob sie als Zahl betrachtet werden können, führen Sie eine dynamische Typprüfung durch.

Infolgedessen können wir feststellen, dass keine Konfrontation zwischen statischen und dynamischen Typen besteht. Sie können diese und andere in derselben Sprache verwenden.

Darüber hinaus sollte beachtet werden, dass die statische Typprüfung ein komplexer Prozess ist. Manchmal ist es sehr schwierig, einige Teile eines Programms statisch zu überprüfen. Anstatt statische Typprüfungen anzuwenden, können Sie daher auf dynamische Prüfungen zurückgreifen.

Es wird empfohlen, ein statisches Typsystem als Typen zu betrachten, die statisch überprüft werden. Ein dynamisches Typsystem ähnelt Typen, die dynamisch überprüft werden.

Bedeutet die Verwendung statischer Typen, dass Typen zur Kompilierungszeit bekannt sind?

Die im Titel dieses Abschnitts gestellte Frage kann verneint werden. Wenn Sie den Quellcode eines Parsers (einschließlich des JavaScript-Parsers) öffnen, können Sie feststellen, dass der Parser die Wertetypen während des Parsens kennt (dies ist Teil des Kompilierungsprozesses).

 let x = "test"; 

Es stellt sich heraus, dass der Parser weiß, dass "test" eine Zeichenfolge ist. Macht dies JavaScript zu einer statisch typisierten Sprache? Nein, das tut es nicht.

Allmähliches Tippen

Ein schrittweises Typsystem ist ein statisches Typsystem, mit dem Sie Typprüfungen für einige Teile eines Programms überspringen können. In TypeScript wird dies beispielsweise mit any oder @ts-ignore implementiert.

Dies macht zum einen das Typensystem weniger sicher. Auf der anderen Seite können Sie mit einem Typensystem mit schrittweiser Eingabe Sprachen mit dynamischer Eingabe schrittweise Typbeschreibungen hinzufügen.

Zuverlässige und unzuverlässige Systeme

Wenn Sie ein zuverlässiges Typsystem (Soundtypsystem) verwenden, wird das Programm während der Typprüfung nicht "genehmigt", wenn Fehler in Bezug auf Typen in diesem Programm vorliegen. Die Verwendung eines unsoliden Typsystems führt zu der Möglichkeit von Typfehlern im Programm. Es stimmt, Sie sollten nicht in Panik geraten, nachdem Sie davon erfahren haben. In der Praxis hat dies möglicherweise keine Auswirkungen auf Sie. Zuverlässigkeit oder Solidität ist eine mathematische Eigenschaft eines Typprüfungsalgorithmus, der bewiesen werden muss. Viele vorhandene Compiler (intern Typprüfungssysteme) sind unzuverlässig.

Wenn Sie mit zuverlässigen Typsystemen arbeiten möchten, werfen Sie einen Blick auf die Programmiersprachen der ML-Familie, die das Hindley-Milner-Typsystem verwenden.

Darüber hinaus muss verstanden werden, dass ein zuverlässiges Typsystem das falsche Programm nicht überspringt (es liefert keine falsch positiven Testergebnisse, wenn die falschen Programme als korrekt angesehen werden), aber möglicherweise nicht das richtige Programm verfehlt (es kann falsch negative Testergebnisse liefern).

Ein Typsystem, das niemals das richtige Programm ablehnt, wird als vollständig bezeichnet.

Kommt es vor, dass ein Typsystem sowohl zuverlässig als auch vollständig ist? Soweit ich weiß, existieren solche Typsysteme nicht. Ich bin mir bis zum Ende nicht sicher, aber es scheint mir, dass die Existenz solcher Typsysteme, wenn sie auf Gödels Unvollständigkeitssatz beruhen, grundsätzlich unmöglich ist (ich kann mich jedoch irren).

Schwache und starke Eingabe

Ich finde es unangemessen, die Begriffe "schwaches Tippen" und "starkes Tippen" zu verwenden. Diese Begriffe sind nicht eindeutig, ihre Verwendung kann mehr Verwirrung als Klarheit bringen. Lassen Sie mich ein paar Zitate geben.

Diese Sprachen können im übertragenen Sinne Sprachen mit schwacher Typprüfung genannt werden (oder schwach typisierte Sprachen, wie sie normalerweise in verschiedenen Veröffentlichungen genannt werden). Die Verwendung einer schwachen Typprüfung in der Sprache bedeutet, dass einige unsichere Vorgänge statisch erkannt werden und andere nicht. Die "Schwäche" der Typprüfungen in Sprachen dieser Klasse ist sehr unterschiedlich.
_{Typ Systeme, Luca Cardelli}

Die wahrscheinlich häufigste Methode zur Klassifizierung von Typsystemen besteht darin, sie in Systeme mit „schwacher“ und „starker“ Typisierung zu unterteilen. Dies kann nur bedauert werden, da diese Wörter an sich praktisch keine Bedeutung haben. In begrenztem Umfang ist es möglich, zwei Sprachen mit sehr ähnlichen Typsystemen zu vergleichen und eine davon mit einem stärkeren Typsystem als das zweite auszuwählen. In anderen Fällen sind die Begriffe „starkes Tippen“ und „schwaches Tippen“ völlig bedeutungslos.
_{„Wissenswertes vor der Diskussion von Typensystemen“, Steve Klabnik}

Die Begriffe „starkes Tippen“ und „schwaches Tippen“ sind äußerst vieldeutig. Hier sind einige Beispiele für ihre Verwendung:

• Manchmal wird unter „starker Typisierung“ „statische Typisierung“ verstanden. Es ist nicht schwierig, eine solche "Substitution" vorzunehmen, aber es ist besser, wenn man von statischer Typisierung spricht, sie einfach "statisch" zu nennen. Tatsache ist, dass die meisten Programmierer diesen Begriff klar verstehen.
• Wenn sie "starke Typisierung" sagen, meinen sie manchmal "das Fehlen einer impliziten Typkonvertierung". In JavaScript können Sie beispielsweise Ausdrücke wie "a" - 1 . Dies kann als Modell für "schwache Typisierung" bezeichnet werden. Fast alle Sprachen bieten dem Programmierer jedoch einige Möglichkeiten zur impliziten Typkonvertierung, beispielsweise die automatische Konvertierung von Ganzzahlen in Gleitkommazahlen in Ausdrücken wie 1 - 1.1 . In der Praxis unterscheiden die meisten Fachleute, die den Begriff "starkes Tippen" auf diese Weise verwenden, zwischen "akzeptablen" und "nicht akzeptablen" Typkonvertierungen. Es gibt jedoch keine allgemein akzeptierte Grenze zwischen solchen Typkonvertierungen. Die "Akzeptanz" und "Inakzeptanz" von Transformationen ist eine subjektive Bewertung, abhängig von der Meinung einer bestimmten Person.
• Manchmal werden Sprachen mit "starker Typisierung" als Sprachen bezeichnet, in denen es unmöglich ist, die Regeln des in ihnen vorhandenen Typensystems zu umgehen.
• Manchmal bedeutet „starkes Tippen“, über ein Typensystem zu verfügen, mit dem Sie sicher mit dem Speicher arbeiten können. Die C-Sprache ist ein bemerkenswertes Beispiel für eine Sprache, die mit dem Speicher unsicher ist. Wenn xs beispielsweise ein Array mit vier Zahlen ist, genehmigt C einen Code, der problemlos Konstrukte wie xs[5] oder xs[1000] verwendet. Mit ihnen können Sie auf den Speicher zugreifen, der sich nach den Adressen befindet, die zum Speichern des Inhalts des xs Arrays zugewiesen wurden.

_{Die Typen, Gary Bernard}

Benötigen statisch typisierte Sprachen Typdeklarationen?

Statisch typisierte Sprachen benötigen nicht immer Typdeklarationen. Manchmal kann ein Typsystem Typen ableiten (indem Annahmen getroffen werden, die auf der Codestruktur basieren). Hier ist ein Beispiel (TypeScript):

 const x = "test"; 

Das Typsystem weiß, dass "test" eine Zeichenfolge ist (dieses Wissen basiert auf den Regeln der Code-Analyse). Das Typsystem weiß auch, dass x eine Konstante ist, dh der Wert von x kann nicht neu zugewiesen werden. Infolgedessen kann geschlossen werden, dass x vom Typ String ist.
Hier ist ein weiteres Beispiel (Flow):

 const add = (x, y) => x / y //            ^        [1]   . add(1, "2") 

Das Typprüfungssystem erkennt, dass wir die Funktion add aufrufen und ihr eine Zahl und eine Zeichenfolge übergeben. Dies analysiert die Funktionsdeklaration. Das Typprüfsystem weiß, dass zur Durchführung der Teilungsoperation die Nummern rechts und links vom entsprechenden Operator stehen müssen. Einer der an der Divisionsoperation beteiligten Operanden ist keine Zahl. Dadurch werden wir über den Fehler informiert.

Hier gibt es keine Typdeklarationen, dies verhindert jedoch nicht eine statische Typprüfung durch das obige Programm. Wenn Sie in der realen Welt auf ähnliche Situationen stoßen, müssen Sie früher oder später einige Typen deklarieren. Das Typensystem kann nicht absolut alle Typen ableiten. Sie müssen jedoch verstehen, dass eine Sprache nicht als "statisch" bezeichnet werden kann, nicht weil sie Typdeklarationen verwendet, sondern weil Typen vor dem Start des Programms überprüft werden.

Ist TypeScript eine unsichere Sprache, weil darin geschriebener Code in JavaScript-Code kompiliert wird?

TypeScript ist eine unsolide Sprache. Daher kann der darauf geschriebene Code zu unsicheren Anwendungen werden. Dies hat jedoch nichts mit dem zu tun, was es kompiliert.

Die meisten Desktop-Compiler konvertieren Programme in eine Assemblersprache. Und Assembler ist eine Sprache, die noch weniger sicher ist als JS.

Wenn Sie hier auf die Idee zurückkommen, dass TS aufgrund der Kompilierung in JS unsicher ist, könnten Sie den folgenden Gedanken bekommen: „Kompilierter Code wird im Browser ausgeführt, JS ist eine unsichere Sprache und kann die Stelle, an der die Zeile erwartet wird, durch null ersetzen ". Denken ist sinnvoll. Dies ist jedoch wiederum kein Grund, TS als unsichere Sprache zu bezeichnen. Damit TS die Sicherheit innerhalb der Anwendung gewährleisten kann, müssen Sie die "Abwehrmechanismen" an den Stellen platzieren, an denen der TS-Code mit der Außenwelt interagiert. Das heißt, Sie müssen beispielsweise die Richtigkeit der Daten überprüfen, die über die Eingabe-Ausgabe-Mechanismen in das Programm eingegeben werden. Angenommen, dies kann das Überprüfen der Eingabe durch den Benutzer, das Überprüfen der Serverantworten, das Überprüfen der aus dem Browserspeicher gelesenen Daten usw. sein.

Zum Beispiel spielen " Häfen " die Rolle solcher "Abwehrmechanismen" in Elm. In TS können Sie dafür so etwas wie io-ts verwenden.

Der entsprechende „Schutzmechanismus“ schafft eine Brücke zwischen statischen und dynamischen Systemen.

Hier ist ein vereinfachtes Beispiel:

 const makeSureIsNumber = (x: any) => {  const result = parseFloat(x);  if (isNaN(result)) {    throw Error("Not a number");  }  return result; } const read = (input: any) => {  try {    const n = makeSureIsNumber(input);    //     n, ,      //              // makeSureIsNumber "" , n    } catch (e) { } } 

Stimmt es, dass Typen nur für Compiler benötigt werden?

Typen sind nur der Hack, der benötigt wird, um dem Compiler Hinweise zu geben.
_{Waut Mertens}

Werden Typen nur von Compilern benötigt? Dies ist eine philosophische Frage. Typen werden für Menschen benötigt, nicht für Autos. Compiler benötigen Typen, da es sich um Programme handelt, die von Personen geschrieben wurden.

Das Phänomen der Typen existiert aufgrund von Menschen. Typen existieren erst, wenn eine Person etwas in Form eines „Datentyps“ wahrnimmt. Der menschliche Geist teilt verschiedene Entitäten in verschiedene Kategorien ein. Typen sind ohne Beobachter nicht sinnvoll.

Lassen Sie uns ein Gedankenexperiment arrangieren. Denken Sie an das Spiel Life. Sie haben ein zweidimensionales Gitter, das aus quadratischen Zellen besteht. Jede der Zellen kann sich in zwei möglichen Zuständen befinden. Es kann "lebendig" oder "tot" sein. Jede Zelle kann mit ihren acht Nachbarn interagieren. Dies sind Zellen, die vertikal, horizontal oder diagonal an sie angrenzen. Beim Ermitteln des nächsten Status des Systems gelten die folgenden Regeln:

• Eine "lebende" Zelle mit weniger als zwei "lebenden" Nachbarn "stirbt" wie bei einer geringen Bevölkerungsdichte.
• Eine "lebende" Zelle mit zwei oder drei "lebenden" Nachbarn überlebt und fällt in die nächste Generation.
• Eine "lebende" Zelle mit mehr als drei "lebenden" Nachbarn "stirbt" wie bei Überbevölkerung.
• Die "tote" Zelle, die genau drei "lebende" Nachbarn hat, wird "lebendig", wie bei der Reproduktion der Bevölkerung.

Äußerlich sieht es aus wie ein Feld, das in quadratische Zellen unterteilt ist, die ständig „eingeschaltet“ und „ausgeschaltet“ werden. Hier können Sie sich das ansehen.

Wenn Sie das Leben einige Zeit beobachten, können stabile Strukturen wie „Segelflugzeug“ auf dem Feld erscheinen.


Segelflugzeug

Sehen Sie ihn? Ein Segelflugzeug bewegt sich über den Bildschirm. Richtig? Lassen Sie uns jetzt etwas langsamer fahren. Existiert dieser Schirm wirklich? Dies sind nur einzelne Quadrate, die erscheinen und verschwinden. Aber unser Gehirn kann diese Struktur als etwas objektiv Vorhandenes wahrnehmen.

Außerdem können wir sagen, dass das „Segelflugzeug“ existiert, weil die Quadrate nicht unabhängig sind (sie hängen von den Nachbarn ab), und selbst wenn das „Segelflugzeug“ selbst nicht existiert, gibt es ein „Segelflugzeug“ in der Form platonische Ideen.

Zusammenfassung

Betrachten Sie jedes Programm, das in einer typisierten Programmiersprache geschrieben ist. Wir können die Typen beobachten. Richtig? Das Programm wird jedoch in Maschinencodes kompiliert. In diesen Codes wird dasselbe ausgedrückt wie im ursprünglichen Programm (obwohl es für eine Person schwierig ist, maschinelle Darstellungen von Programmen zu lesen). Aus Computersicht gibt es keine Typen. Er sieht nur die Folge von Bits - Mengen von Nullen und Einsen ("tote" und "lebende" Zellen). Es gibt Typen für Menschen, nicht für Autos.

Liebe Leser! Welches Typsystem könnten Sie als ideal für die Webentwicklung betrachten?