idris2-elab

name	idris2-elab
description	Idris2 Elaborator Reflection — Elabモナド、runIO、依存型、%language ElabReflection、OOM対策
triggers	["ElabReflection","%language ElabReflection","Elab monad","Elabモナド","elaborator reflection","runIO","dependent types","依存型","type-level programming","型レベルプログラミング","Elab"]

Idris2 Elaborator Reflection スキル

分類: Project Skill 対象: Idris2プロジェクト全般（a-life、TheWorld、TextDAO等） 目的: Elabモナド、runIO、依存型の正しい理解とOOM対策

---

Idris 2 Elab（エラボレータ・リフレクション）教科書

この教科書の目的

Elabは「なんかすごいメタプログラミング機能」として紹介されがちだが、本質を理解しないまま使うと、できないことをやろうとして時間を溶かす。この教科書はElabが何であり、何でないかを、嘘なく伝えることを目的とする。

---

第1章：Elabの正体 —— コンパイラの中に住む小人

1.1 普通のプログラムとElabプログラムの違い

普通のIdris 2プログラムは、あなたが書いて、コンパイラが検査し、ユーザーが実行する。

あなた → コードを書く → コンパイラが型検査 → バイナリ生成 → ユーザーが実行

Elabプログラムは、あなたが書いて、コンパイラが実行する。ユーザーの手に届くことはない。

あなた → Elabスクリプトを書く → コンパイラが実行 → コードや型が生成される → 通常の型検査 → バイナリ生成

Elabはコンパイラの中に住んでいて、コンパイルが終わると死ぬ。

1.2 コンパイラは何をしているのか

Elabを理解するには、まずコンパイラが裏で何をしているか知る必要がある。

あなたがこう書いたとする：

the (Vect 3 Int) [1, 2, 3]

コンパイラは裏で大量の作業をしている：

1. [1, 2, 3] は糖衣構文。1 :: 2 :: 3 :: Nil に展開する
2. Nil の型は Vect 0 Int。3 :: Nil で Vect 1 Int。繰り返して Vect 3 Int
3. 各 :: の暗黙引数（長さ n や要素型 a）を推論する
4. 推論した値を穴に埋める ← これが単一化（Unification）
5. 最終的な型が Vect 3 Int と一致するか確認

この1〜5の作業がエラボレーション（Elaboration）。あなたが書いた「人間に優しい表面言語」を、コンパイラが扱える「厳密なコア言語（TT）」に翻訳するプロセスだ。

1.3 Elabモナドとは

Elabモナドは、上記の1〜5の操作を、あなたが手動でスクリプトとして書ける仕組み。

普通：コンパイラが暗黙にやる Elab：あなたが明示的に命令する

-- 普通：コンパイラに任せる
myFunc : Nat -> Nat
myFunc x = x + 1

-- Elab：自分で項を組み立てる
%runElab do
  -- 「Nat -> Nat 型の関数を作れ」と命令
  -- 「引数を受け取り、1を足す項を構築しろ」と命令
  -- コンパイラが従い、関数を生成する

つまりElabは**「コンパイラへの命令書」を書くための言語**。

---

第2章：Elabモナドの中身 —— 何ができるのか

2.1 基本操作一覧

Elabモナド内で使える主な操作：

操作	やること	例え
check	項の型検査	「この封筒のラベルは正しいか？」
goal	今埋めるべき穴の型を取得	「次に何を作ればいいか教えて」
fill	穴に項を埋める	「この穴にはこの値を入れろ」
unify	二つの項を同じにする代入を見つける	「AとBを一致させる方法を探せ」
declare	新しい定義を作る	「こういう関数を作れ」
search	型に合う値を自動探索	「この型を満たす項を勝手に見つけろ」

2.2 最小限の例：自動的にインターフェースを導出する

最も実用的なElab用途は「退屈なコードの自動生成」。

-- 手動で書くと面倒な Eq の実装
data Color = Red | Green | Blue

-- Elabに任せる（idris2-elab-util ライブラリ使用）
%runElab derive "Color" [Generic, Eq, Show]
-- → コンパイラが Eq Color と Show Color の実装を自動生成

