Elixir 1.20 の漸進型システム — アノテーションなしで「検証済みバグ」を見つけるということの実際

• はじめに — 4年越しで終えた最初のマイルストーン
• dynamic() が any() と違う点
• 1.20が実際に新しくやること
• 「13個中12個通過」を一次資料に照らしてみた
• コンパイル時間 — 「最速」主張の実際の大きさ
• タダではない部分
• アップグレード前に知っておくべきこと
• 型シグネチャはなぜまだ遠いのか
• では今、何をすべきか
• おわりに
• 参考資料

はじめに — 4年越しで終えた最初のマイルストーン

Elixirチームが集合論的型(set-theoretic types)をコンパイラに組み込むと発表したのは2022年です。2023年にはGiuseppe Castagna、Guillaume Duboc、José ValimがThe Design Principles of the Elixir Type Systemで設計原理を発表し、「研究から開発へ移る」と宣言しました。そして2026年6月3日、Elixir v1.20がリリースされ、この最初のマイルストーンが終わりました。

マイルストーンの内容はこうまとめられます — 型アノテーションを一つも導入せずに、すべてのElixirプログラムに対して型推論と漸進的型チェックを行う。 あなたがコードを一行も書き換えなくても、コンパイラがデッドコードと「検証済みバグ(verified bugs)」を見つけてくれるという意味です。ここでいう検証済みバグとは、発表文の定義どおり実行すれば必ずランタイムで失敗することが保証された型付け違反を指します。

本稿はハイプを取り除き、次の3点を見ます。(1) 1.20が実際に新しくやること、(2) 発表文の数値を一次資料に照らすと何が残るか、(3) 文書には書かれているが発表文には出てこないトレードオフ。Elixir 1.18とOTP 27/28の時代の生態系全体の見取り図は、すでにモダン Elixir & Phoenix 2026とモダン Erlang と BEAM 2026で扱ったので、ここでは型システムだけを掘り下げます。

dynamic() が any() と違う点

公式ドキュメントによれば、Elixirの型システムの目標は3つです — 健全性(sound): 推論・割り当てられた型がプログラムの実際の動作と一致すること。漸進性(gradual): dynamic()型があり、dynamic()がなければ静的型システムのように振る舞うこと。開発者フレンドリーさ: 型を和集合・積集合・否定という基本的な集合演算で記述すること(だから「集合論的」です)。

ここで核心となるのがdynamic()です。多くの漸進型システムのany()は、型システムの観点からは「何でもあり」を意味し、そのため違反を一切報告しません。Elixirのdynamic()は違います。発表文の表現では、2つの性質を持っています — 互換性(compatibility) と 絞り込み(narrowing) です。

まず互換性から見てみましょう。発表文の例をそのまま持ってきます。

def percentage_or_error(value) when is_integer(value) do
  value_or_error =
    if value > 1 do
      value
    else
      "not well"
    end
  # ... more code ...
  if value > 1 do
    value_or_error / 100
  else
    String.upcase(value_or_error)
  end
end

value_or_errorは整数かバイナリのどちらかです。/演算子は数値しか受け付けず、String.upcaseはバイナリしか受け付けません。厳格な静的型システムなら、ここで違反を2つ報告するはずです。ところがこのプログラムはランタイムで一切例外を出しません。型システムがプログラムの意図を精密に捉えきれないために生じる偽陽性(false positive)です。

Elixirはこの変数にdynamic(integer() or binary())という型を付けます。そしてdynamic()型の値を関数に渡すときは、供給された型と許容された型が互いに素(disjoint)なときだけ違反を出します。/が数値しか受け付けなくても、dynamic(integer() or binary())は整数でありうるので互いに素ではなく、したがって違反にはなりません。一方、次のように書き換えると、

value_or_error =
  if value > 1 do
    value
  else
    "not well"
  end

Map.fetch!(value_or_error, :some_key)

Map.fetch!はマップを期待しますが、この値はランタイムでは整数かバイナリのどちらかにしかなりません。互いに素なので違反です。これがElixirが「検証済みバグだけを報告する」と言う根拠です。

