AI エージェント向けエラーメッセージ（型エラーアブレーション）

エラーメッセージは数十年、たった一人の読者＝人間を想定して設計されてきた。人間はエラーをざっと読み、読み飛ばし、長いと圧倒される — だから「簡潔であるべき」という設計圧力が働いた。だが AI コーディングエージェントという第二の読者は、疲れず・飽きず・長さに圧倒されない。実質的な上限はコンテキストウィンドウだけで、現代では十分広い。ならば「人間向けに削ったエラー」は、エージェントには情報不足ではないか? Krishnamurthi & Flatt (2026) がこれを制御実験で測った。

中心の問い: エラーは2モード持つべきか

言語は 簡潔な人間モードと詳細な AI モードの2つを提供すべきではないか。

これが論文の核。gcc や Elm のような「人間に最適化された簡潔さ」は、エージェントにとって機会損失かもしれない。ただし「多ければ良い」とも限らない — 詳細過多はエージェントを真の誤りでなく誤った箇所へ誘導しうるし、簡潔な出力で訓練されたモデルは長文診断の読み方を知らないかもしれない。だから経験的に測る必要がある。

なぜ Hindley-Milner を選んだか

アブレーション(情報を段階的に削る比較)を成立させるには、同じ型エラーを詳細度違いで出せる言語が要る。HM の単一化は、誤りが検出された場所と導入された場所がズレることで悪名高い — つまり「短いが誤誘導するメッセージ」と「冗長だが真因を含むメッセージ」の緊張が自然に生まれる。Rust のトレイト解決も同種の性質を持ち、この問いは今日的。

実験言語は Shplait(Racket #lang、Plait の Shrubbery 構文版、HM 推論つき教育用 ML)。型チェックを切って実行できる(~untyped)点が決め手 — ほとんどの型付き言語はランタイムが型に依存して安全チェックを欠くため、これができない。

4つの報告モード（アブレーション軸）

~type_source_mode プラグマで型情報を段階的に削る:

モード	エージェントが受け取るもの
untyped	型チェッカー無効。フィードバックはテスト合否のみ(動的エラー)
min	矛盾する2つの型のみ(`Int vs. Listof(Int)`)。位置はほぼ無し
proximate	上記＋単一化失敗の単一ソース式(ML/OCaml 並み)
all	上記＋残りの単一化スタック全体＋全位置。長いが真因を含みやすい

untyped 以外は、型チェック通過後にテスト失敗の詳細も渡る。

実験プラットフォーム: wheat / chaff / oracle

wheat(小麦) — 正しくテスト通過する10本の参照実装(avl-tree, dijkstra, evaluator, huffman, regex…)。データ型のみ型注釈つき、本体は無注釈で HM を最大限効かせ混乱を最大化
chaff(籾殻) — 各 wheat に局所編集を1つだけ入れた壊れ版(計60)。制約: ①必ず型エラーになる ②テストを5件以上落とす(ライブコード内、42 で誤魔化す逃げを封じる) ③単一エラー
oracle — 決定的シェルスクリプト。修正試行を TYPE ERROR / TESTS FAILED / SUCCESS に3分類。テストはモデルに漏らさない(aider --no-git)
エージェント足場は aider(SEARCH/REPLACE diff)、モデルは再現性重視で qwen2.5-coder:14b(ollama, ローカル)。10回 × 240 = 2,400 試行

3つの発見（RQ）

RQ1: 詳細度は効くか → YES. 成功率は単調に上がる。型付き内では min ≤ proximate ≤ all が10回中10回維持(Page 検定 p=2.6×10⁻⁸)。

モード	成功率(qwen)
untyped	33.5%
min	41.7%
proximate	47.8%
all	52.8%

成功までのターン数中央値は1。冗長性の効果は多段推論ではなく、最初の仮説を正しく形成させることにある。ただしチャフ単位では逆転例もあり(一様に all が最良ではない)。

RQ2: 型システムの存在は効くか → YES. 型付きは untyped を一貫して上回る。型エラーは因果信号(何が・どこで競合したか)、テスト失敗は症状信号(何かが間違っている、原因は逆算が要る)。単一の型エラーは複数のテスト失敗を要約する。※ただし untyped は「型なし」と「フィードバック種別の変化」を同時に変えており、因果の切り分けは未達(内的妥当性の脅威)。

RQ3: 型が通れば意味も正しいか → ほぼ YES(この設定では). 型的に正しくできた872試行中、854 = 97.9% が全意味テストも通過。「型が通れば動く」の俗説を予備的に裏づける。ただし単一エラー設計の産物でもある(1箇所戻せば元の正しさが復活する)— 複数エラーが絡むと乖離しうる。型チェックは大規模テスト実行より速いので、エージェントにとって型指向フィードバックは特に価値が高い。

二次的発見: 難読化してもモデルは意味を再構築する

claude-haiku-4.5 だと素の成功率は 92〜96% と高すぎる。そこで全識別子を無意味な2文字へα変換(avl_node→ap, avl_height→aj)。それでも成功率 untyped 62.8% → all 69.7% と型詳細度の傾向は残り、かつモデルの出力ログには「これはダイクストラのようだ」「af は選択、ax はクリーネスター」等、アルゴリズムを再構築している痕跡が明確に残った(ログ内に “Dijkstra” 18回、“Kleene” 等が出現)。名前が消えても、構造から正体を当ててくる。→ 形式的/機能的言語能力の議論材料。

押さえどころ（カード化候補）

問い → エラーメッセージは人間だけの読者向けに簡潔化されてきたが、AI エージェントは長文に圧倒されない第二の読者。簡潔な人間モードと詳細な AI モードを分けるべきでは?
方法 → HM の単一化(検出位置と真因がズレる)を使い、型情報を untyped→min→proximate→all と段階的に削るアブレーション。Shplait + wheat/chaff + 決定的 oracle + aider。
RQ1 → 詳細なほど修正率↑(33.5→52.8%、単調、p≈10⁻⁸)。効くのは多段推論でなく初手の仮説形成(成功ターン中央値1)。
RQ2 → 型システム有り > テストのみ。型エラー=因果信号、テスト失敗=症状信号。
RQ3 → 型が通った修正の 97.9% が意味テストも通過(ただし単一エラー設計の産物)。型チェックは速いのでエージェント向けに有利。
難読化 → 識別子を全消ししてもモデルは構造からアルゴリズムを再構築して直す。