Elixir 1.20の型システムをRust,TypeScriptと比べたら特徴が見えてきた

この記事について

2026年6月3日、Elixir 1.20 が公開され、型システムが入りました。ただ、これは「型を書いて安全を得る」これまでの型システムとは、目指すものが少し違います。

この記事は、私の疑問に対して AI エージェントが調べてまとめたものです。公式ブログ・ドキュメント・論文といった一次資料に当たり、最後は Elixir 1.20 を実際に入れて型検査の挙動も確かめました。とはいえ正確でない部分もあるかもしれないので、気づいた点があればコメントで指摘いただけると嬉しいです。

型システムが目指す「sound」

まず「sound」という言葉から。sound というと「音」や「That sounds good（いいね）」が浮かぶと思いますが、型システムの sound はそれとは別語源で、「穴がない・健全な」という意味です（safe and sound＝無事で、a sound argument＝穴のない論証）。日本語なら「健全」。

型システムでの sound は「型が『この型だ』と言ったら、実行時に型エラーは起きない」という性質です。逆に unsound は、型が通っても実行時に型エラーが起きうること。

動的な言語で完全に sound にするのは難しく、TypeScript は公式に「sound にしない」と unsound を公言しています。一方 Elixir は、sound を型システムの目標の一つに挙げています。ただしこちらも「すべての間違いを見つける保証はしない（best-effort）」と認めていて、「完全に sound だ」と公言しているわけではありません。どちらも sound／unsound という言葉で型システムを語るので、この記事でもその言葉で揃えます。

sound をどこまで・どう目指すかには、立場があります。鍵は「わからないものをどう扱うか」です。

	sound か	わからないものを
Rust	sound（強い）	却下する
Elixir	sound（best-effort）	通す
TypeScript	unsound	通す

Rust は、わからないものを却下します（通さないので、型と所有権については強く sound。ただし unsafe の部分や、配列の範囲外のような実行時のエラーは保証の外です）。

TypeScript と Elixir は、どちらもわからないものを最終的には通します。違うのは、通すまでの過程です。TypeScript はできるだけ型を書くことを求める設計で、型情報のないところ（any や as で不明になった部分）はサポート対象外として、調べずに通します。Elixir は、通す前にコードの流れ（分岐やガード）をたどって型の可能性を調べ、確実に失敗すると分かったものだけ却下します。同じ「通す」でも、調べてから通すかどうか。その差が、unsound（TypeScript）と sound（Elixir）を分けます。

Elixir 1.20 の型システム

特徴は三つです。

1. dynamic() で判定を遅らせる。 型情報のないところを、TypeScript は検査せずに通します（型を書くことを前提とした設計で、書かれていないところはサポート対象外だからです）。Elixir は、不明なところに「不明（dynamic()）」という型をあてはめ、判定を保留する。その値はコードを流れる中で絞り込まれ、「どの値が来ても必ず失敗する」と確定したところだけ報告する。一部のパスでだけ失敗しうる段階では報告しません。確実なことしか言わない、偽陽性を出さない設計です。グレーのまま終われば見逃しますが（公式も「すべての間違いを見つける保証はしない」と認める best-effort）、報告したものは確実、という側に振ってあります。

2. 否定を型で書ける。 Elixir の型は集合の演算、和・積・否定でできています（set-theoretic types）。「nil ではない」のような否定を素直に書ける。TypeScript にも Exclude や絞り込みで「これを除く」表現はありますが、Elixir は否定そのものを型の演算として持つ。そこが違います。

3. 型を書かないことから始める。 いまは型注釈を書かなくても、コンパイラがコードから型を推論して検査します。既存の膨大なコードに、何も足さずに効かせるためです。将来は、強い保証が欲しい境界に型シグネチャを書けるようにする予定で（公式のロードマップ）、今回の 1.20 は「まず推論」のマイルストーンにあたります。なお、昔からある @spec はドキュメントと Dialyzer 向けで、新しい型システムは使いません。新しい型シグネチャは、これとは別物として設計されます。

将来、型を明示的に書けるようになれば、いまは追えない範囲（struct のフィールドや、モジュールをまたぐ境界）にも保証が広がると見込まれます。ただ、開発元自身も「書き心地への影響はこれから評価する」「型システムが実用的でないと判明する可能性もある」と慎重で、まだ検証中です。型を書ける未来で良くなる「はず」だが、作っている本人たちもまだ手探りのようです。

型を書かずに、ここまで検知する（動かしてみた）

実際に Elixir 1.20 を入れて、型を一行も書かずに何を検知するか試しました。

たとえば、case の全分岐がアトムを返すと、結果はアトムだと推論され、文字列を扱う関数に渡したところで止まります。Elixir では文字列のことを「バイナリ」と呼ぶので、警告にも binary() と出てきます。

