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

2025-07-03, read count: 1, page: 23 ~ 39, pages read: 17

第 4 章 逐次実行と変数定義 関数の型の続き。 TAPL の単純な拡張の中の派生形式・ let 束縛に相当する。 本書では TAPL にならい変数の再定義を許す。 shadowing は同一 block での再定義を禁じて下位 block で許可するやつ。 逐次実行と変数定義の AST が再帰的なのは ML 風で配列での実装もできる。 ここまでで作った型システムは必ず停止する正規化可能性が保証されるので、発散コンビネータ・ omega のようなコードは書けない。 また前方参照は許可していない。 型設計として発生しうるパターンでも parser で生成しないようにしてるってのはちょっと目からウロコ。実装の簡便さのためかな。

2025-07-04, read count: 1, page: 40 ~ 56, pages read: 17

第 5 章 オブジェクト型 ここで対応するのは構造体とか record と呼ばれる複数の値にラベルをつけてまとめるデータ型。 TAPL の単純な拡張の中のレコードに相当する。 なので AST でオブジェクト生成の構文は複数の値を持てるように定義する。 record の実装自体は難しくない。 等価判定の時間計算量が気になったけど今気にするところじゃないのかな。 variant のひとつ union を実装するのは TAPL の範囲を超えてしまい難しいが、 TypeScript の tagged union ならまだましなので演習問題ではそれに挑戦するようになってる(それでも難しい)。 なるほど読み終えてから見直してみるかあ。

2025-07-05, read count: 1, page: 57 ~ 67, pages read: 11

第 6 章 再帰関数 本書の再帰関数は ML 流の型推論の実装が難しいので戻り値の型を明示する。そのため宣言文も専用のものを用意する。 TAPL の単純な拡張の中の一般的再帰に相当する。 型検査器では戻り値の型の検査、また後続処理では再帰関数自身のみを含む型環境での型検査を行う。 このような特別な構文を用いなくても不動点コンビネータ(発散コンビネータの発展型)を利用すれば再帰関数が書ける。 ここで特別な構文を用いたのは抽象度が上がって説明が難しくなるためとのこと。 章の内容はわかったが用語がわからんの後追いで勉強が必要だわ。

2025-07-06, read count: 1, page: 68 ~ 78, pages read: 11

第 7 章 部分型付け TAPL の部分型付けと部分型付けのメタ理論の一部に相当する。 TypeScript でできるような部分型付け(subtyping) という型システムの拡張。 この章ではオブジェクト型の部分型付けを実装するが、文脈によっては異なる型の間や関数の型の部分型付けも可能。 型の代入可能性、共変(covariant)と反変(contravariant)の概念。 条件演算子の型を実装すると join(型の結び)・ meet(型の交わり) で実装が冗長になるので本書は除外。 variance support の波が F# に迫って来そうなので共変・反変ちゃんと覚えようと思ってたらこんなところでばったり出会うとは。

2025-07-07, read count: 1, page: 79 ~ 91, pages read: 13

第 8 章 再帰型 木構造や無限リストのような再帰的なデータ構造を定義するための型。 本書では TAPL の流儀で形式的な表現に置き換える方法で実装をする。 実際にはわかりやすい型エラーのために型エイリアスの遅延評価のような実装の方が採用されることが多い。 本書では型エイリアスの AST への追加は省略。 parser が必要とする箇所に直に埋め込んでくる。 型の定義は型変数と再帰型を追加。面倒さがわかるほど解像度ないのであとで勉強が必要やな。 空腹関数は F# では DU が必要やが TypeScript は直でいけるのか。

2025-07-08, read count: 1, page: 92 ~ 101, pages read: 10

本書の再帰化型の型検査器の実装では、再帰型のデータ型の展開前後が一致していれば OK とする必要がある。 等価判定では型変数の名前の違いは無視し、また無限に再帰しないように、比較中の型変数を覚えておく必要がある。 TAPL の再帰型には同型再帰と同値再帰があり、本書では TypeScript でも採用されている同値再帰を実装した。 同型再帰の方がユーザに注釈を求める代わりに循環検出の実装が不要になると。 また同値再帰は発展的な言語機能との相性の悪さから ML 系では同型再帰が採用されているらしい。 まだぼんやりとしかわからんがキーワードは覚えた。

