型レベルリテラルと行列

行列(matrix)同士の和・差・積は、 行列の形によっては定義されない。せっかくHaskellのように強い型システムをもつ言語を採用していても、実行時エラーの潜在的原因になってしまう。

これをコンパイル時に防ぐには、行列の形まで含めて静的に型付けする。 たとえば行列の積は

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

のように定義できる。 すると、行列の形が正しいかどうかがコンパイル時に自動でチェックされる。

コンパイル時にチェックすることで受けられる恩恵は2つある。 1つは実行時エラーの潜在的原因を減らすことでプログラムの信頼性が高まることだ。これは同時に実装者の心理的負担を減らすことでもある。 もう1つは、形のチェックを前もって行うので、(ノーリスクで!)ランタイムオーバーヘッドを低減できることだ。 GHCではこのような仕組みが 型レベルリテラル によってサポートされている1

Haskell数値計算デファクトスタンダードhmatrixでは、 形の分かる行列の型L m nと形の分からない行列の型Matrix Doubleの二種類を用意し、 2つを区別している。 使う側としてはこれら区別された型どうしを行き来する必要があるのだが、 特に形の分からないものを分かるものにキャストする手段が要になる。 例として、行列を2つ読み込んで「安全な」演算を行い、最小二乗解を出力するプログラムを示す:

main = do
  x <- loadMatrix "sample1.mat" -- x :: Matrix Double
  y <- loadMatrix "sample2.mat" -- y :: Matrix Double
  let beta = withMatrix x $ \x -> -- x :: L m n
             withMatrix y $ (. exactDims) $ \case
               Nothing -> error "y has incompatible dimensions"
               Just y  -> let -- y :: L m k
                 lse = (tr x <> x) <\> tr x <> y -- lse :: L n k
                 in unwrap lse
  putStrLn "least square-error solution is:"
  print beta

このようにすると、少なくとも形の分かる部分での不整合をコンパイル時に検知できるため、 プログラマアルゴリズムの主要ロジックを安全に構築することが出来る(例えば、tr x <> xx <> xと書くとコンパイルが通らない)。 また同時に、煩雑なエラーハンドリングを最初のキャスト時に限定することが出来る(今回で言えばNothing ->のところ)。

参考


  1. 一般に型レベルリテラルが整合するどうかをコンパイル時に完全自動で判定する問題は、入力の多項式時間(現実的な時間)では解けないと考えられている。したがって、複雑なプログラムの場合にはコンパイラのチェックを人手でサポートし、半自動でチェックする必要が出てくる。