Elabがやっていること：

1. Color のコンストラクタ一覧を取得（Reflection）
2. 各コンストラクタの組み合わせに対して == の実装を構築
3. 生成した項を型検査にかける
4. 通ったら定義として登録

2.3 やや高度な例：コンパイル時計算

-- コンパイル時にフィボナッチ数を計算して定数として埋め込む
fib : Nat -> Nat
fib 0 = 0
fib 1 = 1
fib (S (S n)) = fib (S n) + fib n

-- %runElab で fib 10 を計算し、結果をコードに埋め込む
myConst : Nat
myConst = %runElab do
  let result = fib 10  -- コンパイル時に計算される
  fill (quote result)  -- 結果（55）をコードに埋め込む

コンパイル後のバイナリには 55 だけが残る。fib の計算は実行時には起きない。

---

第3章：runIO —— コンパイラが外を見る窓

3.1 runIOとは

runIO はElabモナド内でIOアクションを実行する関数。つまりコンパイル時にファイルを読んだり、ネットワーク通信したり、環境変数を取得したりできる。

%runElab do
  contents <- runIO $ readFile "schema.json"
  -- ↑ コンパイル時にファイルを読む
  -- ↓ 読んだ内容に基づいて型を生成する
  generateTypes contents

3.2 何に使えるか（合法的な用途）

Type Provider パターン：外部のスキーマ定義から型を自動生成。

-- schema.json: {"name": "string", "age": "int"}
-- ↓ コンパイル時にこのJSONを読み、以下の型を自動生成
-- record User where
--   constructor MkUser
--   name : String
--   age : Int

これは合法。なぜならJSONスキーマファイルは基本的に変わらない（変えたら再コンパイルすればいい）。コンパイル結果の正しさは、スキーマファイルが変わらない限り永続する。

コントラクトABI読み込み：

-- EthereumノードからコントラクトのABIを取得
-- → 存在しない関数を呼ぶコードがコンパイルエラーになる型を生成
%runElab do
  abi <- runIO $ fetchABI "0x1234..."
  generateContractInterface abi

これも合法。デプロイ済みコントラクトのABIは変わらない（proxyパターン除く）。

3.3 何に使えないか（致命的な誤用）

市場価格の読み込み：

-- コンパイル時にETH価格を取得
%runElab do
  price <- runIO $ fetchPrice "ETH/USD"  -- 3000ドル！
  -- この 3000 を型に焼き込む
  -- ...だが、実行時には 2800 ドルかもしれない

なぜダメか：この値は「腐る」。コンパイルした瞬間は正しいが、バイナリを実行する瞬間には嘘になっている可能性がある。型システムが保証する「正しさ」は永続的でなければならないが、価格は永続的ではない。

3.4 判定基準：runIOで読んでいいもの

読んでいい	読んではいけない
スキーマ定義（JSON Schema, protobuf）	市場価格
コントラクトABI	ブロック高
設定ファイル	時刻
環境変数（ビルド設定）	API残高
テストデータ	乱数

基準は一つ：再コンパイルせずに値が変わるなら、読んではいけない。

---

第4章：Elabと型の関係 —— 型は封筒、Elabは封筒を作る機械

4.1 三者の役割

Elab（コンパイル時）: 型と項を生成する。生成し終えたら死ぬ。
型（コンパイル時）  : 項の形を検査する。バイナリに焼き込まれる（一部は消去される）。
モナド（ランタイム）: 実際の計算を記述する。実行時に評価される。

時系列で見ると：

1. Elabが走る       → 型と項が生成される（Elab死亡）
2. 型検査が走る     → 生成された項が型に合うか検査される
3. コード生成       → バイナリが作られる（型の一部は消去される）
4. ランタイム       → モナドの中身が実行される

4.2 Elabで型は作れるが、型に値は入れられない

よくある誤解：「Elabで何でも型に入れられるんでしょ？」

正確には：

