【この記事の読み方】

本記事は、「等しさ」を型でどこまで扱えるかを追いかけるシリーズ（全３回）の第１回です。分量が多いため、先に読み方を示しておきます。

Python の具体例と問題提起だけ知りたい方は、「Executive Summary」から「この記事で扱うこと」までをお読みください。
型理論や定理証明支援系に興味のある方は、「どの部で、何を扱うか」以降で、Rocq のコード例と７言語の比較表をご覧いただけます。

また、本記事で扱う「等しさ」には、実行時の比較演算子 ==、コンテナ利用のための同値関係、依存型理論における等号型という、異なる層があります。本記事では、これらを同一視せず、各層で「何を処理系が保証できるか」を比較していきます。

Executive Summary ── ３分で分かる本記事の全体像

プログラムが「等しい」と判定する基準は、プログラマの想定と食い違うことがあります。

例えば、あるサービスの利用者名を集めたPythonのset型（集合型）に、"Alice" の名前が含まれているとき、"alice" で検索しても見つかりません。

（Pythonのset型（集合型）は、重複する要素を持たず、順序がない組み込みデータ型です）

このケースでは、「利用者名は、大文字・小文字を区別しない」というアプリケーション仕様が想定されていました。

しかし、その同一視の規則（正規化の規則）は、実装コードのどこにも表現されていませんでした。それが原因です。

そのため、コードの中で定義されたset型は、文字列の完全一致（大文字・小文字を別の文字として識別）で検索が走る仕様になってしまっていたのです。

users = {"Alice", "bob"}
print("alice" in users)

実行結果です。

False

もう１つ、プログラマの想定した挙動と乖離した挙動を示すコードが生まれてしまう事例を見てみましょう。

今度は、浮動小数点の計算精度に起因する事例です。
登場するデータ型は、Pythonのdict（辞書）型です。

例えば、$0.1 + 0.2$ を辞書のキー（Key）にして、$0.3$というキーで取り出そうとすると、KeyError が返される状況を考えてみましょう。

d = {}
d[0.1 + 0.2] = "値"

print(d)
print(d[0.3])

実行結果です。

{0.30000000000000004: '値'}
Traceback (most recent call last):
  File "example.py", line 5, in <module>
    print(d[0.3])
          ~^^^^^
KeyError: 0.3

このケースでは、プログラマは、実行するまで、この状況でエラーが吐かれると事前に予想することはできませんでした。

計算機は小数を二進法で表すため、$0.1$ も $0.2$ も、わずかな誤差を含んだ値として保持されます。

$0.1$ と $0.2$ を足し合わせた結果は $0.30000000000000004$ であり、$0.3$ と一致しないのです。

これが、このケースで発生したエラーの原因です。

さらに別の事例も見てみましょう。

print(type(1))        # 型を確認
print(type(True))

s = {1, True}         # set型のデータに、両方を入れる
print(s)
print(len(s))

実行結果です。

<class 'int'>
<class 'bool'>
{1}
1

型は違います。 int と bool です。

それでも、set型のデータに入れると１つにまとめられました。

set型は重複を許さない入れ物です。

Python が 1 と True を同じものと判定したため、片方だけが残っています。

「型が違うのだから別のものだろう」というプログラマの理解と、言語が採用している等しさが、ここで食い違っています。

あともう一つ例を挙げてみたいと思います。

print([1, 2, 3] == (1, 2, 3))    # False

中身は同じ３つの数 です。

しかし、リストとタプルは等しくないと判定されます。

先ほどの 1 と True の例では、整数の 1 と、真偽値の True は、型が異なるにもかかわらず、等しいと判定される挙動を見せていました。

しかし、今回は、要素の並びは同じ（”1, 2, 3”）であっても、list型とtuple型は型が異なり、互いに等しくないという等値判定の結果が出力されました。

同じ言語の中で、「型が違っても等しい」場合と、「型が違うから等しくない」場合が、同居している のです。

では、このような プログラマの想定（頭の中）と食い違っている実装コードを、実行する前の静的解析・型検査の段階で、型検査器に見つけさせること は 可能でしょうか？

結論から言うと、通常の静的型検査だけでは、ドメイン固有の等値性――たとえば大文字・小文字を無視すべきか、浮動小数点の近似を許すべきか――を検証することはできません。一方で、Python の静的型チェッカー（mypy など） の厳格設定は、型の重なりがない比較など、一部の明白な誤りであれば警告できます（この点は後述します）。

そのことを確認するために、ここまで見てきたコード例を mypy に検査させた結果 を見てみたいと思います。

まずは、ここまで見てきた４つの事例を、１つのファイルにまとめます。

eq_check.py

# eq_check.py

users = {"Alice", "bob"}
print("alice" in users)

print(type(1))
print(type(True))
s = {1, True}
print(s)
print(len(s))

print([1, 2, 3] == (1, 2, 3))

d = {}
d[0.1 + 0.2] = "値"
print(d)
print(d[0.3])

上記のPythonスクリプトファイルを、mypy に検査させます。

$ mypy eq_check.py
Success: no issues found in 1 source file

一件の指摘もありません。

しかし、このスクリプトを実行させると、Falseや、最後の実行結果では実行エラー（異常終了）が起きてしまいます。

$ python3 eq_check.py
False
<class 'int'>
<class 'bool'>
{1}
1
False
{0.30000000000000004: '値'}
Traceback (most recent call last):
  File "eq_check.py", line 15, in <module>
    print(d[0.3])
          ~^^^^^
KeyError: 0.3

４つとも、プログラマの想定と食い違った結果が出ています。

最後の例では、プログラムが停止しました。

しかし、mypy チェックの結果は、問題事項は指摘されませんでした。

Success: no issues found in 1 source file

このような結果となったのは、型チェッカーが確認しているのは、コードで宣言された型と、そこへ実際に渡されたデータの型が一致しているかどうか。ただそれだけだから です。

１つずつ確かめてみましょう。
まず最初に、以下のコードです。

users = {"Alice", "bob"}
print("alice" in users)

users は文字列を集めた set型です。
そこへ渡した "alice" も文字列です。

型として、何の問題もありません。

次は、dict型（辞書型）のデータを宣言して、キーと値の挙動を確認するコードです。

s = {1, True}

set型に整数と真偽値を入れています。
Pythonでは、bool は int の派生型なので、どちらも整数として扱うことができます。
型として、問題ありません。

次は、以下のコードです。

print([1, 2, 3] == (1, 2, 3))

== は、どんな型の値どうしでも比較できます。
list型とtuple型を比べること自体は、型として許されています。

なお、mypy に --strict を付けると、リストとタプルの比較については指摘が出ます。

$ mypy --strict eq_check.py
eq_check.py:10: error: Non-overlapping equality check (left operand type: "list[int]", right operand type: "tuple[int, int, int]")  [comparison-overlap]
Found 1 error in 1 file (checked 1 source file)

「重なりのない型どうしを、等値比較している」という指摘です。

list[int] と tuple[int, int, int] は、共通する値を持ちません。
したがって、この比較は必ず False になります。
mypy は、そのことを警告しています。

これは、--strict を指定した型チェッカーによって、プログラマがコードの誤りに気づける例でした。

ただし、mypy が指摘しているのは「この２つの型に共通の値がないため、比較しても必ず False になる」という点だけです。

「リストとタプルを等しいとみなすべきかどうか」という判断について、mypy は何も述べていません。

最後は、このコードでした。

d = {}
d[0.1 + 0.2] = "値"
print(d[0.3])

d[0.1 + 0.2] の 0.1 + 0.2 は浮動小数点数です。
d[0.3] の 0.3 も浮動小数点数です。

型としては、何の問題もありません。

