Booklog - 型システムのしくみ TypeScript で実装しながら学ぶ型とプログラミング言語

型システムの背景にある数学的に証明された理論を小型の型検査器を実装して体感し、型システムを学ぶためのきっかけを作るのが本書の目的。 ステップとしては本書 → TAPL(Types and Programming Languages) → TypeScript の型システム(Gradual Typing)。 第 1 章 型システムとは、プログラムの未定義動作に対処する手段の一つ。 プログラムを操作的意味論で定義し、型検査器が OK と判定したプログラムは未定義動作を起こさない性質、型安全性が証明される。 型安全性を意識した型システムが設計された OCaml や Haskell と違い、 TypeScript は JavaScript に後付で型システムが導入されているため、 JavaScript としては未定義動作がない。このため型安全性はそれほど重要視されてない様子。 TAPL 積読状態なので、まずは本書を読み進めていく。

2025-07-01, read count: 1, page: i ~ ix, 1 ~ 7, pages read: 16

第 2 章 真偽値の型と数値の型 まず真偽値と数値のリテラル、条件・加算の演算子を持つ言語を作る。 TAPL の型無算術式・型付き算術式に相当する。 型検査器の判定基準と抽象構文木(Abstract Syntax Tree)の設計。 プログラムを読み込んで AST を生成するパーサーの実装。 型検査器を実装して動かす。エラー時の挙動もここで決める。 TypeScript での実装なので型と AST は discriminated union での実装になってる。 TypeScript が OK/NG にした設計意図の話も面白い。

2025-07-02, read count: 1, page: 8 ~ 22, pages read: 15

第 3 章 関数型 関数の型の実装。この章は変数参照・無名関数・関数呼び出しをやる。 変数参照では定義済み変数を管理する型環境(型付け文脈)を実装する。型環境に見つからない＝未定義変数のエラー。 型環境を更新する際は破壊的更新を行うと静的スコープ外の変数が参照できてしまうので、非破壊的更新を行う。 関数の型の等価判定で仮引数の名前を比較すると仮引数の名前が違う実引数を渡せなくなるので、この実装では比較しない。 argument 実引数と parameter 仮引数の使い分けの経緯おもしろ。

2025-07-03, read count: 1, page: 23 ~ 37, pages read: 15