• Elabで型の構造は自由に作れる（新しいdata型、record、interfaceの定義を生成）
• Elabで型レベルの計算もできる（Nat の足し算とか）
• しかしランタイムでしか決まる値は型に入れられない（型検査はコンパイル時に完了するから）

-- できる：コンパイル時に既知の値を型に入れる
Vect 3 Int   -- 3はコンパイル時に既知

-- できる：∀で量化した変数を型に入れる
f : (n : Nat) -> Vect n Int   -- nは「どんな値でもいい」

-- できない：ランタイムの値で型が変わる
-- 「ユーザーが3と入力したらVect 3 Int、5ならVect 5 Int」
-- → 型検査の時点でユーザーはまだ入力していない

4.3 依存型の「依存」が意味すること

「値に依存する型」と聞くと「実行時の値で型が変わる」と思いがちだが、違う。

正確には：型の中に値レベルの式を書ける。しかしその式がいつ評価されるかは別の話。

-- 「長さnのベクトル」
-- n は型の中に登場する値レベルの変数
append : Vect n a -> Vect m a -> Vect (n + m) a

n + m は型の中にある値レベルの計算。コンパイラはこれを**記号的に（シンボリックに）**扱う。nが3でmが5ならn + mは8と計算できるが、nが未知なら「n + mという式のまま」保持する。

コンパイラは式の具体的な値を知らなくても、構造的な等しさ（n + m と n + m は同じ）や定義に基づく簡約（0 + m は m）で型検査を進められる。

つまり依存型は「ランタイムの具体的な値を知っている」のではなく、「値の世界の式を型の世界に持ち込んで記号的に推論できる」ということ。

---

第5章：Elabとモナドの決定的な違い

5.1 時間軸の違い（最重要）

Elab  : コンパイル時に生き、コンパイル後に死ぬ
IO    : ランタイムに生き、プログラム終了で死ぬ
Prob  : ランタイムに生き、サンプリングで値が確定する

Elabとモナドは同じ時間に存在しない。 これが全ての混乱の根源。

「Elabで確率計算」は「死者に天気を聞く」。 「モナドでコンパイルを操る」は「生まれる前の自分に指示を出す」。

5.2 「メタ」のレベルの違い

レベル0（オブジェクト言語）: 普通のIdrisコード。ランタイムで動く。
レベル1（メタ言語）       : Elabスクリプト。レベル0のコードを生成する。

Elabはレベル1にいる。モナドはレベル0にいる。Elabがモナドを「見下ろして」生成することはできるが、モナドがElabを「見上げて」操ることはできない。

-- Elabがモナドを含むコードを生成する（OK）
%runElab do
  -- 「IO Stringを返す関数」の定義を生成
  declare `(myFunc : IO String)
  define `(myFunc = readFile "hello.txt")

-- モナドがElabを呼ぶ（不可能）
myFunc : IO String
myFunc = do
  %runElab ...  -- ここにElabは書けない。ランタイムにElabはいない。

5.3 エフェクトの違い

	Elab	IO	Prob
いつ走る	コンパイル時	ランタイム	ランタイム
何を読める	ソースコード、ファイル（runIO）	外部世界すべて	乱数源
何を書ける	型、項、定義	外部世界すべて	確率分布
結果は	バイナリに焼き込まれる	実行のたびに変わりうる	サンプルのたびに変わる
死ぬタイミング	コンパイル完了時	プログラム終了時	評価完了時

---

第6章：Indexed Monadと確率 —— 何ができて何ができないか

6.1 Indexed Monadとは

通常のモナド：m a（計算してaを返す） Indexed Monad：m i j a（状態をiからjに変えつつaを返す）

interface IxMonad (m : state -> state -> Type -> Type) where
  pure  : a -> m i i a                     -- 状態を変えずに値を返す
  (>>=) : m i j a -> (a -> m j k b) -> m i k b  -- 状態遷移を連鎖

i, j, k は型レベルの状態。コンパイル時に追跡される。

6.2 何が追跡できるか

プロトコル（手順の正しさ）：

data DoorState = Open | Closed

-- ドアを開ける：Closed → Open に遷移
open : DoorAction Closed Open ()
-- ドアを閉める：Open → Closed に遷移
close : DoorAction Open Closed ()

