Was ist ein Typensystem?

50

Hintergrund

Ich entwerfe eine Sprache als Nebenprojekt. Ich habe einen funktionierenden Assembler, einen statischen Analysator und eine virtuelle Maschine dafür. Da ich mit der von mir aufgebauten Infrastruktur bereits nicht-triviale Programme kompilieren und ausführen kann, habe ich mir überlegt, an meiner Universität einen Vortrag zu halten.

Während meines Vortrags erwähnte ich, dass die VM ein Typensystem bereitstellt, und wurde gefragt, " Wofür ist Ihr Typensystem? ". Nachdem ich geantwortet hatte, wurde ich von der Person, die die Frage stellte, ausgelacht.

Obwohl ich mit ziemlicher Sicherheit den Ruf verlieren werde, diese Frage zu stellen, wende ich mich an Programmierer.

Mein Verständnis

Nach meinem Verständnis werden Typsysteme verwendet, um zusätzliche Informationen über Entitäten in einem Programm bereitzustellen, sodass die Laufzeitumgebung, der Compiler oder eine andere Maschine weiß, was mit den Bitfolgen zu tun ist, mit denen sie arbeitet. Sie helfen auch bei der Aufrechterhaltung von Verträgen - der Compiler (oder Code Analyzer oder Runtime oder jedes andere Programm) kann überprüfen, ob das Programm zu einem bestimmten Zeitpunkt mit Werten arbeitet, die von den Programmierern erwartet werden.

Typen können auch verwendet werden, um Informationen für diese menschlichen Programmierer bereitzustellen. Zum Beispiel finde ich diese Erklärung:

function sqrt(double n) -> double;

nützlicher als dieser

sqrt(n)

Ersteres enthält zahlreiche Informationen: Der sqrtBezeichner ist eine Funktion, nimmt eine einzelne doubleals Eingabe und erzeugt eine andere doubleals Ausgabe. Letzteres sagt Ihnen, dass es sich wahrscheinlich um eine Funktion handelt, die einen einzelnen Parameter verwendet.

Meine Antwort

Also, nach der Frage "Wofür ist Ihr Typensystem?" Ich antwortete wie folgt:

Das Typensystem ist dynamisch (Typen werden Werten zugewiesen, nicht Variablen, die sie enthalten), aber ohne überraschende Zwangsregeln stark (Sie können der Ganzzahl keine Zeichenfolge hinzufügen, da sie inkompatible Typen darstellen, aber Sie können der Gleitkommazahl eine Ganzzahl hinzufügen). .

Das Typsystem wird von der VM verwendet, um sicherzustellen, dass Operanden für Anweisungen gültig sind. und kann von Programmierern verwendet werden, um sicherzustellen, dass an ihre Funktionen übergebene Parameter gültig sind (dh vom richtigen Typ sind).
Das Typsystem unterstützt Untertypen und Mehrfachvererbung (beide Funktionen stehen Programmierern zur Verfügung), und Typen werden berücksichtigt, wenn der dynamische Versand von Methoden für Objekte verwendet wird. VM verwendet Typen, um zu überprüfen, welche Funktion eine bestimmte Nachricht für einen bestimmten Typ implementiert.

Die Folgefrage lautete "Und wie wird einem Wert der Typ zugewiesen?". Daher erklärte ich, dass alle Werte in Kästchen angeordnet sind und einen Zeiger auf eine Typdefinitionsstruktur haben, die Informationen zum Namen des Typs, zu den Nachrichten, auf die er reagiert, und zu den Typen, von denen er erbt, enthält.

Danach wurde ich ausgelacht und meine Antwort mit dem Kommentar "Das ist kein echtes Typensystem." Abgewiesen.

Also - wenn das, was ich beschrieben habe, nicht als "echtes Typensystem" zu qualifizieren ist, was wäre das? Hat diese Person recht, dass das, was ich zur Verfügung stelle, nicht als ein Typensystem angesehen werden kann?