2025-07-09, read count: 1, page: 101 ~ 116, pages read: 16

第 9 章 ジェネリクス ジェネリクス(総称型)の同期は異なる型に対して同じ処理をさせる再利用。 ジェネリクスの実装でも型変数を使用する。再帰型のときは再帰型自身で、ジェネリクスではユーザが指定した型で置き換える。 TAPL では、型変数を用いた抽象化を型抽象、型変数を具体化することを型適用と呼ぶ。 ジェネリクスの実装は複雑。 Java や Go が当初はジェネリクスをサポートしていなかった理由では？とのこと。 次 TypeScript のジェネリクスを紐解くところがひとまとまりなのでここで終えておく。

2025-07-10, read count: 1, page: 117 ~ 121, pages read: 5

TypeScript のジェネリクスを紐解く。 型抽象された形を持つ関数に具体的な型を与えることはできない。 型抽象された型は型変数の名前が違っていても一貫して読み替えできるなら同じ型として扱える。 これは変数捕獲のために型変数の名前の衝突を避けるため。 型変数も shadowing の対象となる。型変数を具体的な型ですべて置き換えることを型代入という。 あと型適用が実行時には全く影響しないという話。 例のコードを " ... " | deno run --check - で検査しながらじゃないと理解が危なかった。 実行時に～は deno で interactive に検査せずやればいい。

2025-07-11, read count: 1, page: 121 ~ 130, pages read: 10

型抽象と型変数を型と構文木に追加する。型抽象では型変数と本体の型を持つ。 TypeScript では型抽象が無名関数の一部として実装されているが、本書は TAPL 流で任意の項に型抽象を書ける。 TypeScript 4.7 で型適用構文が導入されたが、実質的に型適用も関数呼び出しの一部になっている。 ここまでの型代入の実装は間違ってて先で直すらしい。理解が浅いから復習が必要やな。 章のはじめに複雑だといってた通りか、本書の中でも実装量多いな。

2025-07-12, read count: 1, page: 131 ~ 140, pages read: 10

型検査器の実装。 型抽象と型適用に該当する処理を追加するだけだが、 shadowing が正しく扱われない問題と変数捕獲による問題のコーナーケースに対応する必要がある。 それらの問題はこれまでで敢えて間違った実装をしていた型適用に関する部分。 変数捕獲に於いては型変数の名前が衝突しないようにするため全く新しい名前を与える。これはフレッシュな変数と呼ばれる。 ここまでの内容が TAPL の全称型に相当する。 TAPL では有界量化の章で全称型と部分型を組み合わせ、指定した型の部分型なら置き換え可能な制約付きの型変数を導入している。これが TypeScript の extends に相当する。 難しいね。何度か練習しないと一回ではピンとこんな。

2025-07-13, read count: 1, page: 140 ~ 154, pages read: 15

おわりに、演習問題の解答、参考文献、索引。 型システムは型付け規則の集合で、その規則を機械的に判定できるようプログラムにしたのが型検査器といえる。 型システムは証明のしやすさに念頭を置いて作られるので、型検査器で実装しやすくないものもあり、どの規則を選ぶべきかという問題を考える必要がある。 次の step は TAPL に挑戦する、 TypeScript の漸進的型付けの論文を読む、自身を解析できる型解析器を作るとか。 型システムではある型を作る・使う構文を型理論の背景にある論理学の用語からそれぞれ導入形式・除去形式と呼ぶ事がある。 TAPL の Curry-Howard 対応参照。 これで終わり。ページ数少ないしサクサク読めた。でも parser を実装してないのもあって頭の中を素通りしてる箇所もあろうし、まるっと自分で書いてみる必要ありそうかなあ。 一度で習得できたらかっこいいけど中々な。

2025-07-14, read count: 1, page: 155 ~ 173, pages read: 19