ここまで取り上げてきた４つのコードに関する考察をまとめます。

４件のコード事例はすべて、引数として渡したデータ型は、型としては、どれもコードが期待する「仕様通り」の正しいものでした。

しかし「何をもって等しいとするか」という判断は、型の外側にあります。

大文字・小文字を区別しないという設計上の判断。
整数と真偽値を別のものとして扱いたいという理解。

いずれも、コードのどこにも書かれていません。
書かれていないものを、型検査器が確かめることはできないのです。

型が違っても等しいと判定される場合と、型が違うから等しくないと判定される場合。 その両方を、mypy は素通しします。
（後者については、mypyを実行する際に、コマンドライン引数に --strict を指定することで、型が一致しないことをmypyに検出してもらうことができます）

コード	実行結果	想定との食い違い	mypy（既定）	mypy（`--strict`）
`"alice" in users`	`False`	大文字・小文字を区別するかどうか	指摘なし	指摘なし
`{1, True}`	`{1}`	整数と真偽値を別のものとするかどうか	指摘なし	指摘なし
`[1,2,3] == (1,2,3)`	`False`	list型とtuple型を別のものとするかどうか	指摘なし	指摘あり
`d[0.3]`	`KeyError`	計算結果の誤差を許容するかどうか	指摘なし	指摘なし

mypyに、--strictを付けることで指摘を受けることができるのは、リストとタプルの比較結果だけです。

他の3つの事例はいずれも、比較している２つの値が同じ型に属します。

"Alice" と "alice" は、どちらも文字列です。
1 と True は、bool が int の派生型であるため、整数として扱うことができます。
0.1 + 0.2 と 0.3 は、どちらも浮動小数点数です。

型として矛盾がない以上、mypy には判定の手がかりがありません。

ここまでは、Pythonに視野を閉じた議論を展開してきました。

ここからは視野をぐっと広げていきます。

Python以外の他の言語（関数型言語や定理証明支援系）だと、実行する前のコンパイル時点で、「等しさ」をより高精度に、型で見抜くことができる能力を備えているのでしょうか？

この記事ではこの論点を論じてみたいと思います。

例えば、Rust では、浮動小数点数を辞書のキーにしようとした時点でコンパイルが止まります。

// float_key.rs

use std::collections::HashMap;

fn main() {
    let mut map: HashMap<f64, String> = HashMap::new();
    map.insert(0.1 + 0.2, String::from("値"));
    println!("{:?}", map);
}

コンパイルしてみます。
（検証環境：rustc 1.75.0）

$ rustc float_key.rs
error[E0599]: the method `insert` exists for struct `HashMap<f64, String>`, but its trait bounds were not satisfied
 --> float_key.rs:5:9
  |
5 |     map.insert(0.1 + 0.2, String::from("値"));
  |         ^^^^^^
  |
  = note: the following trait bounds were not satisfied:
          `f64: Eq`
          `f64: Hash`

error: aborting due to previous error

f64: Eq が満たされていない、と指摘されています。

Eq は、Rust において「等しさが完全に成り立つ型」であることを表すものです。

浮動小数点数は、これを満たしません。

HashMap は、キーの型に Eq を要求します。

だから、コンパイルが止まるのです。

（正確に述べると、標準の f32／f64 が Eq と Hash を実装していないため、標準の HashMap のキーには使えない、ということです。ラッパー型を使うなど、意図的に選んだ別の等値性で浮動小数点数を扱う道は残されています。）

ここで見たように、Rust では、Python にはない検査が働きます。

HashMap のキーとして使える型は、Eq を実装しているものに限られます。
そして、その要求はコンパイル時に確かめられます。

ただし、注意すべき点があります。

Rust が確かめているのは、 「その型が Eq を実装していることが宣言されているか」どうかまで です。

Eq は、PartialEq の上に載る中身が空のトレイト（マーカートレイト）であり、実装するとは「この型の等値比較は、反射性を含む数学の等しさの条件を満たす」と宣言する契約を結ぶことを意味します。なお、HashMap のキーには実質的に Eq と Hash の両方が要求され、Hash には「等しい値は同じハッシュ値を返す」という整合性が求められます。

その宣言が事実かどうかを、コンパイラは検査してくれません。

数学の等しさの条件を実際に満たすようにコードを書くかどうかは、あくまでもプログラマに委ねられているのです。

つまり Rust は、 「等しさの条件を満たす型かどうか」 を 型のレベルで区別 します。

しかし、「本当に満たしているか」までは踏み込みません。

この区別が、本記事の第１部の主題になります。

Lean であれば、さらに踏み込んだ検査が可能です。

Lean は、「等しい」という主張そのもの を 型として宣言 した上で、その主張が成り立つことを示す証明をコードとして記述 し、さらに Lean処理系が、その証明が正しいかどうかを検証するところまで行ってくれる のです。

Lean のコード例を見てみましょう。

-- eq_lean.lean