Mael
quelle
19
Wenn von Typsystemen die Rede ist, spricht man normalerweise von statischer Typisierung. Dynamisches Tippen ist für Leute, die sich für Schriftsysteme interessieren, nicht sehr interessant, da es so gut wie nichts garantiert. ZB Welche Art von Wert kann Variable x enthalten? Etwas.
Doval
7
Ich wäre neugierig zu hören, was sie zu sagen hatten, um ihre Reaktion zu verteidigen / zu erklären.
Newtopian
18
@Doval Durch dynamisches Tippen können Sie sicherstellen, dass Sie keinen unsinnigen Zustand annehmen, indem Sie Ihrer Katze beispielsweise 5 hinzufügen. Sicher, es wird Sie nicht davon abhalten, es zu versuchen , aber es kann zumindest verhindern, dass es tatsächlich passiert, und Ihnen eine Chance geben, herauszufinden, was schief gelaufen ist, und Korrekturmaßnahmen zu ergreifen, Dinge, die eine wirklich typenlose Sprache nicht kann.
8bittree
10
Die Person hat Probleme mit Ihrer Antwort auf "Und wie wird der Typ einem Wert zugewiesen?". Sie wollten von Tippregeln hören, nicht von Box-and-Pointer-Diagrammen. Das Lachen war jedoch absolut unhöflich.
Gardenhead
10
Die lachende Person ist höchstwahrscheinlich ein Eiferer für eine bestimmte Sprache (Familie) mit einem starken Typensystem (Haskell scheint populär zu sein) und würde alles lächerlich machen, was weniger stark (und somit ein Spielzeug) ist oder stärker (und somit unpraktisch). oder einfach anders. Sich mit Zeloten zu unterhalten, ist gefährlich und vergeblich. So zu lachen ist einfach so unhöflich, dass es auf diese Art von tieferen Problemen hinweist. Sie haben Glück, dass sie nicht mit dem Predigen begonnen haben ...
Hyde

Antworten:

30

Das alles scheint eine gute Beschreibung dessen zu sein, was Typsysteme bieten. Und Ihre Implementierung klingt vernünftig genug für das, was sie tut.

Für einige Sprachen benötigen Sie die Laufzeitinformationen nicht, da Ihre Sprache keinen Laufzeitversand ausführt (oder Sie führen einen Einzelversand über vtables oder einen anderen Mechanismus durch, also benötigen Sie die Typinformationen nicht). In einigen Sprachen reicht es aus, nur ein Symbol / einen Platzhalter zu haben, da Sie sich nur um die Gleichheit der Typen kümmern, nicht um den Namen oder die Vererbung.

Abhängig von Ihrer Umgebung wünschte sich die Person möglicherweise mehr Formalismus in Ihrem Typensystem. Sie wollen wissen, was Sie damit beweisen können und nicht, was Programmierer damit machen können. Dies ist in der Wissenschaft leider ziemlich häufig. Obwohl Akademiker solche Dinge tun, weil es ziemlich leicht ist, Fehler in Ihrem Typensystem zu haben, die es den Dingen ermöglichen, sich der Korrektheit zu entziehen. Möglicherweise haben sie eine davon entdeckt.

Wenn Sie weitere Fragen hatten, ist Types and Programming Languages ( Typen und Programmiersprachen) das kanonische Buch zu diesem Thema und kann Ihnen helfen, einige der von Akademikern geforderten Konsequenzen sowie einige Begriffe zur Beschreibung der Dinge zu erlernen.

Telastyn
quelle
3
"Abhängig von Ihrer Umgebung wünschte sich die Person möglicherweise mehr Formalismus in Ihrem Typensystem." Das ist es wahrscheinlich. Ich habe mich nicht auf das konzentriert, was ich mit dem Typensystem beweisen kann, sondern als Werkzeug gedacht. Danke für die Buchempfehlung!
Mael
1
@Mael Einige Typsysteme werden als Logik verwendet (siehe logische Frameworks ). Der Typ gibt also im Grunde genommen die Formeln an und die Programme sind die Beweise für diese Formeln (z. B. kann der Funktionstyp a -> bals implizites b angesehen werden , dh wenn Sie mir einen Wert vom Typ geben, kann ich einen Wert vom Typ aerhalten b). Damit dies jedoch konsistent ist, muss die Sprache vollständig und damit nicht vollständig sein. Daher definieren alle Systeme des realen Typs eine inkonsistente Logik.
Bakuriu
20

Die Antwort von @ Telastyn gefällt mir besonders wegen des Hinweises auf das akademische Interesse am Formalismus.

Gestatten Sie mir, zur Diskussion beizutragen.

Was ist ein Typensystem?

Ein Typsystem ist ein Mechanismus zum Definieren, Erkennen und Verhindern von illegalen Programmzuständen. Es funktioniert durch Definieren und Anwenden von Einschränkungen. Die Einschränkungsdefinitionen sind Typen , und die Einschränkungsanwendungen sind Verwendungen von Typen , z. B. in der Variablendeklaration.

Typdefinitionen unterstützen normalerweise Kompositionsoperatoren (z. B. verschiedene Formen der Konjunktion, wie in Strukturen, Unterklassen und Disjunktionen, wie in Aufzählungen und Vereinigungen).

