型システム記法はどのように読めばよいのか？

• この記事は、プログラミング言語における型システム記法を読み、理解する方法についての詳細な説明です。
• 型システム記法は、型システムに関する記事や論文で使われる数学的表現です。
• 型システムを説明するために使われる記法は発表ごとに異なりますが、ほとんどの発表は多くの共通部分を共有しています。
• プログラミング言語に適用される型システムは構文システムであり、プログラミング言語の構文に作用する規則の集合です。
• この記法は形式論理に由来し、システムの性質に関する形式的証明を構成するために使われます。
• この記事はまた、型システム記法における関係、判断、公理、推論規則の概念について議論します。
• 型付け関係は通常 e:τ と書かれ、「e は型 τ を持つ」と読むことができます。
• 型付け判断は ⊢e:τ⊢ 記法を使って書かれ、ここで ⊢ は「次の文が真である」を意味するものとして読むことができます。
• この記事はまた、型システム記法における変数、コンテキスト、環境の概念についても詳しく説明します。
• コンテキストまたは型環境は、記法では Γ で表されます。
• この記事はまた、推論規則のレイアウト、サイド条件、サブタイピング、複数コンテキスト、双方向型検査のような、ほかの一般的な記法や考慮事項も扱います。
• この記事は、型システム記法を理解するための総合的なガイドであり、特にこの概念に初めて触れる人に向けたものです。

[GN⁺]

Hacker Newsの意見

• コンピュータサイエンスの論文における型システム記法についての議論で、BNF記法や推論規則などの基礎説明
• 記法の起源はFregeまでさかのぼれ、回転ドアのような記号と水平線が中核要素
• コンピュータサイエンス専攻であっても、一部の読者は |- と |=、そして使われている変数のメタ構文レベルの意味を紛らわしく感じる
• 説明には感謝しているが、一部の読者はなぜこれがStack Exchangeで書かれ、別のプラットフォームである lexi-lambda.github.io では書かれなかったのか疑問に思っている
• Benjamin C. Pierceの "Types and Programming Languages" はこの種の内容を扱う良い教科書として推薦されている
• この主題について何年も気になっていたが、どう取り組めばよいかわからなかったという読者もいる
• Ada Reference Manual がこの種の構文の実用的な使用例として言及されている
• 基本的なところから始めて発展させていく回答への称賛
• 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 はほとんどの言語では無意味だが、Pythonでは True + 2 が実際に整数であり、3に等しいことが例として挙げられている