とはいえ、検証済みバグだけを報告してバグをあまり見つけられないのでは使い物になりません。そこで絞り込みが効いてきます。

def add_a_and_b(data) do
  data.a + data.b
end

dataはdynamic()から始まりますが、data.a、data.bが加算に使われているのを見て%{..., a: number(), b: number()}に絞り込まれます(先頭の...は他のキーがあってもよいという意味です)。そのため.bを書き忘れてdata.a + dataと書くと、dataは先にマップへ絞り込まれてから数値として使われようとするので、違反になります。

一言でいえば — Elixirのdynamic()は範囲のように振る舞い、コードをたどりながら絞り込まれ、型チェックがその範囲を外れたときに違反を出します。 他の漸進型システムがdynamic型で型情報を捨てるのとは正反対の方向です。

1.20が実際に新しくやること

CHANGELOGを基準に、1.20で新しく入ったものを見ていきます。

ガード推論。 今回のリリースの最後のピースでした。

def example(x, y) when is_list(x) and is_integer(y)
# xはリスト、yは整数

def example({:ok, x} = y) when is_binary(x) or is_integer(x)
# xはバイナリまたは整数、yは:okで始まる2要素タプル

def example(x) when is_map_key(x, :foo)
# xは:fooキーを持つマップ -> %{..., foo: dynamic()}

def example(x) when not is_map_key(x, :foo)
# xは:fooキーを持たないマップ -> %{..., foo: not_set()}
# したがって関数本体のx.fooは型付け違反

def example(x) when tuple_size(x) < 3
# タプル要素は最大2個 -> elem(x, 3)は違反

否定(not is_map_key)がnot_set()という型で表現されるのは、いかにも集合論的型システムらしいところです。マップ・リストのサイズ検査は「空かどうか」の検査に変換されます。

関数本体全体の推論。 1.18までは、パターンでのみ推論していました。今は本体も見ます。

def sum_to_string(a, b) do
  Integer.to_string(a + b)
end

+は整数と浮動小数点数の両方を受け付けますが、結果が整数を要求する関数へ渡されるため、aとbが両方とも整数だと推論されます。逆方向に情報が流れているわけです。

節間の推論とoccurrence typing。 case、cond、withにoccurrence typingが付き、先行する節が後続の節を絞り込むようになりました。

case System.get_env("SOME_VAR") do
  nil -> :not_found
  value -> {:ok, String.upcase(value)}
end

System.get_env/1はnilかバイナリのどちらかを返しますが、最初の節がnilを捕らえているのでvalueは必然的にバイナリになり、String.upcaseが違反なく通ります。おまけとして重複節(redundant clauses) の警告も付きました。

依存関係をまたぐ推論。 CHANGELOGの「Perform type inference across applications」の項目です。1.20-rc以前は、標準ライブラリ関数の呼び出しでのみ型を推論しており、あなたの依存モジュールを呼び出しても型チェックだけで推論はしていませんでした。今は依存関係から推論された型情報が、あなたのアプリの推論に流れ込みます。コンパイラを通過する型情報の量が大きく増える変更であり、Elixirチームは2026年1月のロードマップ記事で、この段階だけにリリース候補を丸々一つ割り当てたと述べています。

実際、1.20はリリース候補を七つ(rc.0からrc.6まで)経ました。rc.0が2026年1月9日、rc.6が5月21日、最終リリースが6月3日です。1月のロードマップ記事が予告していた最終リリース時期は「5月」だったので1か月ほど遅れたことになりますが、型システムの全面導入としては上出来な部類です。

「13個中12個通過」を一次資料に照らしてみた

発表文で最も目を引く数値はこれです。

our implementation performs well in the "If T: Benchmark for Type Narrowing" benchmark. Elixir passes 12 of the 13 categories