Die Einschränkungen, die Verwendung von Typen, ermöglichen manchmal auch Kompositionsoperatoren (z. B. zumindest dies, genau dies, entweder dies oder das, vorausgesetzt, dass etwas anderes zutrifft).

Wenn das Typensystem in der Sprache verfügbar ist und zur Kompilierungszeit angewendet wird, um Kompilierungsfehler ausgeben zu können, handelt es sich um ein statisches Typensystem. Diese verhindern, dass viele illegale Programme kompiliert werden, geschweige denn ausgeführt werden, und verhindern daher illegale Programmzustände.

(Ein statisches Typsystem verhindert, dass ein Programm ausgeführt wird, unabhängig davon, ob bekannt (oder unentscheidbar) ist, dass das Programm jemals den fehlerhaften Code erreicht, über den es sich beschwert. Ein statisches Typsystem erkennt bestimmte Arten von Unsinn (Verstöße gegen die angegebenen Einschränkungen). und beurteilt das Programm als fehlerhaft, bevor es jemals ausgeführt wird.)

Wenn ein Typsystem zur Laufzeit angewendet wird, handelt es sich um ein dynamisches Typsystem, das unzulässige Programmzustände verhindert. Dies geschieht jedoch, indem das Programm während der Ausführung angehalten wird, anstatt dass es überhaupt nicht ausgeführt wird.

Ein weit verbreitetes Systemangebot besteht darin, sowohl statische als auch dynamische Funktionen bereitzustellen.

Erik Eidt
quelle
Ich glaube nicht, dass sogenannte Hybridsysteme überhaupt sehr verbreitet sind. Welche Sprachen haben Sie im Sinn?
Gardenhead
2
@gardenhead, die Fähigkeit zum Downcast ist kein statisches Systemmerkmal, daher wird es normalerweise zur Laufzeit dynamisch überprüft.
Erik Eidt
1
@gardenhead: Die meisten statisch typisierten Sprachen ermöglichen es Ihnen, die Eingabe auf die Laufzeit zu verschieben, sei es einfach mit void *Cs (sehr schwachen) Zeigern, C # -Dynamikobjekten oder Haskells existenziell quantifizierten GADTs (die Ihnen eher stärkere Garantien bieten als die statisch typisierten Werte in den meisten anderen Sprachen).
Leftaroundabout
Stimmt, ich habe das "Casting" vergessen. Aber Gießen ist nur eine Krücke für ein schwaches Typensystem.
Gardenhead
@gardenhead Neben statischen Sprachen, die dynamische Optionen bieten, bieten viele dynamische Sprachen statische Typisierung. Beispielsweise verfügen Dart, Python und Hack über Modi oder Tools für die Durchführung statischer Analysen, die auf dem Konzept der "schrittweisen Typisierung" basieren.
IMSoP
14

Oh man, ich bin aufgeregt zu versuchen, diese Frage so gut wie möglich zu beantworten. Ich hoffe ich kann meine Gedanken richtig in Ordnung bringen.

Wie @Doval und der Fragesteller bereits erwähnt haben (wenn auch grob), verfügen Sie nicht wirklich über ein Typensystem. Sie haben ein System dynamischer Prüfungen mit Tags, das im Allgemeinen viel schwächer und auch viel weniger interessant ist.

Die Frage "Was ist ein Typensystem?" Kann durchaus philosophisch sein, und wir könnten ein Buch mit unterschiedlichen Standpunkten zu diesem Thema füllen. Da dies jedoch eine Website für Programmierer ist, werde ich versuchen, meine Antwort so praktisch wie möglich zu halten (und Typen sind wirklich äußerst praktisch in der Programmierung, trotz der Meinung einiger).

Überblick

Beginnen wir damit, dass wir verstehen, wozu ein Typensystem gut ist, bevor wir uns mit den formaleren Grundlagen befassen. Ein Typensystem gibt unseren Programmen Struktur . Sie sagen uns, wie wir verschiedene Funktionen und Ausdrücke miteinander verbinden können. Ohne Struktur sind Programme unhaltbar und äußerst komplex und können beim kleinsten Fehler des Programmierers Schaden anrichten.

Das Schreiben von Programmen mit einem Typensystem ist wie das Fahren einer Pflege in neuwertigem Zustand - die Bremsen funktionieren, die Türen schließen sicher, der Motor ist geölt usw. Das Schreiben von Programmen ohne Typensystem ist wie das Fahren eines Motorrads ohne Helm und mit Rädern aus Spaghetti. Sie haben absolut keine Kontrolle über Ihre.

