型レベル自然数を使って型付き行列を作ってみた

#動機 研究で行列計算ライブラリを使っているのですが、numpyはなぜか異なる型の行列同士を足せてしまいます。 このせいでデバッグがめちゃくちゃ大変でした。

こんな単純な間違いはコンパイル時に弾いてくれればいいのにと思ったので、違った型の行列は足せないようなちょっとしたライブラリを作ってみました。

※行列を安全に計算したい人のためには

Numeric.LinearAlgebra.Static

↑のライブラリが既に存在しました。不勉強ですみません。この記事は「型レベル自然数ってこんなに簡単に(僕でも)使えるんだ」、程度に読んでください。

型レベル変数

最近のGHCでは、自然数をパラメーターとするデータ型を定義できる。固定長リストの長さを型に持たせるとか、行列の大きさを型に持たせるとか、そういうことができる

引用元:Haskell (GHC) の型レベル自然数とリフレクションを試してみる

行列の大きさの情報を型に持たせることができる。 →やってみました

仕様

  • 行列の足し算・掛け算をサポートする・
  • 足し算/掛け算できないものを計算しようとしたらコンパイル時にエラーにする

実装

{-# LANGUAGE DataKinds, KindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}

module SizeFixedMatrix where
import GHC.TypeLits
import Data.List.Split
import Data.List

data SizeFixedMatrix (h :: Nat) (w :: Nat) = MakeMartix [[Integer]] deriving (Eq,Show)

mat1 = MakeMartix [[1,2],[2,3]] :: (SizeFixedMatrix 2 2)
mat2 = MakeMartix [[2,9],[1,3],[4,3]] :: (SizeFixedMatrix 3 2)
mat3 = MakeMartix [[5,9],[3,3],[0,3]] :: (SizeFixedMatrix 3 2)


add :: SizeFixedMatrix p q -> SizeFixedMatrix p q -> SizeFixedMatrix p q
add (MakeMartix m1) (MakeMartix m2) = MakeMartix (map (\(a,b) -> map (\(c,d) -> c+d) (zip a b)) (zip m1 m2))

mul :: SizeFixedMatrix p q -> SizeFixedMatrix q r -> SizeFixedMatrix p r
mul (MakeMartix m1) (MakeMartix m2) = MakeMartix $ splitEvery (length (head m2)) [sum $ zipWith (*) v w | v <- m1, w <- transpose m2]

…これだけです。拍子抜けするくらい簡単に作れました。もう少し凝ったものを作りたかったのですが、締切に間に合いそうにありませんでした。

一応ちょこっとだけ解説しておくと

SizeFixedMatrix p q

が縦p行横q列の行列の型になります。

不適切な型同士でaddしたりmulしたりするとコンパイルエラーになるので安心してプログラミングできます。

結果

$stack ghci
(省略)
*Main FiniteField Lib SizeFixedMatrix> mat1
MakeMartix [[1,2],[2,3]]
*Main FiniteField Lib SizeFixedMatrix> mat2
MakeMartix [[2,9],[1,3],[4,3]]
*Main FiniteField Lib SizeFixedMatrix> mat3
MakeMartix [[5,9],[3,3],[0,3]]

足し算

*Main FiniteField Lib SizeFixedMatrix> add mat1 mat2

<interactive>:4:10: error:
    • Couldn't match type ‘3’ with ‘2’
      Expected type: SizeFixedMatrix 2 2
        Actual type: SizeFixedMatrix 3 2
    • In the second argument of ‘add’, namely ‘mat2’
      In the expression: add mat1 mat2
      In an equation for ‘it’: it = add mat1 mat2

mat1は2行2列の行列型、mat2は3行2列の行列型なので足せないと言われてしまいます

*Main FiniteField Lib SizeFixedMatrix> add mat2 mat3
MakeMartix [[7,18],[4,6],[4,6]]

掛け算

*Main FiniteField Lib SizeFixedMatrix> mul mat1 mat2

<interactive>:8:10: error:
    • Couldn't match type ‘3’ with ‘2’
      Expected type: SizeFixedMatrix 2 2
        Actual type: SizeFixedMatrix 3 2
    • In the second argument of ‘mul’, namely ‘mat2’
      In the expression: mul mat1 mat2
      In an equation for ‘it’: it = mul mat1 mat2
*Main FiniteField Lib SizeFixedMatrix>

mat1*mat2(行列積)は存在しません

*Main FiniteField Lib SizeFixedMatrix> mul mat2 mat1
MakeMartix [[20,31],[7,11],[10,17]]

感想

型レベル変数などという難しい名前の機能をはじめて使いました。案外簡単に使えたので、他にも応用できると思います。

参考文献