TL;DR
- テンソルの形状の不整合を、定理証明なしで静的に防ぐ手法の紹介。
- 多段階計算でコンパイル時と実行時の計算を分け、型検査器が自動で挿入する assertion をコンパイル時に評価する。生成されたコードは実行しても形状の不整合が起きない。
内容
背景
テンソル（多次元配列）を扱うプログラムでは、形状の不整合が起きないことを静的に保証したい。不整合は実行時エラーとして現れ、数時間かかった計算が無駄になる。
よくある回避策には、Idris のような依存型と手動の証明や、Hybrid type checking や GraTen のような篩型と自動証明がある。ただし、どちらも継続的なソフトウェア開発との相性に課題がある。プログラムを直すたびに証明を書き直したり、SMT ソルバによる自動証明が通るようにしたりするのは負担が大きい。
多段階計算による検査
新しい手法では、多段階計算でコンパイル時の計算と実行時の計算を型安全に分ける。多段階計算は Lisp 風のマクロの型付け版で、ステージ 0 は通常の値呼び（CBV）で評価される。形状の assertion はステージ 0 に、テンソルの計算はステージ 1 に置く。型検査のときに挿入されるコンパイル時の assertion で整合性を保証するので、定理証明は要らない。コードが生成されれば、実行しても不整合が起きないことが証明されている。
形式化と改善
assertion は、2 つの型が compatible だが構文として一致しない場合に、型検査器が自動で挿入する。この形式化は証明済みである。記述が冗長になる点は、表層言語 Horsea で改善している。
前提と限界
この手法は、テンソルの形状がそれほど動的でなく、入力が決まれば出力の形状が決まるような演算だけで書けることを前提にしている。List.filter のような演算は使えない。また、評価して真偽を判定できない性質の保証には使えないので、ライブラリの検証には向かない。プロパティベーステストのような使い方はできるかもしれない。
実行時に初めて形状が分かるテンソルも扱える。この場合は実行時にコードを生成して実行するだけなので、不整合が起きる可能性は排除できない。ただし、assertion の失敗はコード生成のときに起きるのであって、実際のテンソルを使った計算の途中で起きるわけではない。
キーワード
- 多段階計算
- 依存型
- 篩型
- プロパティベーステスト