Um die Diskussion zu Boden, lassen Sie uns sagen , dass wir eine Sprache mit wörtlichen Ausdruck haben num[n]und str[s]die repräsentieren die Zahl n und die Zeichenfolge s, bzw., und primitive Funktionen plusund concatmit der Bedeutung bestimmt. Natürlich möchten Sie nicht in der Lage sein, etwas wie plus "hello" "world"oder zu schreiben concat 2 4. Aber wie können wir das verhindern? Von vornherein gibt es keine Methode, um die Zahl 2 von der Zeichenfolgen-Literal-Welt zu unterscheiden. Wir möchten sagen, dass diese Ausdrücke in verschiedenen Zusammenhängen verwendet werden sollten. Sie haben verschiedene Typen.

Sprachen und Typen

Lassen Sie uns einen Schritt zurücktreten: Was ist eine Programmiersprache? Im Allgemeinen können wir eine Programmiersprache in zwei Ebenen unterteilen: die Syntax und die Semantik. Diese werden auch als Statik bzw. Dynamik bezeichnet. Es zeigt sich, dass das Typensystem notwendig ist, um die Wechselwirkung zwischen diesen beiden Teilen zu vermitteln.

Syntax

Ein Programm ist ein Baum. Lassen Sie sich nicht von den Textzeilen täuschen, die Sie auf einem Computer schreiben. Dies sind nur die lesbaren Darstellungen eines Programms. Das Programm selbst ist ein abstrakter Syntaxbaum . Zum Beispiel könnten wir in C schreiben:

int square(int x) { 
    return x * x;
 }

Das ist die konkrete Syntax für das Programm (Fragment). Die Baumdarstellung ist:

     function square
     /     |       \
   int   int x    return
                     |
                   times
                  /    \
                 x      x

Eine Programmiersprache stellt eine Grammatik bereit , die die gültigen Bäume dieser Sprache definiert (entweder konkrete oder abstrakte Syntax kann verwendet werden). Dies geschieht normalerweise mit einer BNF-Notation. Ich würde annehmen, dass Sie dies für die Sprache getan haben, die Sie erstellt haben.

Semantik

OK, wir wissen, was ein Programm ist, aber es ist nur eine statische Baumstruktur. Vermutlich möchten wir, dass unser Programm tatsächlich etwas berechnet . Wir brauchen Semantik.

Die Semantik der Programmiersprachen ist ein reiches Studiengebiet. Grundsätzlich gibt es zwei Ansätze: die Denotationssemantik und die Operationssemantik . Die Denotationssemantik beschreibt ein Programm, indem sie es in eine zugrunde liegende mathematische Struktur abbildet (z. B. die natürlichen Zahlen, stetigen Funktionen usw.). Das gibt unserem Programm einen Sinn. Die operative Semantik hingegen definiert ein Programm, indem sie dessen Ausführung detailliert beschreibt. Meiner Meinung nach ist die operationale Semantik für Programmierer (einschließlich meiner selbst) intuitiver. Bleiben wir also dabei.

