モナド則、証明しました 💪
普通のOCamlライブラリは「テストを書いて動作を確認する」のが普通ですが、certified_base はさらに証明を与えました。
-
Fn.composeの結合律 -
Result/Option/Listの Functor則・Monad則 -
Sign.(*)（符号の掛け算）の交換律・結合律
とかを Rocqの定理としてコンパイル時に証明しています。テストでは保証できない網羅的な検査がされています。
使い方 
利用者からすると使い方は簡単です。open Base の代わりに open Certified_base すれば動くんです。
open Certified_base
let numbers = [ 1; 2; 3; 4; 5 ]
let () =
let evens = List.filter (fun n -> n mod 2 = 0) numbers in
let doubled = List.map (fun n -> n * 2) numbers in
let total = List.fold numbers 0 ( + ) in
Printf.printf "偶数: %s\n" (String.concat ", " (List.map string_of_int evens));
Printf.printf "2倍: %s\n" (String.concat ", " (List.map string_of_int doubled));
Printf.printf "合計: %d\n" total
現在のラインナップ 🎛️
| モジュール | 証明 | 抽出 | 備考 |
|---|---|---|---|
Fn |
✅ | ✅ |
compose/flip/apply_n_times など。結合律など保証 |
Unit |
✅ | ✅ | 皆さんおなじみのunit型 |
Result |
✅ | ✅ | Functor則・Monad則など証明済み |
Option |
✅ | ✅ |
compare/value_map/map2/both/apply まで実装 |
List |
✅ | ✅ |
mapi/iteri/take/drop/zip/unzip/partition_tf などなど。rev_involutive も証明済み |
Sign |
✅ | ✅ | 符号の掛け算の交換律・結合律を証明 |
なにを証明したのか
例1: Sign の掛け算則
Sign.t は Neg | Zero | Pos の3値で、符号の掛け算 (*) を定義しています。
Lemma mult_comm : forall x y, x * y = y * x.
Proof. intros [] []; reflexivity. Qed.
Lemma mult_assoc : forall x y z, (x * y) * z = x * (y * z).
Proof. intros [] [] []; reflexivity. Qed.
3値しかないので intros [] [] で全パターンに分解すれば reflexivity だけで証明が終わります。証明そのものは単純ですが、「本当に全パターンで交換律が成り立つこと」を型検査器が保証してくれるのがポイントです。
例2: Result のMonad則
Lemma left_identity :
forall {A B E} (x : A) (f : A -> t B E), bind (return_ x) f = f x.
Proof. intros; reflexivity. Qed.
Lemma right_identity : forall {A E} (m : t A E), bind m return_ = m.
Proof. intros A E [x | e]; reflexivity. Qed.
Lemma assoc :
forall {A B C E} (m : t A E) (f : A -> t B E) (g : B -> t C E),
bind (bind m f) g = bind m (fun x => bind (f x) g).
Proof. intros A B C E [x | e] f g; reflexivity. Qed.
これはいわゆる「モナド則」そのものです。Option・List にも同様の3つの法則(左単位元・右単位元・結合律)を用意し、証明しています。base そのものにはこの手の法則を保証する仕組みはありません(ドキュメントに書かれているだけです)が、certified_base では型検査に通ればモナド則が保証されます。
実物の base と突き合わせテストもしている
元のbaseライブラリと振る舞いが違わないように、そこはテストでチェックしています。網羅的に検証したい法則は証明して、実行時の振る舞いはテストしている感じで使い分けています。
まとめ
certified_base は「Jane StreetのBaseをRocqで再実装し、Functor則・Monad則などをコンパイル時に証明した上で、実際にOCamlから open Certified_base で使えるようにする」プロジェクトです。証明支援系がテストの外側にある性質まで保証してくれるので、動くけど本当に法則を満たしているか自信がないという不安を解消するのが嬉しいです。イシュー・プルリク歓迎です♪