第 3 課：貢献の振り返りと型判断 Γ ⊢ t : T
一言でいえば：この論文の目標は、「コンポーネントを実行時に動的にマウントし、きれいにアンマウントする」ということを推論可能かつ検証可能にすることです。本課ではまず論文の全体地図を見ます——4 つの貢献がそれぞれどの 2 種類の合成可能性を支えているのか。そして小さな土台を 2 つ補います：型判断
Γ ⊢ t : Tがいったい何を言っているのか、そして作用注釈T^effectがなぜ「実装を見ずに副作用が分かる」ようにしてくれるのか。
1. 論文の 4 つの貢献：まず全体地図を見る
論文の 1.3 節は、4 つの貢献を一気に提示しています。それらは単なる「4 つの成果」ではなく、以後すべての課の目次でもあります：
| 貢献 | 論文の節 | 中核となる仕組み（一言） | たとえ話 | どの合成可能性を支えるか |
|---|---|---|---|---|
| 1. 可逆的な作用 | 3.1 | 「環境を変更する」すべての操作に、追跡と復元を備えた明示的な逆操作をペアにする | 全行程を録画し、いつでも巻き戻せる | 時間的合成可能性 |
| 2. リアクティブな余作用 | 3.2 | コンポーネントは依存集合で自分が必要とするものを宣言し、環境が変わると自動的に通知される：活性化・非活性化・中立 | コンセントが自動で通電・停電する | 空間的合成可能性 |
| 3. コンポーネントライフサイクル + 統一コンテキスト型 | 3.3 / 3.4 | 「マウント→実行→アンマウント」の全過程を操作化し、作用コンテキストと余作用コンテキストを 1 つの型に統合する | プラグインに戸籍を与え、生まれてから死ぬまで登録する | 2 つの次元を 1 つのプログラミングパラダイムに統一 |
| 4. Cordis の実装 + Koishi の事例 | 4 | 時空合成可能性のメタフレームワークを実現：作用の追跡、余作用の解決、宣言的コンポーネントローダー。Koishi エコシステムの 4000 以上のプロダクションプラグインで検証済み | 設計図から量産へ、さらに組み立てラインにも乗せた | 理論全体が実現可能であることを証明 |
分解して見ると、4 つの貢献は 1 本の連鎖になっています：
まず「マウントできてアンマウントできる」を解決し（貢献 1、時間次元）、次に「安定して立つ」を解決し（貢献 2、空間次元）、両者を 1 つの統一モデルに収め（貢献 3、プログラミングパラダイム）、実際のフレームワークとして書き上げてエコシステムで検証する（貢献 4、実装）。
🎁 たとえ話：プラグインはホストに差し込む「USB メモリ」のようなものです——貢献 1 は「抜いた後もシステムが元通りである」こと、貢献 2 は「差し込んだ後、必要なドライバーを自動で見つける」こと、貢献 3 は「USB メモリの使用周期全体が規範的に管理される」ことを担い、貢献 4 は「ホットプラグ対応のコンピューターを実際に作り上げた」ということです。
💡 以後の課では 1 つずつ展開していきます：第 6 課で可逆的な作用、第 8 課でリアクティブな余作用、第 9 課でライフサイクル、第 10 課で統一コンテキスト型、第 11〜12 課で Cordis コアライブラリと Koishi の事例を扱います。本課ではまずこの地図を壁に貼っておきます。
2. 型判断 Γ ⊢ t : T とは何か？
論文の第 2 章は冒頭で、読者が基本的な型理論と圏論に精通していることを前提とすると述べています。慌てないでください——本課で必要なのはたった 1 つの概念だけです：**型判断（typing judgment）**です。これは少しも神秘的なものではなく、あなたが TypeScript で毎日経験していることを、数学記号の書き方に置き換えたものにすぎません。（圏論については、第 4 課でモナドを扱う際に最も素朴な形で紹介します。）
単純型付きラムダ計算（STLC）には、数式のように見える記法があります：
Γ ⊢ t : T
読み上げれば一文になります：「型環境 Γ の下で、項 t は型 T を持つ。」 記号を 1 つずつ分解すると：
| 記号 | 読み方 | 意味 | TypeScript でのたとえ |
|---|---|---|---|
| Γ | ガンマ（Gamma） | コンテキスト / 型環境：「変数名 → 型」の対応表 | 現在のスコープでコンパイラーが記録している宣言（例えば const x: number = 5 という行） |
| t | 項（term） | いま検査されているコード片 / 式 | 関数本体内のある式 |
| T | 型（type） | 項の型 | number、string のような型 |
| ⊢ | ターンスティル（turnstile） | 左辺と右辺を結びつける判断関係 | コンパイラーが「決定を下す」その瞬間：x + 1 が number であることを確認する |
TypeScript と対応づければ、完全に理解できます：
const x: number = 5;
const y = x + 1; // コンパイラー：x は number なので、x + 1 も number
コンパイラーが 2 行目を検査するとき、その頭の中には「x : number」という小さな表があります——この表が Γ です。検査している式 x + 1 が t で、導き出した結論「型は number」が T です。型判断とは、「表を引く + 検証する + 結論を下す」という一連の動作全体の形式的な書き方にすぎません。
⚠️ Γ の読み方に注意：これはギリシャ文字の大文字「ガンマ」であり、英字の G ではありません。論文では常に「現在のスコープで何が分かっているか」を表します。
3. 作用注釈 T^effect：型に「副作用」を記憶させる
通常の型判断 Γ ⊢ t : T が答えるのは 1 つの質問だけです：t は何を返すか。しかし実際のプログラムでは、関数は結果を返すだけでなく、外の世界に触れることもあります——ファイルを読む、データベースに書き込む、グローバル変数を変更する、ネットワークリクエストを送る。これらが副作用です。
作用システム（effect system）は型を細分化します：型の上に作用注釈を付け加えて、次のようにします：
Γ ⊢ t : T^effect
追加された effect は、2 つ目の質問に答えます：t は T を返す以外に、どんな副作用を生じさせるか。これは適当に書いたラベルではなく、「作用代数」の一要素です——作用は合成でき、比較もでき、和集合が取れる集合のようなものです。古典的な例：
Maybe作用：失敗する可能性がある（部分性）State作用：可変な状態IO作用：外部世界とのやり取り（ファイル読み取り、ネットワーク）
💡 論文ではこの歴史が紹介されています：作用注釈のアイデアは Lucassen と Gifford に端を発し、モナドによるモデリングは Moggi によるもので Wadler が Haskell で広め、代数学的作用は Plotkin と Power によるものです。本課で覚えておくべきことは 1 つだけ：作用注釈 = 型レベルの「副作用説明書」。
なぜこれが「合成的推論」を支えるのか？
合成的推論（compositional reasoning）は、この一節で最も価値のある 2 語です。その意味は：合成された式の性質を判断するには、各部分の性質を見るだけでよく、その実装を見る必要はないということです。
具体例を挙げましょう。2 つの関数があるとします：
// f：ファイルを読む（IO 作用を持つ）
// g：純粋関数、算術だけを行う（副作用なし）
// では f(g(x)) はどんな作用を持つか？——IO。
// f と g のソースを読む必要はなく、注釈だけを見れば断定できる。
推論過程は一文で済みます：外側の f は IO を持ち、内側の g は純粋で、副作用は空から消えたりしないので、f(g(x)) 全体には必ず IO があります。
なぜこれが重要なのか？ 実際のコードベースは数十万行に及ぶことが珍しくないからです。作用注釈がなければ、ある関数がこっそりグローバル変数を変更しているかどうかを知るには、その実装を最初から最後まで読むしかありません——しかもそれが呼び出すすべての関数も連れて読む羽目になります。注釈があれば、副作用も型と同じように「局所的に検査」できます：すべての関数が説明書を持ち、合成するときは説明書をつなぎ合わせるだけです。
🎁 たとえ話：通常の型は「出前の注文票に書かれた料理名」（あなたが何を注文したか）のようなもので、作用注釈は「アレルゲン一覧」（その料理に含まれる、あなたが食べられないもの）のようなものです。テーブルいっぱいの料理を組み合わせるとき、各料理のアレルゲン一覧をつなぎ合わせるだけで、全体が食べられるかどうかが分かります——厨房に入って調理過程を見る必要はありません。
4. 作用と余作用を 2 つの次元に対応させる
論文 1.3 節の冒頭の一文が、論文全体の鍵です：
動的合成可能性の 2 つの次元は、それぞれ計算がどのように環境を変更するか、および計算がどのように環境に依存するかに関わる。
- 作用 = 「計算が環境を変更したもの」に答える（私が何を変えたか）
- 余作用（coeffect） = 「計算が環境に提供してもらう必要のあるもの」に答える（私が必要とするもの）
2 つの方向はちょうど正反対で、次の図はそれらを一緒に描いたものです：
效应问「我改了什么」（对世界的影响）；余效应问「我需要什么」（世界对我的约束）
伝統的には、作用も余作用も字句的に固定されたスコープ内でコンパイル時に静的解析するしかありませんでした——つまり、コンパイラーはコードを開けばすべてを見ることができ、すべてがコードを書いた時点で決まっていたからです。しかし Cordis のシナリオはコンポーネントが実行時に動的に参加・退出するものです：実行時にまだ何が読み込まれるかは誰にも分かりません。そこで論文は両者を 1 段階ずつ格上げしました：
| 次元 | 問うこと | 従来のツール | 論文の格上げ | たとえ話 |
|---|---|---|---|---|
| 時間 | 計算が環境をどう変更するか | 作用（コンパイル時の静的解析） | 可逆的な作用：すべての変更に明示的な逆操作をペアにし、実行時に本当に取り消せる | 録画を巻き戻せる、プラグインを抜いても痕跡を残さない |
| 空間 | 計算が環境にどう依存するか | 余作用（コンパイル時の静的解析） | リアクティブな余作用：依存集合 + 充足通知により、自動的に活性化・非活性化・中立になる | コンセントは通電すれば動き、停電すれば待機する |
ここまでで、4 つの貢献と 2 つの次元がループを閉じます：
- 貢献 1（可逆的な作用） → 時間的合成可能性：コンポーネントは一生「環境を変更」し続けるので、変更した後は元に戻せなければならない。
- 貢献 2（リアクティブな余作用） → 空間的合成可能性：コンポーネントは依存グラフの中に立っており、依存が揃っているかどうかを感知できなければならない。
- 貢献 3（ライフサイクル + 統一コンテキスト型） → この 2 つの次元を 1 つのプログラミングモデルに練り込む。
- 貢献 4（Cordis + Koishi） → この仕組みが本当に動くことを証明する。
5. 要点の振り返り
この課の内容を 5 文に凝縮すると：
- 4 つの貢献は 1 本の連鎖：可逆的な作用→時間的合成可能性。リアクティブな余作用→空間的合成可能性。ライフサイクル + 統一コンテキスト型→プログラミングパラダイム。Cordis + Koishi→実装による検証。
Γ ⊢ t : T= 「型環境 Γ の下で、項 t は型 T を持つ」。Γ は「変数名 → 型」のスコープ表であり、TypeScript コンパイラーが頭の中に持っている表と同じものです。- 作用注釈
T^effectは、型を「返り値だけを記録する」ものから「副作用も記録する」ものへと格上げします。 - 作用注釈の価値は合成的推論：f が IO を持ち、g が純粋だと分かれば、
f(g(x))が IO を持つと断定できます——実装を読む必要はありません。 - 2 つの次元、2 つの方向：作用 = 環境の変更 = 時間。余作用 = 環境への依存 = 空間。Cordis はこれらを「コンパイル時の静的解析」から「実行時の動的メカニズム」へと格上げしました。
🚀 次の課ではモナドを扱います——この節で出てきた IO、State、Maybe を覚えていますか？ これらはすべてモナドのインスタンスです。作用注釈は「型レベルの宣言」で、モナドは「実行時レベルの箱」であり、両者は同じものの 2 つの顔です。
セルフチェック · 貢献と型判断
回答を終えたら「解答を送信」をクリックすると、正誤と解説を確認できます。