If-Tは実在するサードパーティのベンチマークです。Hanwen GuoとBen Greenmanが作り(arXiv:2508.03830)、ユタ大学PLTグループのutahplt/ifT-benchmarkリポジトリに置かれています。型の絞り込み(occurrence typing)を測るベンチマークで、テーマごとに「型チェックを通過すべきプログラム」と「通過してはいけないプログラム」を対にして持っています。カテゴリはちょうど13個です — positive、negative、connectives、nesting_body、struct_fields、tuple_elements、tuple_length、alias、nesting_condition、merge_with_union、predicate_2way、predicate_1way、predicate_checked。

ところが発表文がこの文につけているリンクは、リポジトリのBenchmark Results表です。その表を開くと — Elixirの列がありません。

今日(2026-07-16)時点で確認した内容はこうです。上流の結果表が扱う型チェッカーはTyped Racket、TypeScript、Flow、mypy、Pyright、Sorbet、Luau、MLsem、Typed Clojure、ty、Pyreflyの11個です。リポジトリのツリー(106エントリ)の言語ディレクトリもこの11個だけで、Elixirディレクトリはありません。READMEの全文を大文字小文字を区別せず「elixir」で検索すると0件で、Elixirの追加を提案するPRも、開いているものと閉じているものを合わせて存在しません。

つまり正確に言うとこうなります — 「13個中12個通過」はElixirチーム自身の自己測定値であり、発表文がリンクしている結果表はその数値を裏付けていません。 間違っているという意味ではありません。上流に再現可能な実装が上がっていないため、第三者が確認できないという意味です。どのカテゴリを1つ通過できなかったのかも公開されていません(検索結果の要約には特定のカテゴリを名指しする文が漂っていますが、どの一次資料でも確認できないため、ここでは引用しません)。

文脈のために、上流表の実際の数字を写しておくと、自己測定値の位置づけをつかむ助けになります。

上流If-T結果表(utahplt/ifT-benchmark, v1.1) — 13カテゴリ基準
  Typed Clojure : 13/13  (全項目通過)
  Typed Racket  : 12/13  (tuple_length で失敗)
  MLsem         : 12/13  (connectives で失敗)
  Flow          : 11/13
  Pyright       : 11/13
  TypeScript    : 10/13  (nesting_condition, predicate_1way, predicate_checked で失敗)
  mypy          :  9/13

  Elixir        : 表になし(発表文の自己測定 12/13)

12/13が事実なら、Typed Racketと同格でTypeScriptより上ということになります。アノテーションが一切ないコードでそこまでの絞り込み精度が出るなら、実際に印象的な結果です。ただし現状では、著者自身の自己測定であり、条件と失敗項目が公開されておらず、リンク先の表では照合できないという注記を付けてこそ正確です。

コンパイル時間 — 「最速」主張の実際の大きさ

発表文にはもう一つ主張があります — 「我々の合成ベンチマークでは、ElixirのビルドツールはいまやBEAM言語のなかで最速だ」。

根拠はJosé Valim本人のリポジトリjosevalim/langcompilebenchです。著者自身の測定であり、リポジトリ自体が「合成ベンチマーク(synthetic benchmarks)」だと明記しています。測定対象は独立した100モジュール、それぞれhello worldな関数を100個コンパイルし、アプリケーションを起動し、最小限のテストスイートを走らせる時間です。条件はMacStudio M1、5回平均です。

Erlang/OTP 28 基準
  Elixir v1.19                        ~0.73s
  Elixir v1.20                        ~0.63s
  Elixir v1.20 (interpreted defmodule) ~0.58s
  Erlang (rebar3)                     ~0.72s
  Gleam v1.14                         ~0.71s

Erlang/OTP 29 基準
  Elixir v1.19                            ~0.65s
  Elixir v1.20-rc.2                       ~0.55s
  Elixir v1.20-rc.2 (interpreted defmodule) ~0.50s
  Erlang (rebar3)                         ~0.64s
  Gleam v1.14                             ~0.67s

数字をそのまま読めば — 1.19から1.20になって0.73秒が0.63秒になり、Erlangの0.72秒とGleamの0.71秒を上回っています。これは事実です。同時に、作業全体が0.7秒程度で、差は0.1秒前後だということも事実です。そしてこのワークロードはhello world関数の塊であって実際のコードではありません — 型チェックを重く走らせるようなコードは、そもそも存在しないのです。