Ich werde nicht näher auf die Definition einer formalen operativen Semantik eingehen (die Details sind ein bisschen kompliziert), aber im Grunde wollen wir Regeln wie die folgenden:

  1. num[n] ist ein Wert
  2. str[s] ist ein Wert
  3. Wenn num[n1]und num[n2]zu den ganzen Zahlen n_1$ and $n_2$, thenplus (num [n1], num [n2]) `ausgewertet wird, ergibt sich die ganze Zahl $ n_1 + n_2 $.
  4. Wenn str[s1]und str[s2]zu den Zeichenfolgen s1 und s2 concat(str[s1], str[s2])ausgewertet wird, wird zu der Zeichenfolge s1s2 ausgewertet.

Die Regeln sind in der Praxis viel formeller, aber Sie verstehen das Wesentliche. Wir stoßen jedoch bald auf ein Problem. Was passiert, wenn wir folgendes schreiben:

concat(num[5], str[hello])

Hm. Das ist ein ziemliches Rätsel. Wir haben nirgendwo eine Regel definiert, wie eine Zahl mit einer Zeichenfolge verkettet werden soll. Wir könnten versuchen, eine solche Regel zu erstellen, aber wir wissen intuitiv, dass diese Operation bedeutungslos ist. Wir wollen nicht, dass dieses Programm gültig ist. Und so werden wir unaufhaltsam zu Typen geführt.

Typen

Ein Programm ist ein Baum, wie er durch die Grammatik einer Sprache definiert ist. Programmen wird durch Ausführungsregeln eine Bedeutung gegeben. Einige Programme können jedoch nicht ausgeführt werden. Das heißt, einige Programme sind bedeutungslos . Diese Programme sind falsch geschrieben. Tippen kennzeichnet also sinnvolle Programme in einer Sprache. Wenn ein Programm gut typisiert ist, können wir es ausführen.

Nennen wir einige Beispiele. Wie bei den Bewertungsregeln werde ich auch hier die Schreibregeln informell präsentieren, aber sie können rigoros gestaltet werden. Hier sind einige Regeln:

  1. Ein Token des Formulars num[n]hat einen Typ nat.
  2. Ein Token des Formulars str[s]hat einen Typ str.
  3. Wenn expression e1den Typ natund expression e2den Typ hat nat, hat der Ausdruck plus(e1, e2)den Typ nat.
  4. Wenn expression e1den Typ strund expression e2den Typ hat str, hat expression concat(e1, e2)den Typ str.

Nach diesen Regeln gibt es plus(num[5], num[2])also einen Typ nat, dem wir jedoch keinen Typ zuweisen können plus(num[5], str["hello"]). Wir sagen, dass ein Programm (oder Ausdruck) gut typisiert ist, wenn wir ihm einen beliebigen Typ zuweisen können, und dass es ansonsten schlecht typisiert ist. Ein Typensystem ist gesund, wenn alle gut getippten Programme ausgeführt werden können. Haskell ist gesund; C ist nicht.

Fazit

Es gibt andere Ansichten zu Typen. Typen entsprechen in gewisser Weise der intuitionistischen Logik und können in der Kategorietheorie auch als Objekte angesehen werden. Das Verständnis dieser Zusammenhänge ist faszinierend, aber nicht unbedingt erforderlich, wenn man lediglich eine Programmiersprache schreiben oder sogar entwerfen möchte. Das Verstehen von Typen als Werkzeug zur Steuerung von Programmformationen ist jedoch für das Entwerfen und Entwickeln von Programmiersprachen von wesentlicher Bedeutung. Ich habe nur die Oberfläche zerkratzt, was Typen ausdrücken können. Ich hoffe, Sie denken, dass sie es wert sind, in Ihre Sprache aufgenommen zu werden.

Gartenkopf
quelle
4
+1. Der größte Trick, den die Enthusiasten für dynamisches Tippen jemals gemacht haben, war, die Welt davon zu überzeugen, dass man "Typen" ohne ein Typensystem haben könnte. :-)
Ruakh
1
Da Sie nichts Interessantes für beliebige Programme automatisch überprüfen können , muss jedes Typsystem einen Besetzungsoperator (oder das moralische Äquivalent) enthalten, da es sonst die Vollständigkeit opfert. Dazu gehört natürlich auch Haskell .
Kevin
1
@ Kevin Ich kenne den Satz von Rice sehr gut, aber er ist nicht so relevant, wie Sie vielleicht denken. Zunächst erfordert eine große Mehrheit der Programme keine uneingeschränkte Rekursion. Wenn wir in einer Sprache arbeiten, die nur primitive Rekursionen enthält, wie beispielsweise Gödels System T, können wir interessante Eigenschaften mithilfe eines Typsystems überprüfen, einschließlich Anhalten. Die meisten Programme in der realen Welt sind ziemlich einfach - ich kann mir nicht vorstellen, wann ich das letzte Mal wirklich Casting brauchte. Die Vollständigkeit der Angaben wird überbewertet.
Gardenhead
9
"Dynamisches Tippen ist nicht wirklich Tippen" kam mir immer so vor, als ob klassische Musiker sagten: "Popmusik ist nicht wirklich Musik", oder Evangelikale sagten: "Katholiken sind nicht wirklich Christen". Ja, statische Typsysteme sind leistungsfähig und faszinierend und wichtig, und dynamisches Tippen ist etwas anderes. Aber (wie andere Antworten beschreiben) es gibt eine Reihe nützlicher Dinge, die über statische Typsysteme hinausgehen und die traditionell als Typisierung bezeichnet werden und alle wichtige Gemeinsamkeiten aufweisen. Warum müssen wir darauf bestehen, dass unsere Art des Tippens die einzig wahre ist?
Peter LeFanu Lumsdaine
5
@IMSoP: Für etwas, das kürzer als ein Buch ist, Chris Smiths Aufsatz Was Sie wissen müssen, bevor Sie über Schriftsysteme debattieren, ist großartig. Er erklärt, warum dynamisches Tippen wirklich etwas ganz anderes ist als statisches Tippen.
Peter LeFanu Lumsdaine