Wie sollte man die Notation von Typsystemen lesen?

• Dieser Artikel bietet eine ausführliche Erklärung dazu, wie man die Notation von Typsystemen in Programmiersprachen liest und versteht.
• Die Notation von Typsystemen ist ein mathematischer Ausdruck, der in Artikeln oder wissenschaftlichen Arbeiten über Typsysteme verwendet wird.
• Die zur Beschreibung von Typsystemen verwendete Notation unterscheidet sich je nach Darstellung, doch die meisten Darstellungen teilen viele gemeinsame Elemente.
• Ein auf eine Programmiersprache angewandtes Typsystem ist ein syntaktisches System, also eine Menge von Regeln, die auf die Syntax einer Programmiersprache wirken.
• Diese Notation hat ihren Ursprung in der formalen Logik und wird verwendet, um formale Beweise über Eigenschaften eines Systems zu konstruieren.
• Der Artikel behandelt außerdem die Konzepte von Relationen, Urteilen, Axiomen und Inferenzregeln in der Notation von Typsystemen.
• Eine Typisierungsrelation wird üblicherweise als e:τ geschrieben und kann als „e hat den Typ τ“ gelesen werden.
• Ein Typisierungsurteil wird mit der Notation ⊢e:τ⊢ geschrieben, wobei ⊢ als „die folgende Aussage ist wahr“ gelesen werden kann.
• Der Artikel erklärt außerdem ausführlich die Konzepte von Variablen, Kontext und Umgebung in der Notation von Typsystemen.
• Der Kontext oder die Typumgebung wird in der Notation als Γ dargestellt.
• Der Artikel behandelt außerdem weitere gebräuchliche Notationen und Überlegungen wie das Layout von Inferenzregeln, Nebenbedingungen, Subtyping, mehrere Kontexte und bidirektionales Type Checking.
• Dieser Artikel ist ein umfassender Leitfaden zum Verständnis der Notation von Typsystemen, insbesondere für Menschen, die mit diesem Konzept noch nicht vertraut sind.

[GN⁺]

Hacker-News-Kommentar

• Diskussion über die Notation von Typsystemen in Informatik-Publikationen, mit grundlegenden Erklärungen zu BNF-Notation, Inferenzregeln usw.
• Die Ursprünge der Notation lassen sich bis zu Frege zurückverfolgen; das Turnstile-Symbol und horizontale Linien sind dabei zentrale Elemente
• Obwohl sie Informatik studiert haben, empfinden einige Leser |- und |=, sowie die metasyntaktische Bedeutung der verwendeten Variablen, als verwirrend
• Die Erklärung wird geschätzt, aber einige Leser fragen sich, warum sie auf Stack Exchange geschrieben wurde und nicht auf einer anderen Plattform wie lexi-lambda.github.io
• Benjamin C. Pierces "Types and Programming Languages" wird als gutes Lehrbuch empfohlen, das diese Inhalte behandelt
• Einige Leser haben sich jahrelang für dieses Thema interessiert, wussten aber nicht, wie sie den Einstieg finden sollten
• Das Ada Reference Manual wird als praktisches Beispiel für die Verwendung dieser Art von Syntax erwähnt
• Lob für eine Antwort, die bei den Grundlagen beginnt und darauf aufbaut
• 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 ist in den meisten Sprachen unsinnig, aber in Python ist True + 2 tatsächlich eine Ganzzahl und entspricht 3