著者本人がリポジトリに残した注記をそのまま持ってくるのが最も誠実です。

もちろん、これは同規模のElixirプロジェクトがGleamやErlangのプロジェクトより速くコンパイルされるという意味ではありません。生のコンパイラ性能以外にも変数があるからです。(…) 理論的に言えば、rebar3がこの中で最も良い性能を出すべきです。

増分コンパイルに移ると、順位は完全にひっくり返ります。同じリポジトリの分析によれば、モジュール間の依存関係をコンパイル時/ランタイムで区別できるかどうかで差がつきます。Erlangは(まれにしか使われないparse transformを除けば)ランタイム依存だけなので、ここに登場する言語の中で増分性能が最も良くなります。 ファイルを1つ変えれば、そのファイルだけが再コンパイルされます。Gleamはすべての依存をコンパイル時として扱うので最も悪くなります。Elixirはその中間です。

langcompilebenchの整理表
  言語     | 依存の種類              | 循環許可 | 変更ごとの想定再コンパイル
  Erlang   | ランタイムのみ          | あり     | 最小
  Elixir   | ランタイム + コンパイル時 | あり     | 中程度
  Gleam    | コンパイル時のみ         | なし     | 最大

つまり「最速」という主張はクリーンビルドの合成ベンチマークに限った話であり、開発中に実際に体感する増分ビルドではErlangが上だというのが、同じリポジトリ自身の結論です。発表文だけを読むと見落とす文脈です。

タダではない部分

文書には書かれているのに、発表文には出てこないトレードオフです。

dynamicは常にルートに現れる。 公式ドキュメントの説明どおり、{:ok, dynamic()}のようなタプルを書くと、Elixirはこれをdynamic({:ok, term()})に書き換えます。文書が明示する欠点はこれです — タプル・マップ・リストの一部だけをgradualにすることはできず、全体がgradualになります。 その代わりdynamicが常にルートに明示的に現れるので、静的に型付けされたプログラムにdynamicがこっそり忍び込むのを防いでくれるというのが利点として提示されています。意図された設計判断ですが、精度を差し出す取引であることは間違いありません。

構造体の更新は設計上、違反を出す。 文書自身が挙げている例です。

user = find_user_by_id(42)
%User{user | name: "John Doe"}

find_user_by_idがランタイムでは常にUser構造体を返すとしても、型システムがそれを静的に証明できなければ型付け違反を出します。文書の表現では「構造体の更新はこう動くように設計されている」とのことです。解決策は、変数を定義する際にマッチさせておくことです。

%User{} = user = find_user_by_id(42)
%User{user | name: "John Doe"}

「偽陽性率が極めて低い」という発表文の主張は、数値なしで提示されたベンダー自己評価であり、こういう形でコードを手直ししなければならない箇所が残っていることと合わせて見るべきです。

interpreted defmoduleには代償がある。 上のベンチマークで最速の数字を出したmodule_definition: :interpretedオプションは、発表文では利点しか触れられていませんが、CHANGELOGには欠点が書かれています。

• コンパイル中に発生するエラーのスタックトレースが、精度が落ちる場合がある
• defmodule内の無名関数が受け取れる引数は最大20個まで(defなどで定義した関数自体は引き続き255個まで可能)

デフォルトは:compiledで、有効にするにはmix.exsにelixirc_options: [module_definition: :interpreted]を入れます。.beamファイル自体は変わりません — defmoduleの内部を実行する方式だけが変わります。

アップグレード前に知っておくべきこと

OTP要件。 1.20はErlang/OTP 27以上を要求し、OTP 29と互換性があります。OTP 26以下に縛られている場合、1.20はそもそも選択肢になりません。