-- これはコンパイルが通る
correct : DoorAction Closed Closed ()
correct = do
  open    -- Closed → Open
  close   -- Open → Closed

-- これはコンパイルエラー
wrong : DoorAction Closed Closed ()
wrong = do
  close   -- Closed → ??? 型エラー！Closed状態でcloseはできない

6.3 確率をインデックスに入れたらどうなるか

夢：

-- 事前分布Priorから事後分布Posteriorへの遷移を型で追跡
observe : ProbAction (Prior p) (Posterior (update p obs)) Observation

これは書ける。依存型だからインデックスに関数適用を入れられる。

しかし update p obs はコンパイル時に評価される。 つまり：

• p（事前分布）がコンパイル時に確定している必要がある
• obs（観測データ）がコンパイル時に確定している必要がある
• ランタイムで新しい観測が来るたびに型が変わる、ということはできない

6.4 じゃあ何に使えるのか

型レベルで追跡できるもの（コンパイル時に決まる構造）：

• 「observeを呼んだ回数」
• 「どの確率変数をサンプル済みか」
• 「条件付けを行ったかどうか」
• 「モデルの構造（何が何に依存しているか）」

型レベルで追跡できないもの（ランタイムで決まる値）：

• 「事後確率が0.73である」
• 「分布の平均が3.2である」
• 「この観測のあと信念がどう変わったか」の具体的な数値

つまりIndexed Monadで確率計算のプロトコルは検査できるが、確率計算の結果は検査できない。

-- 型が保証すること：
-- 「observeを呼ばずにposteriorを使うコードはコンパイルエラー」
-- 「sampleせずにscoreするコードはコンパイルエラー」

-- 型が保証しないこと：
-- 「posteriorの値が正しいかどうか」
-- 「scoreの計算が数学的に妥当かどうか」

---

第7章：Elabの実用パターン集

7.1 パターン1：ボイラープレート生成

最も一般的な用途。Eq, Show, Ord などのインターフェースを自動導出する。

-- 手動で書くと各コンストラクタの組み合わせ分のコードが必要
-- Elabなら1行
%runElab derive "MyType" [Generic, Eq, Show, Ord]

7.2 パターン2：Type Provider（外部データからの型生成）

コンパイル時に外部スキーマを読み、型安全なアクセサを生成。

-- DBスキーマから型を生成（概念的な例）
%runElab do
  schema <- runIO $ readFile "schema.sql"
  for_ (parseTables schema) $ \table => do
    declareRecord table.name table.columns
    deriveInsert table.name
    deriveSelect table.name

7.3 パターン3：証明の自動探索

型が要求する証明項を自動的に見つける。

-- 「n < m であることの証明」を自動生成
%runElab do
  goal <- getGoal  -- 今求められている型（例：LT 3 5）
  search           -- 型に合う項を探索（この場合は自明なので見つかる）

7.4 パターン4：DSL（ドメイン特化言語）のコンパイル

Elabを使って、自作のDSLをIdrisのコア言語に変換する。