theorem add_zero_ok (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ m ih => simp

theorem add_zero_ok (n : Nat) : n + 0 = n の部分が、証明したい主張です。

「どんな自然数 n についても、n + 0 は n に等しい」と読みます。

:= by の後が、その証明です。

この証明式が成立するかどうか、処理系に検査させます。

$ lean eq_lean.lean

何も出力されません。

これは、証明が通った（証明成立）ということです。

では、成り立たない主張を書くと、どうなるでしょうか？

-- eq_lean2.lean

theorem wrong (n : Nat) : n + 1 = n := by
  induction n with
  | zero => rfl
  | succ m ih => simp

n + 1 = n という、成り立たない主張です。

検査させてみます。

$ lean eq_lean2.lean
eq_lean2.lean:4:12: error: tactic 'rfl' failed, the left-hand side
  0 + 1
is not definitionally equal to the right-hand side
  0
case zero
⊢ 0 + 1 = 0
eq_lean2.lean:5:14: error: unsolved goals
case succ
m : Nat
ih : m + 1 = m
⊢ False

「0 + 1 と 0 は等しくない」と指摘されました。

Lean は、書かれた主張が本当に成り立つかどうかを検査します。

宣言するだけでは Lean の検証を通りません。

証明を書き、その証明が正しいことを確かめて、初めて Lean の検証を通過するのです。

前述のLean 4のコードについて、以下の ３つの段階がコードの中でどう実装されているのか、順に見ていきます。

① 主張を、型として宣言する
② 証明を、コードとして記述する
③ 処理系が、証明の正しさを検証する

① 主張を、型として宣言する

theorem ok (n : Nat) : n + 0 = n

n + 0 = n の部分が、型です。

「どんな自然数 n についても、n + 0 は n に等しい」という主張が、そのまま型として書かれています。

② 証明を、コードとして記述する

:= by
  induction n with
  | zero => rfl
  | succ m ih => simp

:= by の後が、証明にあたる部分です。

n がゼロの場合と、そうでない場合に分けて示しています。

③ 処理系が、証明の正しさを検証する

誤った証明を書くと、どうなるでしょうか。
すでに見た反例（証明が成立しない例）とは別の反例を掲載します。

-- chk5.lean

theorem bad2 (n : Nat) : n + 0 = n := by
  induction n with
  | zero => exact Nat.zero_lt_one
  | succ m ih => simp

Nat.zero_lt_one は、「$0 < 1$」という別の主張の証明です。

検査させます。

$ lean chk5.lean
chk5.lean:3:12: error: type mismatch
  Nat.zero_lt_one
has type
  0 < 1 : Prop
but is expected to have type
  0 + 0 = 0 : Prop

「渡されたのは 0 < 1 の証明だが、ここで必要なのは 0 + 0 = 0 の証明である」と指摘されました。

証明として提出したものが、示すべき主張と対応していない。それを処理系が検出しています。

ここまで、Lean 4 は、以下の ３つのステップ をすべて、型検査・証明検査を担う処理系の中核部分がチェックする言語であることを確認しました。

① 主張を、型として宣言する
② 証明を、コードとして記述する
③ 処理系が、証明の正しさを検証する

なぜ言語によって、このような大きな差が出るのでしょうか。

理由は、２つあります。

第１に、「等しさ」が１種類ではないこと。

第２に、複数ある「等しさ」のうち、どこまでを型として宣言できるかが、言語ごとに違うこと。

まず、１つ目から述べます。

完全一致か
大文字小文字を無視するか
誤差を許容するか
計算だけで確かめられるものか、証明を書かないと示せないものか

これらは、互いに異なる複数の「等しさ」 です。

複数ある異なる「等しさ」 の それぞれ を、型として宣言すること はできるのか？

これがひとつの論点となります。

そして、この 「異なる等しさ」を、言語がどこまで捉えることができるのか、言語ごとの「異なる等しさ」を識別する解像度 にも、段階があります。

なお、以下で述べる「第１段階〜第４段階」という区分は、型理論に公式に存在する分類ではなく、本記事の議論を整理するために筆者が導入した独自の整理です。

第１段階 ── 型として区別する

浮動小数点数は、辞書のキーとして使ってよい型なのでしょうか？
Rust は、これを 型のレベルで判定 します。

use std::collections::HashMap;

let mut map: HashMap<f64, String> = HashMap::new();

このコードは、コンパイルが通りません。

Rust は等しさに関するトレイトを２つに分けており、辞書のキーには条件の強いほうを要求します。 浮動小数点数は、その条件を満たしません。

詳しくは、本連載シリーズの第１部で扱います。

第２段階 ── 約束として宣言させる

「この型の等値比較は、数学の等しさの条件を満たす」と、プログラマが コードに書いて宣言 します。

言語処理系は、その宣言があるかどうか しか、確認してくれません。

宣言の中身が事実かどうかは、言語処理系は検査してくれない、ということ です。

その結果、嘘の宣言を書いても、コンパイルは通ってしまう のです。

Python も、Haskell も、Rust も、この段階 にとどまっています。

しかし、Lean 4、Rocq、Agda といった言語では、様相が異なります。

これらの言語では、本記事で扱う Eq のような性質について、宣言したとおりに実装が振る舞うことの証明を、インターフェースの条件として要求できます。この形で定義された条件については、証明を書かなければコンパイルが通りません。

この証明が求められるレベルが、次に挙げる「第３段階」にあたります。

第３段階 ── 証明として要求する

Lean 4、Rocq、Agda では、証明を要求する形で条件を定義した場合、宣言があるだけではコンパイルが通りません。

「本当に条件を満たしている」ことの証明 を、プログラマがコードとして書く必要 があります。

そして、上記の言語の処理系は、その証明を検査 します。

他方で、Python、JavaScript、Haskell、Rust では、本記事で扱っている Eq / Hash などの性質について、通常の型検査だけでは、その性質そのものの証明までは要求されません。

宣言が書かれてさえいれば、その宣言どおりに実装が振る舞っているかを確かめることなく、コンパイルが通ってしまう のです。これは、第２段階にとどまっている段階です。

第４段階 ── 等しさそのものの構造を扱う

「２つの値が等しい」という主張（論理命題） を、型として宣言できる言語があります。

Lean 4 、Rocq 、Agda 、Idris 2 など が、それに該当します。

これらの言語では、次の対応関係が成り立っています。

論理の側	型の側
命題	型
その命題の証明	その型を持つ値を、実際に構成すること

この対応を「カリー＝ハワード同型対応」と呼びます。

1934年にハスケル・カリーが原型を示し、1968年にウィリアム・ハワードが現在の形に定式化しました。

そして、この同型対応が、いま数学研究の最前線で使われています。

未解決だった数学の定理が成り立つかどうかを、Lean 4 のような定理証明支援系で機械的に確かめる試みが、国際的な数学者の共同体で進行しているのです。

このあたりは、筆者の以下の過去記事で詳しく取り上げたところです。

その理論的な支柱の一つが、このカリー＝ハワード同型対応です。

さて、ここで一つ疑問が生じてきます。

「２つの値が等しい」という主張が型になり、その証明を書ける言語がある（ Lean 4 、Rocq 、Agda 、Idris 2 など ）と、先ほど申し上げました。

では、『同じ主張』についての証明を、『２通り』書いたとしたら、それら『２つの証明』は、互いに等しいとみなされるべきでしょうか？

「互いに等しいとみなす」・「互いに等しいとみなさない」という、回答となる主張もまた、一つの主張です。

したがって、型として宣言できます。

そして、「等しいとみなす方法」に、 複数のアプローチが発見済みの場合 は、同じ議論が、「等しさ」の「等しさ」のそのまた「等しさ」と、具体的な等しさから、抽象的な等しさに向けて、地上から天空高く、「等しさ」の階段が、無限に続いていきます。

このあたりは、本記事執筆者による以下の記事で論じています。

この記事の到達点を、先に述べておきます。

第４段階の解像度に踏み込んでいる言語があります。

Cubical Agda、Arend、そして Rocq（HoTT ライブラリなどの拡張を経由する形）などです。 Lean 4 でも、条件を課した範囲でなら扱えます。

しかし、そのような言語であっても、無限に高次の等しさへと積み上がっていく等しさの階層のすべてを、型として宣言することは、筆者の知る限りできていません。

なぜ、全体は宣言できないのか。

その理由を、本記事は明らかにします。

この記事が扱う範囲

本記事の議論は、大きく次の流れで進みます。

本シリーズは、ここまで見てきた ４つの段階 を、７つの言語 を通して辿ります。

また、以下の問いにも向き合います。

「複数ある異なる『等しさ』のそれぞれを、型として宣言できるのか？」

この問いに対する答え を、 Haskell、Rust、Idris 2、Lean 4、Rocq、Agda、Arend の ７言語 を比較しながら練り上げていきます。
（この７つの言語を選択した理由については、後述します）

各言語が、どこまでを型で捉えているかを、各言語のコード例を眺めながら、確かめていきます。

その上で、どの言語にも越えられない限界が２つあること を示します。

その具体的な中身は、後述の「本記事が示す『２つの限界』とは何か」の節で提示します。

この記事を読むと、何が得られるのか

この記事をお読みいただくことで、次のことが判断できるようになります。

自分が書いた等値比較は、数学的に「等しさ」と呼べる条件を満たしているか？
満たしていないとき、型システムはそれを捉えられるか？
「型で保証する」という言葉は、どこまでを指しているのか？

この記事は、以下のような読者の皆様にとって、新しい気づきをお届けすることができるのではないか、と考えております。

① 定理証明支援系を触り始めた人

refl が通らない理由を、判定的等しさと命題的等しさの区別から説明した日本語の記事は、ほとんどありません。第2部だけで独立した価値があります。

② 型クラスやトレイトを設計する人

「約束の表明」と「証明の提出」の区別は、等値性に限らず効きます。Rust の Eq／PartialEq がなぜ分かれているかを、数学的な理由から説明した記事も稀です。

③ 処理系を選ぼうとしている人

7言語を同じ軸で並べた表は、他に見当たりません。

Rocq が公理を型クラスにしているという事実は、調べても簡単には出てきません。

実務者向けの設計チェックリスト

本編に入る前に、この記事の内容を実務の設計判断に落としたチェックリストを掲げておきます。理論編を読み終えたあとに、もう一度見返していただくことを想定しています。

大文字・小文字を無視する ID や名前は、境界で casefold() などにより正規化し、正規化済みの値を格納する
金額など厳密な十進小数を扱う場面では、二進浮動小数点数をキーにせず、整数の最小通貨単位または Decimal を採用する
近似比較は、== やハッシュキーの同一視に流用せず、許容誤差を明示した専用関数として設計する
__eq__ を定義する型は、可変性・__hash__・コンテナ利用の要件をセットで設計する
Rust の Eq は「数学的性質が処理系により証明済み」という意味ではなく、型レベルの契約である
Lean などの定理証明支援系では、必要な性質を「命題」として明示し、その証明そのものを検査の対象にできる

この記事で扱うこと ── 問いの設定と本記事の地図

x == x が偽になることがあります。

たとえば、NaN です。

浮動小数点数の演算で、$0.0 \div 0.0$ のような計算を行うと現れる値です。

（補足：これは IEEE 754 の演算としての説明です。IEEE 754 の仕様では $0.0 \div 0.0$ のような不定形の演算は NaN を生じますが、言語のランタイムがこうした演算を例外として扱う場合があります。実際、Python の通常の float 演算では 0.0 / 0.0 は ZeroDivisionError を送出します。Python で NaN の値を得るには、この後のコード例のように float("nan") や math.nan を使います。）

Python でも Rust でも Haskell でも、自分自身と比べて偽になります。

x = float('nan')
print(x == x)          # False

同じことが、SQL でも起きます。

SELECT NULL = NULL     -- 結果は NULL（真でも偽でもない）

そのため IS NULL という専用の構文が用意されています。（なお、NaN と NULL は似て見えますが、別の問題です。IEEE 754 の NaN は浮動小数点仕様における特殊な値であり、SQL の NULL は「未知・欠損」を表すための三値論理の概念です。どちらも x == x が通常の意味で真にならないように見える点は共通ですが、その理由と背後の論理体系は異なります。）

「自分は自分と等しい」という当たり前に見える条件が、実務で使う値について成り立たないのです。

この記事は、そこから始めて、次の問いへ進みます。

「等しさ」を、型クラスとして扱うことは可能か？

型クラスという仕組みによって、「等しさ」をどこまで取り扱うことができて、どこから先が扱えないのか？

なぜ、この問いを立てるのか

コードを書くとき、私たちは絶えず「等しいかどうか」を判定しています。

条件分岐
テストの期待値照合
辞書の検索
重複の除去
キャッシュの一致判定
── どれも等値比較の上に成り立っています。

そして、等しいと判定されるべき２つの値が等しくないと判定されたとき、その原因を突き止めることは容易ではありません。

型が一致しない誤りであれば、コンパイラが指摘してくれます。

しかし、「等しさの定義が、プログラマの想定と異なっていた」という誤りは、 プログラムを実行するまで表面化しません。

こうした誤りを、コンパイラは型検査によって見つけることができないからです。

こうした誤りを、なぜコンパイラは型検査で検出することができないのでしょうか？

型検査が調べているのは、 「その型の値を、その型を受け取る場所に渡しているか」 です。

浮動小数点数を、浮動小数点数を受け取る場所に渡している
── ここまでは合っています。

しかし、「渡した値が想定どおりの値か」までは、型検査の範囲外です。

したがって、コンパイルは通ってしまいます。

具体例を３つ挙げます。

① 辞書のキーに、浮動小数点数を使う

冒頭で触れた例です。実際のコードで見てみます。

d = {}
d[0.1 + 0.2] = "値"
print(d[0.3])          # KeyError

何をしているコードか、順に述べます。

d = {} で、空の辞書を用意します。
辞書は「キーと値の組」を保存する入れ物です。

d[0.1 + 0.2] = "値" で、$0.1 + 0.2$ をキーとして "値" を保存します。

そして d[0.3] で、$0.3$ というキーを使って取り出そうとしています。

このコードを書いたプログラマの頭の中は、きっと以下のような意図があったはずです。

$0.1 + 0.2$ は $0.3$ である。
だから、同じキーで値を取り出すことができる。

しかし、このコードを実行してみると、 KeyError が出ます。
そのキーは存在しない、という意味です。

なぜ $0.1 + 0.2$ が $0.3$ にならないのでしょうか？

コンピュータは、小数を二進法で表します。
そして $0.1$ や $0.2$ は、二進法では循環小数になります。

十進法で $1 \div 3$ が $0.3333\ldots$ と続いて終わらないのと同じことです。 桁数に限りがあるので、どこかで打ち切ることになります。

打ち切った時点で、わずかな誤差が生じます。

print(f"{0.1:.20f}")   # 0.10000000000000000555
print(f"{0.2:.20f}")   # 0.20000000000000001110
print(f"{0.3:.20f}")   # 0.29999999999999998890

$0.1$ と $0.2$ は本来の値より少し大きく、$0.3$ は少し小さく保持されています。

そのため足し合わせた結果は、$0.3$ として保持されている値と一致しないのです。

print(0.1 + 0.2)       # 0.30000000000000004

「同じ数だから同じキーだろう」という想定が、実際の等値比較と食い違っているわけです。

② 大文字と小文字を区別せずに比較したかった

users = {"Alice", "bob"}
print("alice" in users)    # False

波括弧で囲む記法は、Python の set を作ります。

setは、重複を許さない入れ物で、同じものを２回入れても１つしか残りません。

print({1, 2, 2, 3})        # {1, 2, 3}

in は、 その入れ物の中に指定したものがあるかを調べます。

いまのコードの例では、利用者名を集めた入れ物に "alice" があるかを問うています。

このコードを書いたプログラマの意図は、きっと以下であったことが想像されます。

"Alice" は登録されている。
だから "alice" でも見つかるはずだ。

しかし、実際には、False が返ってきてしまいます。

文字列の一致判定は、文字列の完全一致で行われるからです。

「利用者名は大文字小文字を区別しない」という想定は、コードのどこにも書かれていませんでした。

③ 独自クラスで __eq__ を書き換えた

class Point:
    def __init__(self, x, y):
        self.x, self.y = x, y
    def __eq__(self, other):
        return self.x == other.x and self.y == other.y

print(Point(1, 2) == Point(1, 2))    # True

s = {Point(1, 2)}                    # TypeError: unhashable type

上記のコードについて解説します。

Point という独自のクラスを作り、__eq__ を書き換えています。

x と y が一致すれば等しいと判定する、という定義です。

そして２行目で比較し、３行目で set に入れようとしています。

このコードを書いたプログラマが思い描いていたことは、以下のようなことです。

__eq__ を書いたので、等しさの扱いは思いどおりになる。

比較そのものは、想定どおり True を返します。

しかし実際には、最後の行でプログラムが停止 してしまいます。

なぜ失敗するのでしょうか？

set は、格納するときに ハッシュ値 という数を計算します。
値ごとに数を割り当てて、その数を手がかりに高速に探すためです。

そして「等しい２つの値は、同じハッシュ値を持つ」という前提の上で動いています。

Point(1, 2) と Point(1, 2) は等しいと __eq__ で定義しました。
しかし、ハッシュ値の計算方法は変えていません。

もし既定のハッシュ計算（オブジェクトの同一性に基づくもの）がそのまま残っていれば、別々に作られた２つの Point に別の数が割り当てられます。 等しいのにハッシュ値が違う ── 前提が崩れます。

そこで Python は、この事故を避けるため、__eq__ を定義して __hash__ を定義していないクラスについては、__hash__ を None にして、ハッシュ値の計算そのものを無効にします。

矛盾した状態で動かすより、停止させるという判断です。

__hash__ を自分で書けば動きます。

ただし、__eq__ と食い違わないように書く責任は、プログラマが負います。

（Python の実際の挙動を、順を追って正確に整理しておきます。①通常のクラスで __eq__ を定義し、__hash__ を定義しないと、Python はそのクラスの __hash__ を None にします。②その結果、インスタンスは set の要素や dict のキーには使えなくなります。③値に基づく __hash__ を自分で追加する場合は、a == b ならば hash(a) == hash(b) という整合性を守る必要があります。④さらに、ハッシュ計算に使うフィールドは、コンテナへの格納後に変更されない（不変である）ことが求められます。本記事の主題である「宣言と、その整合性の検査」は、まさにこの③と④をどう保証するかという問題です。）

（なお、本文のコード例の __eq__ は、説明を簡潔にするため、other が Point でない場合を考慮していません。実務のコードでは、isinstance で型を確かめ、該当しない場合は NotImplemented を返す書き方が推奨されます。また、不変（immutable）なクラスとして設計し、__eq__ と整合する __hash__ を実装した場合にだけハッシュ可能にする、というのが安全な設計です。）

以上、見てきた３つの事例に共通するのは、いずれのコードも、コードを書いた時点では誤りを含むものとして検出されないことです。

①と②は、プログラムは動作するものの、間違った答えが返されてしまいます。

③は実行時に停止しますが、 それでも、動かしてみて初めて、停止するコードであったことが分かります。

先ほど、こうした誤りは型検査では見つけられないと述べました。

しかし、本記事で取り上げる７つの言語のうち、いくつかの言語は、こうした誤りを型検査で見つけられる仕組みを持っています。

それでは、どの言語が、型検査によって処理系のレベルで、コードに潜む誤りをどこまで見つけだすことができるのでしょうか？

この記事は、各言語の型の仕組みを掘り下げて論じることで、上記の問いに向き合います。

それによって、型で見つけられる誤りと、見つけられない誤りの線引きを、７つの言語を比べることで明らかにします。

①はすでに型で防げる

先に挙げた３つの例のうち、①には言語による対処法があります。

Rust では、浮動小数点数を辞書のキーに使おうとすると、 コンパイルの段階で拒否されます。

let mut map: HashMap<f64, String> = HashMap::new();
// コンパイルエラー: f64 は Eq を実装していない

なぜ拒否できるのでしょうか？

Rust は、「等しさが完全に成り立つ型」と「一部しか成り立たない型」を、型のレベルで区別しているからです。

浮動小数点数は後者です。

NaN があるせいで、「自分は自分と等しい」が成り立たないからです。

そして辞書のキーには、前者しか使えないと定められています。
その結果、事例①で挙げたような誤りを含むコードは、コンパイルの時点で、誤りが検出されて、プログラマはコードを修正することの必要性に気付くことができるのです。

この区別を支えているのが、型クラスと呼ばれる仕組みです。

型クラスとは何か

型クラス とは、「この型は、こういう操作ができる」「こういう性質を満たす」という約束を、型ごとにまとめて宣言する仕組みです。

Python でいえば、抽象基底クラスに近い役割を持ちます。

from abc import ABC, abstractmethod

class Comparable(ABC):
    @abstractmethod
    def __eq__(self, other) -> bool:
        ...

Comparable を継承したクラスは、__eq__ を実装しなければなりません。 「等値比較ができる」という約束を、クラスの側で宣言しているわけです。

Haskell では、同じことを次のように書きます。

class Eq a where
  (==) :: a -> a -> Bool

class Eq a where の a が、型を表す変数です。「型 a が Eq に属するとは、== という関数を持つことである」という宣言です。

(==) :: a -> a -> Bool の :: は「という型を持つ」を表します。 a を２つ受け取って、真偽値を返す関数 という意味です。

Rust では、こう書きます。

pub trait PartialEq {
    fn eq(&self, other: &Self) -> bool;
}

trait が、Haskell の class にあたります。fn eq(...) -> bool が、実装すべき関数の宣言です。

なお、実際の PartialEq には型引数が付いています。 正確な定義は第１部で扱います。

３つとも、やっていることは同じです。 「この型を使うなら、この関数を書くこと」と条件を掲げています。

ただし、Python との違いが１つあります。

Python の抽象基底クラスは、継承したクラスが __eq__ を実装しているかどうかを、 実行時に確認します。

Haskell と Rust は、 コンパイルの段階で確認します。
書き忘れれば、プログラムは動きません。

②と③はどうなるのか？

①は、Rust が型で防ぎました。

残る２つについても述べます。

②大文字と小文字を区別せずに比較したかった

これは、等値比較そのものを取り替えたい場合です。

String に定義されている等しさは、完全一致 です。

そこに「大文字小文字を無視する」という別の等しさを持ち込みたい ── １つの型に、２通りの等しさを与えたいわけです。

Haskell や Rust では、標準の等値比較として、１つの型に２通りの等しさを与えることができません。 等値比較の実装は、型ごとに１つだけと定められています。

ただし、newtype によるラップ、比較関数の明示的受け渡し、Rust の異なる Rhs を伴う PartialEq など。標準的ではない方法が存在します。

しかし Lean には、Setoid という仕組みがあります。

型に組み込まれた等しさとは別に、独自の等しさを持ち込めます。
本連載シリーズの第３部で扱います。

③__eq__ と __hash__ の食い違い

Python では、__eq__ を書き換えても __hash__ の整合はプログラマの責任でした。

Rust では、Eq と Hash の両方を実装するよう型で要求できます。 ただし、両者が整合しているかどうかは検査されません。

Lean であれば、整合性を証明として要求できます。 宣言だけでは済まず、実際に証明を書かなければインスタンスを作れません。

ここで、定理証明支援系という語を説明します。

Lean 、Agda 、Rocq など がそれです。

プログラムを書くだけでなく、「この主張は正しい」ということをコードとして書ける言語です。

そのコードを、証明と呼びます。

書いた証明が正しいかどうかは、処理系の中核にある型検査・証明検査の仕組みが確かめます。
誤っていれば通りません。

この違いが、本記事の中心的な論点です。

「約束を宣言させる」ところまでは、Rust や Haskell でもできます。
「約束が守られていることを検査する」ところから先が、定理証明支援系の領域になります。

どの部で、何を扱うか

各部で何を見ていくのか、順に述べます。

第１部 ── Rust

浮動小数点数は、辞書のキーとして使えません。Rust がそれを型で拒む仕組みを、コードを読みながら確かめます。

第２部 ── Agda

$2 + 3$ と $5$ は、処理系が計算して等しいと分かります。しかし「どんな $n$ でも $n + 0$ は $n$ に等しい」は、計算では確かめられません。

この違いが、記事全体を貫く区別になります。 そして前者は、型クラスの条件にできません。

第３部 ── ７言語の比較

Haskell、Rust、Idris 2、Lean 4、Rocq、Agda、Arend を並べます。

Lean には、Rust にないものがあります。

Rust では「この型の等しさは、数学の条件を満たす」と宣言するだけで済みました。

Lean は、その宣言に加えて証明を要求します。

証明を書かなければ、コンパイルが通りません。
嘘の宣言ができないわけです。

（厳密に述べると、Lean の論理核（カーネル）が主張を受理するには、その主張を導く証明項が必要である、ということです。もっとも、axiom として公理を追加する、外部の定理を信頼して用いるなど、何を信頼の基盤に置くかは別途明示すべき問題として残ります。本記事で「嘘の宣言ができない」と述べるときは、こうした公理の追加を行わない、通常の使い方を想定しています。）

Rocq はさらに進んで、等しさに関する公理そのものを型クラスにしています。

実際の Rocq のコードで、このことを確かめておきます。

Rocq の標準ライブラリ（Coq.Classes.RelationClasses）には、次のような 型クラス が定義されています。

(* 標準ライブラリの定義（属性などの表記を一部簡略化） *)

Class Reflexive (R : relation A) :=
  reflexivity : forall x : A, R x x.

Class Symmetric (R : relation A) :=
  symmetry : forall {x y}, R x y -> R y x.

Class Transitive (R : relation A) :=
  transitivity : forall {x y z}, R x y -> R y z -> R x z.

Class Equivalence (R : relation A) : Prop := {
  Equivalence_Reflexive  :: Reflexive R ;
  Equivalence_Symmetric  :: Symmetric R ;
  Equivalence_Transitive :: Transitive R }.

注目すべきは、この型クラスが実装者に要求しているものです。

Haskell の class Eq a where (==) :: a -> a -> Bool が実装者に要求していたのは、== という 関数（実装すべきコード） でした。

反射性・対称性・推移性という等しさの３条件 は、コードの 外側にある「守ってほしい約束」にとどまり ます。

これに対して、Rocq の Reflexive が要求しているのは、forall x : A, R x x
──「どんな x も自分自身と関係する」という 命題の証明そのもの です。

反射性・対称性・推移性という「等しさの公理」が、型クラスのフィールド（実装すべきメンバー）として書かれているのです。

したがって、この型クラスのインスタンスを作るとは、公理が成り立つことの証明を提出すること にほかなりません。

実際にインスタンスを作ってみます。

「偶奇が一致すれば等しいとみなす」という独自の関係を定義し、それが同値関係であることを証明します。

(* same_parity.v *)
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Arith.PeanoNat.

(* 「偶奇が一致する」という独自の等しさ *)
Definition same_parity (m n : nat) : Prop :=
  Nat.even m = Nat.even n.

(* Equivalence のインスタンス ＝ ３つの公理の証明の提出 *)
Instance same_parity_equiv : Equivalence same_parity.
Proof.
  split.
  - intros x. reflexivity.
  - intros x y H. symmetry. exact H.
  - intros x y z H1 H2. unfold same_parity in *. rewrite H1. exact H2.
Qed.

split によって、証明すべき目標が反射性・対称性・推移性の３つに分かれます。
- で始まる３行が、それぞれの公理の証明です。

検査させてみます。

（検証環境：Coq 8.18.0。RocqはCoqが改名された処理系であり、本記事では新名称のRocqに表記を統一しています）

$ coqc same_parity.v

何も出力されません。３つの公理の証明が、すべて受理されたということです。

では、公理の証明を１つ欠いたまま提出すると、どうなるでしょうか。
推移性の証明（- で始まる３行目）を削って、検査させてみます。

$ coqc same_parity.v
File "./same_parity.v", line 12, characters 0-4:
Error:  (in proof same_parity_equiv): Attempt to save an incomplete proof

「不完全な証明を保存しようとした」と拒否されました。

公理の証明が１つでも欠ければ、インスタンスは受理されない のです。

Haskell の型クラスが「実装すべき関数」を掲げるのに対して、Rocq の型クラスは「成り立つべき公理」そのものを掲げることができます。

型クラス とは単に Eq のような API を定義するだけの仕組みではない、ということを、Rocq は標準ライブラリのレベルで示しているのです。

第４部・第５部 ── 限界

型で扱えるものにも、限界があります。

等しさの証明どうしの関係を問うと、階層が無限に続きます。

その階層の全体を型で表す一般的な方法は、筆者の知る限り、まだ確立されていません。

そこで、別の道を選んだ体系があります。

立方体型理論 （ cubical type theory ）です。

この体系では、等しさを「２点を結ぶ線」として 言語そのものに組み込み ました。
プログラマが階層を定義する必要はありません。

線を引く 仕組みが最初から用意されている ので、その上の階層も自動的に付いてきます。

ただし、これは問題を解いたことにはなりません。

「階層の全体を型クラスとして宣言できるか」という問いは、依然として未解決 です。

立方体型理論は、この問いに答えていません。

型クラスとして宣言しようとするのをやめ、 等しさを言語の基本部品にしてしまったからです。

部品として最初から備わっているものについて、「宣言できるか」を問う必要がありません。

何を言語の基本部品に選ぶか。

そこを変えることで、問いそのものを回避 しました。

第５部で詳しく述べます。

第６部 ── 発想の転換

等しさそのものを型クラスにするのではなく、別のものを型クラスにする研究があります。

$a = b$ が分かっているとき、$a$ について成り立つことを $b$ についても成り立つものとして扱う
── この操作を型クラスにします。

たとえば、２つのデータ構造が同じものを表していると分かっているとき、一方について証明した定理を、他方へと移すことができます。

その移し替えを自動化する枠組みです。

では、この「移し替えの枠組み」を実際に備えている言語やシステムには、どのようなものがあるのでしょうか。

代表的なものを挙げます。

言語・システム	位置づけ
Rocq	この分野の研究の中心地。標準機能の一般化書き換え（`Proper` 型クラス）のほか、証明向きのデータ構造で証明した定理を計算向きのデータ構造へ移送する CoqEAL、一価性の考え方とパラメトリシティを組み合わせ、型クラスのインスタンス解決によって移送を自動化する Univalent Parametricity（2018〜）・Trocq（2024）などの研究があります
Lean 4（Mathlib）	同値 `Equiv`（`≃`）を軸に、`α ≃ β` と `β` 上の構造（`Monoid` など）から `α` 上の構造を作る移送（`TransferInstance`）を提供しています
Cubical Agda・Arend	一価性が言語に組み込まれているため、移送は型クラスではなく言語の基本部品です。同値 `e` から `ua e : A ≡ B` を作り、`subst` で定理を運びます
Isabelle/HOL	Transfer／Lifting パッケージ。型クラスによる仕組みではありませんが、この目的の最も古典的で、実用化された枠組みです

本記事でいう「この操作を型クラスにする研究」に最も直接対応するのは、Rocq の Univalent Parametricity と Trocq の系統です。

移送の型クラスをコードで確かめる

「移す操作」を型クラスとして宣言すると、どのようなコードになるのでしょうか。

先の図で示した「同じものを表す２つのデータ構造」に対応する、検証可能な最小の実例として、同じ自然数の２つの表現 を使います。

単進の nat ── O と S が鎖のように連なる表現
二進の N ── 二進の桁で構成される表現

研究の枠組み（CoqEAL・Univalent Parametricity）を単純化した 「移送の型クラス」を宣言 し、nat 側で証明済みの定理を、N 側へ移送してみます。

(* transport_demo.v *)
Require Import NArith Arith.

(* ============================================================
   「移す操作」を型クラスとして宣言する（研究の枠組みの最小版）
   ============================================================ *)

(* ２つの型のあいだに「行き来できる対応」があることの宣言 *)
Class Transport (A B : Type) := {
  to      : A -> B;
  from    : B -> A;
  to_from : forall b, to (from b) = b;
  from_to : forall a, from (to a) = a
}.

(* この型クラスから導かれる「移送」の操作：
   「to で移した値について成り立つ」ことが分かっていれば、
   B 側のすべての値について成り立つ *)
Lemma transport2 {A B} `{Transport A B} (P : B -> B -> Prop) :
  (forall x y : A, P (to x) (to y)) -> forall u v : B, P u v.
Proof.
  intros HP u v.
  rewrite <- (to_from u), <- (to_from v).
  apply HP.
Qed.

(* ============================================================
   ２つの表現：単進の nat（鎖）と、二進の N（桁の構造）
   ============================================================ *)

(* インスタンス宣言 ＝ 対応と、往復で元に戻ることの証明の提出 *)
Instance nat_N_transport : Transport nat N := {
  to      := N.of_nat;
  from    := N.to_nat;
  to_from := N2Nat.id;   (* N.of_nat (N.to_nat b) = b *)
  from_to := Nat2N.id    (* N.to_nat (N.of_nat a) = a *)
}.

(* ============================================================
   nat 側で証明された定理を、N 側へ移送する
   ============================================================ *)

(* nat 側の定理（既存） *)
Check Nat.add_comm.  (* forall n m : nat, n + m = m + n *)

(* N 側の定理：中身は「移送」だけ *)
Theorem add_comm_N : forall u v : N, (u + v = v + u)%N.
Proof.
  apply (transport2 (A := nat)).
  intros x y.
  rewrite <- !Nat2N.inj_add.     (* to は加法を保つ *)
  now rewrite Nat.add_comm.      (* nat 側の定理を適用 *)
Qed.

検査させてみます。

（検証環境：Coq 8.18.0）

$ coqc transport_demo.v

何も出力されません。移送された定理 add_comm_N が、受理されたということです。

このコードで起きていることを、３つに分けて述べます。

① 「行き来できる対応」を、型クラスとして宣言している

Class Transport のフィールドには、to・from という関数だけでなく、「往復すると元に戻る」という公理の証明（to_from・from_to）が含まれています。

関数と公理の証明をひとつの型クラスに束ねる ── Rocq の Equivalence 型クラスで見たのと同じ思想です。

② インスタンス宣言は、対応関係と証明の提出である

Instance nat_N_transport は、nat と N のあいだの対応と、往復の証明を提出しています。
これが、先の図の「同じものを表すと分かっている（$a = b$）」に当たります。

③ 移送された定理の証明本体は、「移送の呼び出し」だけである

add_comm_N の証明は、加法の可換性を N の上で証明し直してはいません。nat 側の既存の定理 Nat.add_comm を、transport2 という移送の操作で N 側へ運んでいるだけです。

一価性を持つ言語では、型クラスすら要らない

一方、一価性を言語に組み込んだ Cubical Agda では、同じことを型クラスなしで書けます。

A≡B : A ≡ B
A≡B = ua e                -- 同値 e から「型の等しさ」を作る（一価性）

thmB : P B
thmB = subst P A≡B thmA   -- A で証明した定理を B へ運ぶ

移送は、型クラス として宣言するものではなく、言語の基本部品として最初から備わっている のです。

先に「第４部・第５部 ── 限界」の紹介で述べた 「何を言語の基本部品に選ぶか」という問い の構図が、ここにもそのまま現れています。

（注記：上記の Transport クラスは、説明のために筆者が単純化した最小版です。CoqEAL や Trocq などの実際の研究用ライブラリは、より精密な対応関係の宣言と、強力な自動化を備えています。また、Cubical Agda のコードは概念を示すためのスケッチであり、Rocq のコードのような処理系での実行検証は行っていません。）

第７部 ── 各言語の強みと弱みの比較考察

言語の選び方と、最初につまずく箇所を挙げます。

本記事が示す「２つの限界」とは何か

等しさの多くは、型として宣言できます。

しかし、 ２つだけ宣言できないものが残ります。

第１の限界 ── 計算だけで確かめられる等しさ

$1 + 1$ と $2$ は、計算すれば同じ形になります。

この種の等しさを、型クラスとして宣言することはできません。

理由を述べます。

型クラスは、「この型を使うなら、この関数を書くこと」という条件を掲げる仕組みでした。

class Eq a where
  (==) :: a -> a -> Bool

この宣言は、「Eq に属する型は == という関数を持つこと」を要求しています。 プログラマは、その関数を書いて応えます。

つまり型クラスが指定できるのは、プログラマが書くコードです。

では、$1 + 1$ と $2$ の等しさについて、プログラマは何を書くのでしょうか。

何も書きません。
処理系が計算して確認し、そこで終わります。

確認した事実は、コードのどこにも現れません。
書くものがないので、型クラスの条件にできないのです。

（誤解のないように補足します。これは「型システムの中で表現できない」という意味ではありません。計算だけで確かめられる等しさは、型検査の内部でむしろ常に使われています。ここで述べているのは、計算すれば分かる事実を「実装すべきメソッド」として型クラスに要求することには意味がない、というより限定的な主張です。）

では、それで困るのか。

$1 + 1$ と $2$ の比較であれば、困りません。コンパイラが計算してくれるからです。

問題は、変数が入ったときです。

たとえば「どんな自然数 $n$ についても、$n + 0$ は $n$ に等しい」という主張を考えます。

$n$ にどんな数が入るかは決まっていません。
したがって、処理系には計算のしようがありません。

そこで、プログラマがこの主張の証明をコードとして書きます。

Lean であれば、次のような形になります。

theorem add_zero (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ m ih => simp [ih]

theorem add_zero (n : Nat) : n + 0 = n が、証明したい主張です。「自然数 n を受け取って、n + 0 = n が成り立つ」と読みます。

:= の後が、証明の中身です。

n がゼロの場合と、そうでない場合に分けて示しています。

この add_zero という名前は、他の場所から呼び出すことができます。
関数と同じように扱えるのです。

コードとして存在するので、こちらは型クラスの条件に掲げられます。

つまり、同じ「等しい」でありながら、扱いが分かれるわけです。

第２の限界 ── 等しさが持つ、無限の階層

いま見たとおり、変数を含む主張については、プログラマが証明をコードとして書きます。

そして、同じ主張について、書き方が２通りある場合があります。

たとえば同じ結果を返す関数を、繰り返しで書く方法と再帰で書く方法があるのと似ています。 証明の書き方も、１通りとは限りません。

では、その２通りの証明は、等しいのか。

具体例で述べます。先ほどの add_zero を、別の書き方でも証明できたとします。名前を add_zero' とします。

theorem add_zero  (n : Nat) : n + 0 = n := ...
theorem add_zero' (n : Nat) : n + 0 = n := ...

この２つは、同じ主張を証明しています。では、証明そのものは同じものなのか。

これも１つの主張です。
したがって、また証明を書くことになります。

theorem same : add_zero = add_zero' := ...

そして、この same の書き方が２通りあれば、同じ問いがまた立ちます。

この階層は、上へ無限に続きます。

ここから先は、HoTT という最先端の数学が関わってくる分野です。

定理証明言語のなかには、等しさが無限に積み上がる現象を取り扱う HoTT 理論を取り扱うことができる言語が存在します。

ただし、この階層の全体を型クラスとして宣言することは、筆者が調べた範囲では、どの言語でも実現されていません。

どの高さの階層についても通用する形で満たすべき条件を書き下す一般的な方法が、筆者の知る限り、まだ知られていないからです。

（この結論の射程を明確にしておきます。ここで「できていない」と述べているのは、本稿でいう「型クラスとして一様に宣言する」
──すなわち、無限に続く高次の等しさの構造を、有限個のメソッドと条件からなる一つのインターフェースとして要求する
──という意味においてです。

筆者が確認できた主要な処理系・ライブラリの範囲では、そのような一般的スキームは見当たりませんでした。

個別の高さの階層を扱う手段や、等しさを言語の基本部品として組み込む立方体型理論のようなアプローチは、本文で述べるとおり存在します。）

この２つが、本記事で扱う限界です。

それぞれ第２部と第４部で詳しく述べます。

型理論では、等しさの種類がさらに増える

Rust が分けたのは、「等しさの条件を すべて満たす 型」と「一部しか満たさない 型」でした。

型理論まで進むと、等しさそのものが複数に分かれます。

計算するだけで確かめられる等しさ と、 証明を書かないと示せない等しさ です。

両者は性質がまったく異なります。

では、それらを型クラスとして扱えるのでしょうか。

Haskell、Rust、Idris 2、Lean 4、Rocq、Agda、Arend ── ７つの言語が、この問いに対して、互いに異なる答え を出しています。

なぜ、この７つの言語なのか。

等しさをどこまで型に載せるかという軸の上で、 それぞれ違う位置に立っているからです。

言語	選んだ理由
Haskell	型クラスという仕組みを最初に持ち込んだ言語
Rust	等しさの条件を満たすかどうかで、型を分けている
Idris 2	証明を書けるが、実用のプログラミングに軸足がある
Lean 4	数学の形式化で最も使われており、標準の等しさが特殊な位置にある
Rocq	等しさに関する公理そのものを、型クラスにしている
Agda	型クラスを使わず、構造を明示的に渡す流儀を取る
Arend	等しさを言語に組み込みつつ、型クラスも備えている

（参考）

Arend
https://arend-lang.github.io/
https://arend-lang.github.io/documentation/getting-started/arend-features
https://arend-lang.github.io/2022/04/15/Arend-1.8.0-released.html

Java や C++ を扱わないのは、等値比較の仕組みが等しさの条件を型で区別しないからです。 そのため、本記事の問いに対して、比較の材料が出てきません。

それでは、７つの言語がそれぞれどのような答えを出しているのか、先に一覧で示します。

問いは、次の３つに分けられます。

問い①：証明を書かないと示せない等しさを、型クラス（相当の仕組み）の条件に載せられるか？
問い②：載せられるとして、何を条件として要求しているか？
問い③：計算するだけで確かめられる等しさを、型として宣言できるか？

（なお、この仕組みは Idris 2 では「インターフェース」、Rust では「トレイト」と呼ばれますが、本記事では型クラス相当の仕組みとして統一的に扱います。）

まず、問い①と問い②です。

言語	問い①への答え	問い②：型クラス（相当の仕組み）が要求するもの
Haskell	載せられない。値の等しさの命題を型として直接書く標準的な仕組みがない（GHC 拡張や singletons ライブラリによる部分的なエンコードは存在します）	`Eq` は `==` という関数のみを要求する。等しさの３条件は、コードの外側の約束にとどまる
Rust	載せられない。ただし「条件を満たす」という宣言までは型に載る	`PartialEq` は関数を、`Eq` は宣言（マーカー）を要求する。宣言の真偽は検査されない
Idris 2	載せられる	`DecEq` は「２つの値が等しいか否かを、等しさの証明（または反証）付きで判定する手続き」を要求する
Lean 4	載せられる	真偽値の比較 `BEq` と、命題としての等しさを分けたうえで、`LawfulBEq` が「`==` の判定結果が、命題的等しさと一致することの証明」を要求する
Rocq	載せられる	`Equivalence` が、反射性・対称性・推移性という公理の証明そのものをフィールドとして要求する
Agda	載せられる（ただし型クラスを主役にしない）	型クラス機構に頼らず、`Setoid`（担い手の型・同値関係・公理の証明の束）をレコードとして明示的に受け渡す
Arend	載せる必要がない	等しさ（道）が言語の基本部品として組み込まれているため、等しさそのものを型クラスとして宣言する必要がない。型クラス機構は、それ以外の構造のために備わっている

表の読み方を、順に述べます。

Haskell と Rust は、「宣言まで」に留まる言語です。

Haskell の Eq が要求するのは == という関数だけです。

Rust はそこに一歩進んで、「等しさの条件をすべて満たす」という宣言（Eq）を型のレベルで区別しました。

しかし、どちらの言語でも、宣言が事実かどうかは検査されません。
先に述べた第２段階にとどまる、ということです。

Idris 2、Lean 4、Rocq は、「証明まで」踏み込む言語です。ただし、証明の載せ方がそれぞれ違います。

Idris 2 の DecEq は、等しさの判定手続きに 証明の提出 を組み込みます。
判定結果が「等しい」なら等しさの証明を、「等しくない」なら反証を、値として返させるのです。

Lean 4 は、真偽値を返す比較（BEq）と、命題としての等しさを別のものとして扱ったうえで、両者が一致することの証明 を LawfulBEq という型クラスで要求します。

「計算による判定」と「命題としての等しさ」のあいだの整合性そのものを、型クラスの条件にしている、と言えます。（なお、Lean 4 には Idris 2 の DecEq に相当する DecidableEq も別途あります。）

Rocq は、すでに見たとおり、等しさの公理そのもの を型クラスのフィールドにしています。

Agda は、同じことを型クラスの外でやる言語です。

Agda にも型クラスに相当する仕組み（インスタンス引数）はありますが、標準的な流儀では、担い手の型・同値関係・公理の証明を束ねた Setoid というレコードを、関数の引数として明示的に渡します。

要求している中身は Rocq の Equivalence と同じですが、「処理系に暗黙に探させる」のではなく「プログラマが手で渡す」ことを選んでいるのです。

Arend は、問いの前提を変えた言語です。

等しさが道（path）として言語に組み込まれているため、等しさそのものを型クラスとして宣言する必要がありません。

部品として最初から備わっているものについて、「宣言できるか」を問う必要がないからです。

次に、問い③です。ここで、答えの様相が一変します。

言語	問い③への答え	計算による等しさは、どこに現れるか
Haskell	できない	値の等しさを型として直接書く標準的な仕組みがないため、この問い自体が立たない
Rust	できない	同上
Idris 2	できない	両辺が計算で同じ形になるとき、`Refl` で命題的等しさの証明が書ける。「計算で分かる」こと自体は、型として区別されない
Lean 4	できない	同様に `rfl` が通る、という形でのみ姿を見せる。判定的等しさは型検査の内部で働く
Rocq	できない	同様に、変換規則（convertibility）として型検査の内部で働き、`eq_refl` が受理されるという形で姿を見せる
Agda	できない	同様に `refl` が通る、という形でのみ姿を見せる
Arend	できない	道としての等しさは組み込まれているが、判定的等しさそのものは同様に内部にとどまる

問い①への答えは、言語ごとに見事に分かれました。しかし、問い③への答えは、７言語すべてで「できない」に揃います。

計算するだけで確かめられる等しさは、どの言語でも型検査の内部で働いています。rfl や Refl が通るのは、まさにこの等しさが処理系の中で確認されているからです。

しかし、その等しさそのものを、型として宣言したり、型クラスの条件として掲げたりすることは、本記事で扱う７言語ではできません。 確認した事実がコードのどこにも現れず、プログラマに 書かせるものがない からです。

（なお、型理論の研究には、判定的な等しさを命題的な等しさとは別の型として内部化する「２レベル型理論（two-level type theory）」と呼ばれる体系が存在します。

ただし、これは本記事で扱う７言語のいずれにも標準機能としては実装されていない、研究段階の体系です。）

この「答えが揃ってしまう」という事実こそが、先に「第１の限界」として述べたことの正体です。

この記事の結論

等しさに関する多くのことは、型クラスとして宣言できます。

「この型の等値比較は、数学の等しさの条件を満たす」という約束。
「２つの値が等しいかどうか、必ず判定できる」という保証。
さらには「型と型が同じであるとはどういうことか」を定める公理まで
── いずれも型クラスにしている言語があります。

しかし、先に述べた２つの限界は残ります。

計算だけで確かめられる等しさ と、等しさが持つ無限の階層
── この２つは、筆者が調べた範囲では、どの言語でも型クラスにできていません。

そこで、扱えないものを無理に扱おうとするのではなく、 別のものを型クラスにするという方向が探られています。

等しさそのものではなく、 等しさによって性質や構造を移す操作 です。

a = b が分かっているとき、a について成り立つことを b についても成り立つものとして扱う ── この操作を型クラスにする研究 が進んでいます。

（次回記事に続く）