セキュリティパッチは1.20にしかない。 1.20.1(2026年6月9日)でCVE-2026-49762(GHSA-w2h8-8x3g-278p、深刻度medium、Erlang Ecosystem Foundation発行)が修正されました。内容はVersionモジュールでの無制限な整数パースです。バージョン文字列の数値構成要素を長さ制限なしに整数へ変換していたため、すべて数字からなる1つの大きな構成要素があると超線形かつ非譲歩的(non-yielding)な変換が起き、BEAMスケジューラを1つ占有し続け、さらに大きければSystemLimitErrorでプロセスが落ちます。OSVの記録によれば、1メガバイト程度の文字列1つで十分で、認証も不要です。 到達経路はVersion.parse/1、Version.parse!/1、Version.match?/3、Version.compare/2、Version.parse_requirement/1で、HTTPパラメータやパッケージメタデータのような信頼できない入力にこれらの関数を呼ぶアプリが対象です。修正は整数構成要素を10進14バイトに制限するというものです。

ここで重要な点 — 影響範囲は1.5.0から1.20.1未満のすべてです。ところが確認すると、2026年6月9日以降にリリースされたのは1.20.1と1.20.2だけで、v1.19.6やv1.18.5のタグは存在しません。つまりこの脆弱性の修正を受けるには、1.20.1以上に上げる以外に方法がありません。 1.19以下にとどまる計画なら、Elixirチームの推奨どおり、Versionモジュールに渡すデータのサイズを自分で制限する必要があります。

ハード非推奨。 1.20で実際に警告を出し始めるものです。

• File.stream!(path, modes, lines_or_bytes) → File.stream!(path, lines_or_bytes, modes)へ引数順序を変更
• ビットパターン内でサイズをマッチさせる際にピン演算子が必要に: <<x::size(^existing_var)>>
• Kernel.ParallelCompiler.async/1 → Kernel.ParallelCompiler.pmap/2
• Logger.*_backend系の関数 → ハンドラ方式へ(引き続きバックエンドを使うには:logger_backendsパッケージ)
• Logger.enable/1、Logger.disable/1 → Logger.put_process_level/2、Logger.delete_process_level/1
• mix.exsのxref: [exclude: ...] → elixirc_options: [no_warn_undefined: ...]

潜在的な破壊的変更が2つ。 文字列・コメントおよび?直後での生のCR改行がセキュリティ上の理由で禁止され、require SomeModuleはコンパイル時にそのモジュールへ展開されなくなりました(ランタイムにモジュールを返すのは変わりません)。CHANGELOGがわざわざ後者を書いているのは、require(SomeMod).some_macro()のようなコードが壊れうるからです。

型シグネチャはなぜまだ遠いのか

最も気になる質問 — @specの代わりにコンパイラが強制する型シグネチャをいつ使えるようになるのか。

発表文は条件を4つ挙げています。型シグネチャは次がすべて満たされたときにだけ導入されます。

1. 1.20の型システムの性能に満足したとき
2. 再帰型(recursive types)を効率的に実装できるとき
3. パラメトリック型(parametric types)を効率的に実装できるとき
4. マップのキー・値ペアの走査をenumerableとして効率的に実装できるとき — ここはまだ解法を研究中だと明記されています

つまり残っているのはエンジニアリングだけではなく、未解決の研究課題だということです。1月のロードマップ記事は、これらの問題をv1.21(2026年11月)とv1.22(2027年5月)で探ると述べたうえで、型システムが実用的でないと判明しうるリスクを2つ自ら書き記しています — エルゴノミクス(ここまでの改善はすべて言語変更なしに舞台裏で起きており、開発者体験への影響はまだ評価されていない)とパフォーマンス(現在の実装は再帰型・パラメトリック型をサポートしておらず、これらが性能を直接損なう可能性がある)です。

残りのマイルストーンの順序はこうです。2番目は型付き構造体(typed structs) — 構造体フィールドの型をネイティブに定義し、コードベース全体に伝播させること。3番目が集合論的型シグネチャです。

