Kategorisierung von Typsystemen (stark / schwach, dynamisch / statisch)

Kurz: Wie werden Typensysteme im akademischen Kontext kategorisiert? insbesondere, wo kann ich seriöse Quellen finden, die die Unterscheidung zwischen verschiedenen Arten von Typsystemen deutlich machen?

In gewisser Weise liegt die Schwierigkeit bei dieser Frage nicht darin, dass ich keine Antwort finden kann, sondern dass ich zu viele finden kann und keine als richtig hervorsticht. Der Hintergrund ist, dass ich versuche, einen Artikel im Haskell-Wiki zum Thema Tippen zu verbessern , in dem derzeit die folgenden Unterscheidungen gemacht werden:

• Keine Typisierung: Die Sprache hat keine Typisierung oder aus typisierter Sicht: Es gibt genau einen Typ in der Sprache. Assemblersprache hat nur den Typ 'Bitmuster', Rexx und Tk haben nur den Typ 'Text', Kern-MatLab hat nur den Typ 'Matrix mit komplexen Werten'.
• Schwache Typisierung: Es gibt nur wenige unterschiedliche Typen und möglicherweise Synonyme für mehrere Typen. Beispielsweise verwendet C Ganzzahlen für Boolesche Werte, Ganzzahlen, Zeichen, Bitmengen und Aufzählungen.
• Starke Typisierung: Feinkörniger Satz von Typen wie in Ada, Wirthian (Pascal, Modula-2), Eiffel

Dies steht im völligen Widerspruch zu meiner persönlichen Wahrnehmung, die eher so aussah:

• Schwache Typisierung: Objekte haben Typen, werden jedoch implizit in andere Typen konvertiert, wenn der Kontext dies erfordert. Zum Beispiel sind Perl, PHP und JavaScript alle Sprachen, in denen "1"mehr oder weniger jeder Kontext verwendet werden 1kann.
• Starke Typisierung: Objekte haben Typen und es gibt keine impliziten Konvertierungen (obwohl Überladung verwendet werden kann, um sie zu simulieren). Die Verwendung eines Objekts im falschen Kontext ist daher ein Fehler. In Python löst das Indizieren eines Arrays mit einem String oder Float eine TypeError-Ausnahme aus. In Haskell schlägt die Kompilierung fehl.

Ich habe andere Personen, die mehr Erfahrung auf diesem Gebiet haben als ich, um Meinungen dazu gebeten, und eine hat diese Beschreibung gegeben:

• Schwache Eingabe: Die Ausführung ungültiger Operationen an Daten wird nicht kontrolliert oder abgelehnt, sondern führt lediglich zu ungültigen / willkürlichen Ergebnissen.
• Starke Typisierung: Operationen an Daten sind nur zulässig, wenn die Daten mit der Operation kompatibel sind.

Soweit ich weiß, würde die erste und letzte Charakterisierung C als schwach typisiert bezeichnen, die zweite als stark typisiert. Der erste und der zweite würden Perl und PHP als schwach typisiert bezeichnen, der dritte als stark typisiert. Alle drei würden Python als stark typisiert beschreiben.

Ich denke, die meisten Leute würden mir sagen "Nun, es gibt keinen Konsens, es gibt keine akzeptierte Bedeutung der Begriffe". Wenn die Leute falsch sind, würde ich gerne davon hören, aber wenn sie richtig sind, dann , wie Sie CS Forscher beschreiben und Typsysteme vergleichen? Welche Terminologie kann ich verwenden, die weniger problematisch ist?

Als verwandte Frage habe ich das Gefühl, dass die dynamische / statische Unterscheidung häufig in Bezug auf "Kompilierungszeit" und "Laufzeit" erfolgt, was ich angesichts der Tatsache, dass eine Sprache kompiliert wird oder nicht, nicht so sehr eine Eigenschaft dieser Sprache ist, als unbefriedigend empfinde als ihre Implementierungen. Ich denke, es sollte eine rein semantische Beschreibung von dynamischer versus statischer Typisierung geben. Etwas im Sinne von "Eine statische Sprache ist eine, in die jeder Unterausdruck eingegeben werden kann". Ich würde mich über alle Gedanken, insbesondere Referenzen, freuen, die Klarheit in diesen Begriff bringen.

