読者です 読者をやめる 読者になる 読者になる

型レベルリテラルと行列

Haskell

行列(matrix)同士の和・差・積は、 行列の形によって定義されたりされなかったりするため、科学技術計算において予期しない実行時エラーの原因になることがある。 これをコンパイル時に防ぐには、行列の形まで含めて静的に型付けすればよい。 たとえば行列の積を

matmul :: Matrix a b -> Matrix b c -> Matrix a c

のように定義すれば、 matmulは行列の形が原因では実行時エラーとならないことが コンパイル時の型チェックによって保証される。 Haskellではこのような仕組みが 型レベルリテラル によってサポートされており、DataKinds言語拡張を通して使用可能になる。

ところがこの仕組みも万能ではない。 問題は、多くの場合行列の形(aとかbとかcとか)はコンパイル時点で未知数ということだ。 例えば統計処理プログラムでは、入力データの総数が実行時に初めて分かったりする。 なぜこれが問題かというと、一般に未知の型レベルリテラルが整合するどうかをコンパイル時に判定する問題は 「定理の自動証明」と同等に困難(絶対に解けないケースが存在する)なのだ。

ではどうするか。 hmatrixライブラリによる行列演算の実装では、 形の分かる行列の型L m nと形の分からない行列の型Matrix ℝの二種類を用意し、 2つを区別している。 使う側としてはこれら区別された型どうしを行き来する必要があるのだが、 特に形の分からないものを分かるものにキャストする手段が要になる:

withMatrix :: forall z . Matrix ℝ -> (forall m n . (KnownNat m, KnownNat n) => L m n -> z) -> z

当然「形の分からない行列のクラス」より「形の分かる行列のクラス」のほうが小さいため、 この関数は安全ではない。 つまり、実行時エラーを防ぐことができない。 ではこの「区別」にどのようなご利益があるかというと、 少なくとも「形の分かる部分」での不整合をコンパイル時に検知できるため、 アルゴリズムの主要部を安全に構築することが出来るということだ。 逆に言えば、実行時エラーを形の分からない部分のみに限定することが出来る。 しかも、冒頭の例で上げたように 多相な型レベルリテラル(aとかbとかcとか)を利用することで Haskell型推論の力を借りて整合性をチェックすることが出来るので、 チェック可能な範囲はそこそこ広い。

参考