多段階計算によるコンパイル時テンソル形状検査

テンソル（多次元配列）を扱いプログラムを書くときは、形状の不整合が起きないことを静的に保証したい

不整合は実行時エラーとして現れ、数時間かかった計算が水の泡に

よくある回避策と課題

依存型と手動証明: e.g. Idris

篩型 + 自動証明: e.g. Hybrid type checking, GraTen

課題: 継続的なソフトウェア開発との親和性

プログラムを修正するたびに証明の置き換えや SMT ソルバの自動照明が動くようにするのは負担

新しい回避策

多段階計算: コンパイル時計算と実行時計算を型安全に分離

型チェック時に挿入されるコンパイル時の assert によって保証

定理証明は不要（証明は過剰？）

コードが生成されたら、実行しても不整合が起きないことが証明されている

多段階計算

Lisp 風マクロの型付け版

https://gyazo.com/e51af7e7a2eb82548c919cb8511684c3

Stage0 が通常の CBV で評価

Assertion がコンパイル時に評価する

assertion は Stage0 に

一方でテンソル計算は Stage1 で

形式化の詳細と改善

assertion は型検査器が自動挿入する

2 つの型が compatible だが構文的に一致しない場合

証明済み

改善ポイント

冗長な記述

暗黙の前提と限界

テンソルの形状はそれほど動的ではなく、入力が決まれば出力の形状が決まるような演算のみを用いて書けること前提

評価によって審議を判定できない性質の保証には使えない

したがって、ライブラリの検証には不向き

実行時に初めて形状が分かるようなテンソルも扱える

が、不整合が生じる可能性を排除することはできない

単に実行時にコード生成して、実行するだけ

しかし、assertion failure はコード生成時に生じるのであって、実際のテンソルを使った計算中に起きるわけではない