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

23

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.

Ben Millwood
quelle
6
Ich denke, Sie haben bereits Ihre Antwort: Es gibt keine akzeptierte Definition für schwaches und starkes Tippen.
Svick
Ich würde es nicht schwer glauben, aber ich stelle die Frage in der Hoffnung, dass es eine gibt, von der ich noch nichts gehört habe :) oder zumindest eine Definition, die maßgeblicher ist als die, die ein Typ, der ein Wiki bearbeitet hat, für den Fall hält .
Ben Millwood
3
Weitere Informationen hierzu finden Sie in dieser verwandten Frage zu SO .
Svick
1
Um Svicks Standpunkt zu bekräftigen, ist es nicht möglich, eine Autoritätsreferenz für etwas zu finden, das nicht akzeptiert wird. Alles, was behauptet, maßgebend zu sein, wäre einfach falsch (da eine beliebige Anzahl von Gegenbeispielen angegeben werden könnte).
edA-qa mort-ora-y
Nun, es gibt einen Unterschied zwischen jemandem, der ein Papier mit der Aufschrift "Hier ist die einzig wahre Definition, über die sich alle einig sind" schreibt, und jemandem, der ein Papier mit der Aufschrift "Hier sind die Definitionen, die ich für dieses Papier verwenden werde, obwohl ich weiß, dass es solche gibt Andere". Auch letzteres wäre besser als das, was ich bisher kenne. Ich denke, Sie haben vielleicht Recht. In welchem ​​Fall haben die Leute etwas über die verschiedenen Arten von Typensystemen zu sagen? Ist die dynamische / statische Unterscheidung zumindest konkret?
Ben Millwood

Antworten:

18

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.

Uday Reddy
quelle
Können Sie einige Referenzen für die historische Entwicklung geben? "Das Fehlen von Laufzeitfehlern bedeutet nichts" - meinst du hier die Kompilierungszeit?
Raphael
Hier ist ein Artikel über Euclid , der in Google Scholar veröffentlicht wurde. Ich erinnere mich, dass ich in den 70er Jahren mehrere Artikel gesehen habe, in denen behauptet wurde, Sprachen seien stark typisiert. Es wurde allgemein als Verkaufsargument angesehen.
Uday Reddy
1
@ Raffael. Ich meinte "Laufzeitfehler". Um zur Laufzeit zu gelangen, müsste das Programm zunächst an der statischen Typprüfung vorbeikommen. Der Punkt ist, dass eine stark typisierte Sprache, z. B. Java, zur Laufzeit Typfehler liefert, wenn sie beim Kompilieren nicht überprüft werden kann. Mit einer Typ-Hole-Sprache, z. B. C, kann die Laufzeit Datenmüll erzeugen, anstatt Fehler zu verursachen.
Uday Reddy
1
@benmachine. Siehe den Abschnitt über "Typprüfung" in dem von mir zitierten Euclid-Papier. Ich denke, der wichtigste Punkt ist, dass "stark getippt" ein Modewort ist. Es ist kein technischer Begriff. Bestenfalls soll der technische Inhalt bedeuten, dass es keine Typlöcher gibt.
Uday Reddy
1
Bei einer typischen modernen Implementierung, bei der zwei verschiedene Integer-Typen dieselbe Darstellung haben (z. B. beide intund long32 Bit oder beide longund long long64 Bit), verwendet ein Programm einen Zeiger auf einen solchen Typ, um Speicher zu schreiben, und verwendet einen Zeiger des anderen Typs Das Lesen löst in der Regel keinen erkennbaren Laufzeitfehler aus, kann aber auf beliebige andere Art und Weise zu Fehlfunktionen führen. “Modern C verliert somit die Typensicherheit anderer Sprachen, ohne die Semantik zu erlangen, die bei hochwertigen Implementierungen von Ritchies Sprache vorherrschte früher im Austausch angeboten
Supercat
7

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.

Benmachine
quelle
Als Community-Wiki gepostet, da ich die Anerkennung dafür nicht verdiene.
Ben Millwood
Das Problem, das ich hier habe, bezieht sich auf Svicks ersten Kommentar. Es mag zwar schön sein, dass Sie eine Definition für starke Typisierung gefunden haben, aber dies ist sicherlich keine allgemein akzeptierte Definition.
edA-qa mort-ora-y
@ edA-qamort-ora-y: auf welcher grundlage sagst du das? Haben Sie etwas Besseres als anekdotische Beweise dafür, was allgemein akzeptiert wird und was nicht? Irgendwelche Zitate? (Ich verstehe, dass Sie vielleicht einen gültigen Punkt haben, auch wenn dies nicht der Fall ist, aber ich denke immer noch, dass das oben Gesagte meine Frage beantwortet. Auch wenn es keinen Konsens gibt, ist es gut, mindestens eine der ernsthaften akademischen Antworten zu kennen.)
Ben Millwood
1
Ich kann das Fehlen einer vereinbarten Definition nicht wirklich beweisen, oder? Das ist logisch nicht möglich. Die Wikipedia-Artikel zu starker Typisierung liefern jedoch viele Beweise und Hinweise für Meinungsverschiedenheiten und Widersprüche. en.wikipedia.org/wiki/Strong_typing
edA-qa mort-ora-y
@ edA-qamort-ora-y: Die Zitate aus Wikipedia sind nicht wirklich hilfreich: Einige sind nicht akademisch, andere werden aus anderen Gründen als der Definition der Begriffe zitiert. Das Typische Programmierpapier scheint vielversprechend zu sein, bezieht sich jedoch nur ganz kurz auf die Definitionen; Vielleicht lohnt es sich trotzdem, meine Antwort zu überarbeiten. In Bezug auf den Nachweis der Abwesenheit denke ich, dass der Nachweis von Kontroversen / Meinungsverschiedenheiten zwischen Menschen, die wissen, wovon sie sprechen, für mich ausreichen würde (was mir das Typeful Programming Paper in der Tat geben könnte).
Ben Millwood
6

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.

Uday Reddy
quelle
Hervorragend, genau das wollte ich. Die Zeitung braucht ein wenig Lesen, daher denke ich, dass es eine Antwort geben sollte, die die wichtigsten Punkte zusammenfasst. Soll ich sie in deine Antwort einfügen oder meine eigene Community-Wiki-Antwort posten? In jedem Fall werde ich noch ein paar Tage warten, falls jemand anderes etwas dazu sagt, und dann akzeptieren, was noch übrig ist :)
Ben Millwood,
@benmachine. Das vollständige Papier ist eine Lektüre wert, aber die konzeptionellen Fragen auf hoher Ebene werden nur in den ersten Abschnitten behandelt.
Uday Reddy
4
Ich denke immer noch, dass es auf dieser Seite zusammengefasst werden sollte. Der Link läuft möglicherweise später ab.
Ben Millwood
@benmachine. Sie können gerne eine Zusammenfassung als Ihre eigene Antwort auf Ihre Frage posten.
Uday Reddy