そしてここに、静かながら大きなニュースが1つあります。公式ドキュメントが明示している内容です — 既存のErlang Typespecは集合論的型に使うには十分な精度がなく、この段階が終わると言語から段階的に取り除かれ(phased out)、後処理は別ライブラリへ移されます。 @specを熱心に使ってきたコードベースなら、いずれ移行がやってくるという意味です。時期は決まっていません。

では今、何をすべきか

上げてよい場合。 OTP 27+にいて、上のディプリケーション一覧が対応可能な範囲なら、上げる理由は十分にあります。型チェックはオプトインではなく、ただ有効になっており、コードを直さなくても構いません。得られるものはほぼタダです。さらにVersionのCVEパッチは1.20.1以上にしかないので、Versionモジュールに外部入力を渡すアプリなら、アップグレードは事実上セキュリティ案件です。

急ぐ必要がない場合。 型シグネチャを使いたくて待っていたのなら、1.20はそれではありません。少なくともv1.21(2026年11月)、現実的にはそれ以降で、研究課題が解けなければさらに遅れる可能性があります。構造体の型もまだです。OTP 26以下に縛られているなら、そもそも上げられません。

期待値の調整。 1.20が見つけてくれるのは「実行すれば必ず落ちる」違反とデッドコードです。型が正しいと証明してくれるわけではありません。アノテーションがない以上、コンパイラが知っているのはコードから推論できることだけで、あいまいな箇所はdynamic()のまま残り、互いに素なときだけ引っかかります。Dialyzerを使ったことがあるなら見覚えのある位置ですが、違いはElixir 1.20がコンパイラに組み込まれていて、別実行やPLTビルドが不要な点です。

アップグレード後に警告が大量に出るなら、その多くは本物のバグである可能性が高いです。発表文の最後の一文が言っているのはそういうことです — 「Elixir v1.20を試してみて、タダで見つかったバグを直すのを忘れないように」。

おわりに

まとめるとこうなります。Elixir 1.20は2022年に始まった型システム作業の最初のマイルストーンを実際に終えており、これは本物です — アノテーションなしですべてのプログラムを漸進的に型チェックし、dynamic()が型情報を捨てる代わりに範囲として絞り込まれ、ガード・関数本体・節・依存関係をまたいで推論が流れます。コストは実質的にアップグレードそのものだけです。

同時に、発表文の2つの数字は一次資料に照らすと大きさが変わります。If-Tの「13個中12個」は、リンク先の上流表にElixirの列すら存在しない自己測定値であり、コンパイル速度1位は著者本人のhello world合成ベンチマークで、0.7秒の作業における0.1秒の差にすぎず、増分ビルドでは同じリポジトリがErlangを上に置いています。どちらの主張も嘘ではありませんが、発表文だけを読んで受け取る印象より小さいものです。

そして本当に欲しいもの — 型シグネチャと型付き構造体 — は、まだ1年以上先にあり、Elixirチーム自身が「実用的でないと判明する可能性がある」と書いた未解決の研究課題の向こう側にあります。その正直さこそが、このプロジェクトが4年経っても信頼を保っている理由でもあります。

参考資料

• Elixir v1.20 released: now a gradually typed language (2026-06-03, José Valim)
• Elixir v1.20 CHANGELOG (一次資料)
• Type inference of all constructs and the next 15 months (2026-01-09) — ロードマップとRCスケジュール
• Gradual set-theoretic types — 公式ドキュメント(v1.20.2)
• The Design Principles of the Elixir Type System — Castagna, Duboc, Valim (Programming journal, 2024, Vol. 8, Issue 2, Article 4)
• If-T: A Benchmark for Type Narrowing — Guo, Greenman (arXiv:2508.03830)
• utahplt/ifT-benchmark — 上流ベンチマークと結果表
• josevalim/langcompilebench — BEAM言語のコンパイル時間合成ベンチマーク
• CVE-2026-49762 / GHSA-w2h8-8x3g-278p — Versionモジュールの無制限整数パース
• モダン Elixir & Phoenix 2026 — 生態系の見取り図(関連記事)
• モダン Erlang と BEAM 2026 — OTPとランタイム(関連記事)