def categorize(n) do
  label =
    case n do
      x when x < 0 -> :negative
      0 -> :zero
      _ -> :positive
    end
  String.length(label)
end

warning: incompatible types given to String.length/1:
    given types:     dynamic(:negative or :positive or :zero)
    but expected one of:     binary()

パイプラインでも、途中で変わる型を追います。

def pipeline(n) do
  n
  |> Integer.to_string()   # 整数を文字列にする（Elixir では文字列を「バイナリ」と呼ぶ）
  |> Kernel.+(1)           # 文字列（バイナリ）に整数を足そうとして警告
end

warning: incompatible types given to Kernel.+/2:
    given types:     binary(), integer()
    but expected one of:     integer(), integer()   # ほか数値同士の組み合わせ

どちらも型注釈はゼロです。case の3つの分岐を :negative or :positive or :zero と束ね、パイプの型変化を追って、「どの値でも必ず失敗する」一点だけを指してくる。

正直に書くと、「TypeScript では見逃すが Elixir だけが検知する」例を作ろうとしましたが、うまく作れませんでした。型の不整合は TypeScript も検知しますし、配列の境界外のような unsound なケースは Elixir も（best-effort で）見逃します。違いは検知できる範囲ではなく、この例のための型を一行も書いていないのに検知できる点です。

つきつめると、静的な型の言語だけでよいのでは？

ここまで動かしてみて、根っこの疑問が出てきました。Rust のような静的な型の言語があるなら、つきつめれば、それだけでよいのではないか。動的な型の言語は、そもそもなぜ要るのか。確かめたくて、AI エージェントに聞いてみました。返ってきたのが、次の回答です。

まず、問いを少し分けさせてください。Rust の重さは、静的な型そのものより、所有権とライフタイム（GC を持たずにメモリ安全を取る仕組み）から来ています。GC を持つ静的言語なら型推論も効いて、注釈はほとんど書かずに済む。だから本当の対立は「Rust か 動的か」ではなく「静的か 動的か」で、その中間に GC 付きの静的言語がいます。

正直に言うと、「静的だけでいい」側は、いま強くなっています。型推論が進んで「動的のほうが速く書ける」差は縮みましたし、TypeScript や Python、そして Elixir 1.20 のように「動的言語に後から型を足す」流れは、コードが大事になれば結局は静的な保証を欲しがる、という証拠でもあります。

それでも、動的な型が原理的に消えない理由が二つあります。

1. 健全な静的型は、正しく動くプログラムを必ず一部はじく。 「実行時に型エラーを起こさないか」は一般には判定できない（ライスの定理）ので、安全でないものを通さないことを優先すると、その代償として「本当は動くのに、証明できないから却下する」コードが必ず残ります。型システムを良くすれば消える欠点ではなく、原理的な天井です。証拠に、どの静的言語にも逃げ道（Rust の unsafe、各言語の Any や動的キャスト）がある。静的で覆いきれない部分を認めて、動的を持ち込んでいるわけです。

2. 型が実行時にしか決まらない仕事がある。 外から来る雑多なデータ、対話的に試す REPL、コードを生成するマクロ、動かしたまま差し替えるホットコードリロード。どれも性質からして動的で、「全体を事前に検査する」前提とぶつかります。

まとめると、静的と動的は「型の正しさの代金を、どこで払うか」が違うだけです。静的はコンパイル時に、あらゆる実行について前払いする。動的は実行時に、起きたその一回について後払いする。前払いできない、あるいは前払いが割に合わない場面があるから、動的は要る。そして現実の答えは「どちらか」ではなく、「動的を土台にして、効くところだけ静的を足す」に向かっています。

この回答を読んで、Elixir 1.20 の存在意義と立ち位置がちょっとわかりました。

Elixir は Rust になろうとしているわけではありません。動的のまま走れる土台を残し、確実な間違いだけを静的に止め、将来は保証が欲しい境界に型を足せるようにする。回答でいう「動的を土台に、効くところだけ静的を足す」を、言語の設計として選んでいる。

そして、これは AI にコードを書かせる時代とも重なります。AI は速く大量に書けますが、すべてを完全に作り切れるわけではありません。そこで型システムが、決定的に見つかる間違いをコンパイラのレベルで確実に指摘し、AI が作り切れていない部分をアシストする。Elixir 1.20 の型システムは、その一つの形に見えます。

参考

• Elixir v1.20 released: now a gradually typed language（公式リリースブログ）
• Gradual set-theoretic types（公式ドキュメント。sound の記述、best-effort、typespecs の phase out）
• Typespecs reference（@spec の役割＝ドキュメントと Dialyzer 向け）
• Type inference of all constructs and the next 15 months（ロードマップ）
• Giuseppe Castagna, Guillaume Duboc, José Valim, "The Design Principles of the Elixir Type System"
• TypeScript Design Goals（非目標に「健全（sound）な型システムにはしない」と明記）