-- 状態遷移図をDSLで書き、Elabが型付きコードに変換
%runElab compileStateMachine `{
  states: [Locked, Unlocked]
  transitions:
    Locked  --coin--> Unlocked
    Unlocked --push--> Locked
}
-- → Indexed Monadベースの型安全なステートマシンコードが生成される

7.5 パターン5：コントラクトABIからのバインディング生成

（今回の議論で出た実用例）

-- Elabがコントラクトの関数シグネチャを型として生成
-- 存在しない関数を呼ぶ → コンパイルエラー
-- 引数の型が違う → コンパイルエラー
%runElab do
  abi <- runIO $ fetchABI contractAddress
  for_ abi.functions $ \f => do
    declareExternalFunction f.name f.inputs f.outputs

---

第8章：まとめ —— 三つの世界の分離

8.1 三つの世界

┌─────────────────────────────────────────────┐
│ Elab の世界（コンパイル時）                    │
│                                              │
│ できること：型を作る、項を作る、                │
│           ファイルを読む（runIO）、            │
│           証明を探す、コードを生成する          │
│                                              │
│ できないこと：ランタイムの値を知る、            │
│             ユーザー入力を受け取る、           │
│             市場価格を「永続的に正しく」知る     │
│                                              │
│ 寿命：コンパイル開始 → コンパイル完了で死亡     │
├─────────────────────────────────────────────┤
│ 型 の世界（コンパイル時に検査、一部は残る）      │
│                                              │
│ できること：形の検査、手順の強制、               │
│           リソースの追跡（線形型）、            │
│           全パス網羅の保証（totality）          │
│                                              │
│ できないこと：値の正しさの検査、                │
│             確率の計算、市場の予測              │
│                                              │
│ 寿命：永遠（コンパイルが通った事実は不変）       │
├─────────────────────────────────────────────┤
│ モナド の世界（ランタイム）                     │
│                                              │
│ できること：実際の計算、IO、確率計算、           │
│           外部状態の読み書き、                  │
│           観測に基づく信念更新                  │
│                                              │
│ できないこと：型を変える、コンパイラを操る、     │
│             過去に遡って型検査をやり直す         │
│                                              │
│ 寿命：実行開始 → 実行終了                      │
└─────────────────────────────────────────────┘

8.2 一言でまとめると

Elabは型を作る。型はモナドの形を検査する。モナドは計算する。 Elabは死者。型は法律。モナドは生者。 死者が法律を書き、法律が生者を縛り、生者が世界を動かす。

8.3 実用上の判断基準

何かをやりたいとき：

1. それはコンパイル時に確定するか？ → Yes → Elab/型で扱える
2. それは手順の正しさか？ → Yes → Indexed Monad + 線形型で強制できる
3. それは値の正しさか？ → Yes → モナドの中で計算し、ランタイムで検証
4. それは「腐らない」外部データか？ → Yes → runIOで読んでいい
5. それは「腐る」外部データか？ → Yes → 型に入れるな。モナドで扱え。

---

付録A：用語集

用語	意味
Elaboration	表面言語をコア言語（TT）に変換するプロセス
Elab モナド	エラボレーションの操作をスクリプトとして書くためのモナド
Reflection	コンパイラの内部表現をプログラムから読み書きする機能
Unification	二つの項を等しくする代入を見つける操作
TT	Idris 2のコア言語（Type Theory）
QTT	Quantitative Type Theory。変数の使用回数を型レベルで追跡
runIO	Elabモナド内でIOアクションをコンパイル時に実行する関数
Type Provider	外部データからコンパイル時に型を生成するパターン
Totality	関数が全入力に対して停止し、全パターンを網羅していること
線形型	変数を正確に1回だけ使用することを強制する型（QTTの多重度1）

付録B：参考資料

• Idris 2公式ドキュメント — Elaborator Reflection
• Christiansen & Brady, "Elaborator Reflection: Extending Idris in Idris"
• Brady, "Idris 2: Quantitative Type Theory in Practice"
• idris2-elab-util ライブラリ

---

付録C：Elab操作のコストとOOM対策

なぜOOMになるのか：根本原因

Idris 2のコンパイラ（Core）は内部的にIORef（可変参照）ベースで実装されている。Brady本人が「State Monadより2〜3倍速いから"ugly"な方を選んだ」と書いている。つまりGCに頼った設計で、巨大な中間項が生成されるとGCが追いつかずにOOMになる。

各操作のコストモデル

unify（単一化）— 🔴 最大の犯人

計算量：項のサイズに対して最悪指数関数的

unifyは二つの項を正規形（Normal Form）に簡約してから比較する。問題はこの**正規化（normalisation）**にある。

unify A B
  → A を正規形に簡約（NF）
  → B を正規形に簡約（NF）
  → 構造的に比較
  → メタ変数があれば制約を生成

OOMを引き起こすパターン：

1. 型レベルのNatが大きい：Vect 256 Int の型検査で 256 がペアノ数 S (S (S ... (S Z) ...)) として展開される。256段のコンストラクタが正規化時にメモリ上に実体化する。

2. ネストしたパターンマッチ：Vect 3 (Vect 3 (Maybe a)) のパターンマッチだけで1GB消費した報告がある（Idris 1のIssue #1707）。パターンの組み合わせ爆発 (3^n) が原因。

3. 型クラス（interface）の解決チェーン：Monad m => ... の解決で、Monad → Applicative → Functor の連鎖を辿る際、各段階でunifyが走る。深いモナドスタック（StateT を重ねるなど）で爆発する。

対策：

• 型レベルのNatは小さく保つ（256以上は避ける）
• Integer を使い、必要な性質は believe_me で仮定する（証明を諦める代わりにコンパイルを通す）
• パターンは浅く。ネストしたVectのパターンマッチは補助関数に分割
• %auto_implicit_depth はデフォルト50。これを上げるとOOMリスクが跳ね上がる

---

search（auto implicit / proof search）— 🔴 二番目の犯人

計算量：探索深さに対して指数関数的

searchは以下の順序で項を探す：

1. ローカル変数（パターン変数、let束縛）
2. 対象の型のコンストラクタ（引数があれば再帰的に探索）
3. 関数型のローカル変数（引数を再帰的に探索）

最大探索深さはデフォルト50（%auto_implicit_depth で変更可能）。

search (目標型 T)
  → T のコンストラクタ C1, C2, ... を列挙
  → 各 Ci の引数型について再帰的に search
  → 深さ50まで繰り返す（分岐 × 深さ → 指数爆発）

OOMを引き起こすパターン：

1. interfaceの実装が多い：Eq や Show の実装が大量にスコープにあると、候補が多すぎて探索空間が爆発
2. public export vs export：export（定義を公開しない）だとコンパイル時に関数を簡約できず、searchが正規形を得られずに詰まる。public export（定義も公開）にすると簡約可能になりsearchが進む。しかし簡約自体にメモリを食う。トレードオフ。
3. 複雑な証明のauto探索：{auto prf : complicated_predicate x y z} で complicated_predicate の評価にメモリが爆発

対策：

• auto は単純な型にだけ使う（IsJust x レベル）
• 複雑な証明は auto に頼らず手書きで渡す
• %auto_implicit_depth 10 のように下げて実験
• %hint の数を管理する。スコープ内のhintが多いほど探索空間が広い

---

check（型検査）— 🟡 中程度

計算量：項のサイズに対して概ね線形。ただしunifyを内部で呼ぶ

check自体は項を走査して各サブ項の型を検査するだけなので線形的。しかし暗黙引数を見つけるたびにメタ変数を生成し、unifyで解決しようとするため、暗黙引数が多いと間接的にコストが上がる。

OOMを引き起こすパターン：

• 暗黙引数が非常に多い関数の適用（各暗黙引数にメタ変数が生成され、それぞれunifyが走る）
• リスト/Vectリテラルが長い：[1,2,3,...,100] は 1 :: 2 :: 3 :: ... :: Nil に展開され、各 :: にオーバーロード解決（:: はListにもVectにもある）が走る。Issue #1771で「リスト長nに対してAST サイズが3^n」になる報告あり

対策：

• 長いリテラルは避ける。ファイルから読むか、Elabで生成
• 暗黙引数は必要最小限に
• 型注釈を明示的に書く（the (List Int) [1,2,3]）。コンパイラの推論負荷を減らす

---

fill（穴埋め）— 🟢 低コスト

計算量：項のサイズに線形

穴に項を代入するだけ。ただし代入後にcheckが走ることが多いので、fillのコスト自体は低くても、連鎖的にunifyが走る。

---

goal（目標型の取得）— 🟢 低コスト

計算量：ほぼO(1)

現在の穴のメタ変数の型を参照するだけ。正規化が必要な場合はコストが上がるが、通常は低い。

---

declare（宣言の追加）— 🟡 宣言内容に依存

計算量：宣言する定義の型検査コスト

declare自体は定義をコンテキストに登録するだけだが、登録時に型検査が走るので、コストは宣言する内容のcheck + unifyコストに等しい。

大量のdeclareを%runElabで回すと、各宣言の型検査が積み重なる。

---

runIO（コンパイル時IO）— ⚠️ 予測不能

計算量：実行するIOアクション次第

ファイル読み込みならファイルサイズに比例。ネットワーク通信なら応答時間に依存。メモリ的には読み込んだデータがそのままIdrisの項に変換されるため、大きなファイルを読むとOOMの原因になる。

---

コスト一覧表

操作	メモリ危険度	主な原因	最悪計算量
unify	🔴 高	正規化の展開、パターン組み合わせ爆発	指数関数的
search	🔴 高	探索空間の分岐×深さ	指数関数的
check	🟡 中	暗黙引数のメタ変数生成→unify連鎖	線形×unifyコスト
declare	🟡 中	宣言内容のcheck+unifyコスト	宣言の複雑さ次第
fill	🟢 低	代入自体は軽い	線形
goal	🟢 低	参照のみ	O(1)
runIO	⚠️	読み込むデータ量次第	予測不能

OOM回避の実践ルール

1. 型レベルの計算を減らす

-- 🔴 OOMリスク高：型レベルで256回のS適用
myVec : Vect 256 Int

-- 🟢 安全：型レベルの数値は小さく保つ
-- 大きな固定長データはerased indexで
data SizedArray : Type where
  MkSizedArray : (0 n : Nat) -> (data : List Int) -> SizedArray

2. 型注釈を明示する

-- 🔴 コンパイラに推論させすぎ
f x = map (+1) (filter (>0) x)

-- 🟢 型を書いてunifyの負荷を下げる
f : List Int -> List Int
f x = map (+1) (filter (>0) x)

3. モナドスタックを浅く保つ

-- 🔴 OOMリスク：深いモナドスタック
-- StateT (ReaderT (WriterT (ExceptT ...)))
-- → interface解決の連鎖で爆発

-- 🟢 レコードで状態をまとめる
record AppState where
  constructor MkAppState
  counter : Nat
  config  : String
  errors  : List String

4. %auto_implicit_depth を管理する

-- デフォルトは50。必要なら下げる
%auto_implicit_depth 25

-- 特定のブロックだけ上げることはできない
-- グローバルに影響するので注意

5. パターンマッチを分割する

-- 🔴 ネストしたパターンで組み合わせ爆発
check : Vect 3 (Vect 3 (Maybe a)) -> Maybe a
check [[Just p, _, _], [Just p, _, _], [Just p, _, _]] = Just p
-- ↑ これだけで1GB消費する可能性

-- 🟢 補助関数に分割
checkCol : Fin 3 -> Vect 3 (Vect 3 (Maybe a)) -> Maybe a
checkCol i grid = ...  -- 1行ずつ処理

6. コンパイル時のメモリ監視

# メモリ使用量を監視しながらコンパイル
# Chez Schemeバックエンド使用時
idris2 --build myproject.ipkg +RTS -M4G -RTS

# ログで何が遅いか特定
idris2 --log elab 3 --build myproject.ipkg
idris2 --log unify 5 --build myproject.ipkg

まとめ：OOMの80%はunifyとsearch

あなたのOOMはほぼ確実に以下のどれか：

1. 型レベルのNatが大きい（正規化で展開）
2. autoで複雑な証明を探させている（探索空間爆発）
3. リストリテラルが長い（オーバーロード解決で3^n）
4. モナドスタックが深い（interface解決チェーン）

型は物理。物理には限界がある。RAMが足りないならコンパイラに楽をさせろ。型注釈を書け。autoを減らせ。パターンを分割しろ。

---

このスキルの使い方

Idris2プロジェクトで以下の状況になったら、このスキルを参照：

1. Elabスクリプトを書こうとしている → 第1〜3章を読む
2. runIOで何かを読み込もうとしている → 第3章の判定基準を確認
3. Indexed Monadで何かを追跡しようとしている → 第6章を読む
4. コンパイル時にOOMになる → 付録Cを読む
5. 「型で値を保証したい」と思った → 第4〜5章を読んで可能性を判断