Historisch gesehen wurde der Begriff "stark typisierte Programmiersprache" in den 70er Jahren als Reaktion auf die vorhandenen, weit verbreiteten Programmiersprachen verwendet, von denen die meisten Typlöcher aufwiesen. Einige Beispiele:

• In Fortran gab es sogenannte "GEMEINSAME" Speicherbereiche, die von Modulen gemeinsam genutzt werden konnten. Es wurde jedoch nicht geprüft, ob jedes Modul den Inhalt des GEMEINSAMEN Speichers mit demselben Typ deklarierte. Ein Modul könnte also deklarieren, dass ein bestimmter COMMON-Speicherblock eine Ganzzahl und ein anderes eine Gleitkommazahl hat, und die Daten würden dadurch beschädigt. Fortran hatte auch "EQUIVALENCE" -Anweisungen, mit denen derselbe Speicher so deklariert werden konnte, dass er zwei verschiedene Objekte unterschiedlichen Typs enthielt.

• In Algol 60 wurde der Typ der Prozedurparameter als "Prozedur" deklariert, ohne die Typen der Parameter der Prozedur anzugeben. Man könnte also annehmen, dass ein Prozedurparameter eine ganzzahlige akzeptierende Prozedur ist, aber eine echte akzeptierende Prozedur als Argument übergeben. Dies würde zu derselben Art von Korruption führen wie die Anweisungen COMMON und EQUIVALENCE. (Algol 60 beseitigte jedoch die älteren Probleme.)

• In Pascal wurden "Variantendatensätze" hinzugefügt, die fast genau den alten EQUIVALENCE-Anweisungen entsprachen.

• In C wurden "Typumwandlungen" hinzugefügt, wodurch jeder Datentyp als Daten eines anderen Typs interpretiert werden konnte. Dies war eine eher absichtliche Art Loch für Programmierer, die angeblich wissen, was sie tun.

Die stark typisierten Sprachen, die in den 70er Jahren entwickelt wurden, sollten alle derartigen Typlöcher beseitigen. Wenn Sie genauer untersuchen, was dies bedeutet, bedeutet dies im Wesentlichen, dass Datendarstellungen geschützt sind. Es ist nicht möglich, ein Datenobjekt eines Typs als ein Objekt eines anderen Typs anzusehen, das zufällig das gleiche Bitmuster wie seine interne Darstellung aufweist. Theoretiker begannen, den Begriff "Repräsentationsunabhängigkeit" zu verwenden, um diese Eigenschaft zu charakterisieren, anstatt die vage Vorstellung von "starker Typisierung".

Beachten Sie, dass dynamisch typisierte Sprachen wie Lisp, die eine vollständige Typüberprüfung zur Laufzeit durchführen, im Sinne des Schutzes von Repräsentationen "stark typisiert" sind. Gleichzeitig verlieren statisch typisierte Sprachen die Repräsentationsunabhängigkeit, es sei denn, sie überprüften die Array-Grenzen. Sie sind also nicht "stark typisiert" im engeren Sinne. Aufgrund dieser anomalen Konsequenzen wurde der Begriff "stark typisiert" nach den 70er Jahren nicht mehr verwendet. Als das US-Verteidigungsministerium strenge Anforderungen für das Design von Ada entwickelte, enthielten sie die Anforderung, dass die Sprache "stark typisiert" sein sollte. (Es scheint damals geglaubt worden zu sein, dass die Vorstellung von "stark getippt" selbstverständlich war. Es wurde keine Definition angeboten. ) Alle als Antwort eingereichten Sprachvorschläge gaben an, "stark getippt" zu sein. Als Dijkstra alle Sprachvorschläge analysierte, stellte er fest, dass keiner von ihnen stark typisiert war, und tatsächlich war nicht einmal klar, was der Begriff bedeutete. Siehe den BerichtEWD663 . Ich sehe jedoch, dass der Begriff jetzt durch eine jüngere Generation von Forschern, die die wechselvolle Geschichte des Begriffs nicht kennen, wieder verwendet wird.

Der Begriff "statisch typisiert" bedeutet, dass die gesamte Typprüfung statisch erfolgt und zur Laufzeit keine Typfehler auftreten. Wenn die Sprache auch stark typisiert ist, bedeutet dies, dass während der Ausführung keine Tippfehler auftreten . Wenn das Typsystem dagegen Typlöcher enthält, hat das Fehlen von Laufzeit-Typfehlern keine Auswirkung. Die Ergebnisse könnten völlig verfälscht sein.

In der neuen Debatte um "Starke gegen Schwache Typisierung" scheint es darum zu gehen, ob bestimmte Typkonvertierungen zulässig sein sollten. Das Zulassen einer Zeichenfolge, für die eine Ganzzahl erforderlich ist, ist nach diesen Angaben eine "schwache Typisierung". Dies hat einen gewissen Sinn, da der Versuch, eine Zeichenfolge in eine Ganzzahl umzuwandeln, fehlschlagen kann, wenn die Zeichenfolge nicht zufällig eine Ganzzahl darstellt. Das Konvertieren einer Ganzzahl in eine Zeichenfolge hat dieses Problem jedoch nicht. Wäre das laut diesen Leuten ein Beispiel für "schwaches Tippen"? Ich habe keine Ahnung. Mir ist aufgefallen, dass in den Wikipedia-Diskussionen zum Thema "Schwaches Tippen" keine referierten Publikationen genannt werden. Ich glaube nicht, dass es eine zusammenhängende Idee ist.

Anmerkung hinzugefügt : Der grundlegende Punkt ist, dass der Begriff "starke Typisierung" nicht als technischer Begriff mit einer strengen Definition verwendet wurde. Es war eher so, als ob einige Sprachdesigner meinten: "Unser Schriftsystem ist stark, es fängt alle Schreibfehler auf; es hat keine Schriftlöcher." . Es war ein Modewort, das sich gut anhörte und von den Leuten benutzt wurde. Das Cardelli-Wegner-Papier war das erste, das ich gesehen habe, in dem analysiert wurde, was es bedeutet. Mein Beitrag hier sollte als eine Ausarbeitung ihrer Position verstanden werden.

Die Arbeit Uday Reddy, die er in seiner Antwort Auf das Verständnis von Typen, Datenabstraktion und Polymorphismus (1985) fand, gibt die folgenden Antworten:

Programmiersprachen, in denen der Typ jedes Ausdrucks durch statische Programmanalyse bestimmt werden kann, werden als statisch typisiert bezeichnet. Statische Typisierung ist eine nützliche Eigenschaft, aber die Anforderung, dass alle Variablen und Ausdrücke zur Kompilierungszeit an einen Typ gebunden sind, ist manchmal zu restriktiv. Es kann durch die schwächere Anforderung ersetzt werden, dass garantiert ist, dass alle Ausdrücke typenkonsistent sind, obwohl der Typ selbst statisch unbekannt sein kann. Dies kann in der Regel durch die Einführung einer Laufzeit-Typprüfung erreicht werden. Sprachen, in denen alle Ausdrücke typenkonsistent sind, werden als stark typisierte Sprachen bezeichnet. Wenn eine Sprache stark typisiert ist, kann der Compiler garantieren, dass die von ihr akzeptierten Programme ohne Tippfehler ausgeführt werden. Im Allgemeinen sollten wir nach einer starken Typisierung streben und statische Typisierung anwenden, wann immer dies möglich ist.

Maßgebliche Antworten finden Sie in Cardellis und Wegners Umfrageartikel: Über das Verständnis von Typen, Datenabstraktion und Polymorphismus .

Wohlgemerkt, während "starkes Tippen" eine akzeptierte Bedeutung hat, tut "schwaches Tippen" dies nicht. Jeder Fehler bei starker Typisierung kann als schwach angesehen werden, und die Leute können sich unterscheiden, welche Art von Fehler akzeptabel ist und welche nicht.