実世界を扱う依存型プログラミングのたぶん基本～外界から安全な世界までの道
依存型ならさらに安全にプログラミングできちまうんだ！と言ったところで，「無料で遊べちまうんだ！」とか「3000円払えば無料で10連まわせる」みたいな感があり，
- 依存型使わない場合とどう違ってくるのか
- 入出力から扱い始めるとどういった形のプログラムになるのか
- 大概どういう流れでプログラミングすることになるのか
とか，そういった話を通しではそんなに見ないかなーという気がしたので，ごく基本的なものを一通りまとめておこうと思って．
まず，説明に使う問題設定について．行列演算，特に行列積を考えてみる．ただし，行列の形(行はいくつ，列はいくつ)についてはプログラムの外から入力によって決定するような状況とする．これ自体は普通の問題設定だと思われる．
依存型を使わなければ特にどうということも無い．恐らく行列の型を次のように定義し，
-- 形のみ持っておき，中身の数値については簡単のため省略 data Matrix = Matrix { row :: Integer , col :: Integer }
外部からの行列データ読み出しについては，恐らく悩むことはない．
-- 省略 readMatrix :: IO Matrix
行列積については，定義できる行列同士かどうかを検査して，成功する場合にのみ積を定義するだろう．
-- きっとこんな感じ prod :: Matrix -> Matrix -> Maybe Matrix prod m1 m2 | col m1 == row m2 = Just ... | otherwise = Nothing
あるいは，もう行列積が定義できることは前提にしてしまて，ダメならお行儀よくないがエラーにしてしまうかもしれないし，そもそも検査もしないでエイヤかもしれない．
-- きっとこんな感じ prod :: Matrix -> Matrix -> Matrix prod m1 m2 | col m1 == row m2 = ... | otherwise = error "Invalid"
と，この依存型を使わない行列積の定義は，とにかく何らかの形で失敗することを考慮する必要がある．2つの行列の形が行列積を定義するのに不都合な場合だ．そのため，本来値としてしか持っていない行列の形まで型情報に載せることができた上で，型レベルで整合している場合にのみ積が定義できるようになれば，今度は失敗を考える必要が無くなって安全になる．使うにしてもMaybeモナドとかがあらゆる箇所に挟まってくることがなくて喜ばしい．このためには依存型が必要になる．
とりあえず今回の前準備としては次のGHC拡張やらモジュールを使うので書いておく．いかにもって感じ．ちなみにghcは8でよろしく．
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeInType #-} import Data.Kind import Data.Proxy import Data.Singletons -- stack install singletons import Data.Singletons.TypeLits import Data.Type.Equality import GHC.TypeLits
今回の目的に沿った行列の型についてだが，3×4行列だったらMatrix 3 4といったように型レベル自然数を使って定義しておきたい．そうすれば，Matrix 3 4はMatrix 2 3とは積を取れないけどMatrix 4 5とは積を取れる，といったことが型レベルで，つまり，型検査時に判別できるからだ．なので，行列の定義は次のようになる．
-- 行列の形(行と列)を型レベルに持っておく．行列の中身は省略 data Matrix (row :: Nat) (col :: Nat) = Matrix { row :: Sing row , col :: Sing col } instance Show (Matrix (row :: Nat) (col :: Nat)) where show m = show (fromSing $ row m) ++ " x " ++ show (fromSing $ col m)
形を保持するにsingletonsパッケージからsingleton typeを利用している．Data.ProxyからProxyでもいいかもしれないが，なんとなく便利なことが多いように思うのでこちらを使っている．たぶん型から取り出すこともできるだろうし持ってなくてもいいかもしれないが．
この行列定義を使った行列積の定義は次のようになり，型変数bが同じ型(型レベル自然数)の場合に積が定義される．
-- 行列積(形が整合していることを型レベルで検査) prod :: Matrix a b -> Matrix b c -> Matrix a c prod m1 m2 = Matrix (row m1) (col m2)
証明とかの話だったら大体このくらいの段階で終わりで，このまま進めばやったぜとなるところだが，現実からデータを拾ってくることを意識するような今回の問題設定ではまだもうちょっとだけというかだいぶ足りてない話題があるのでもっと先まで掘っていくことになる．
外部からのデータで行列の形が決まる場合，事前に形を決めておくことができないので，同じIOアクションで統一的に読み出すことができないという問題がある．「毎回2×3行列を読み出す」IOアクションは書けるが，「今回読み出した結果2×3行列だった，次回読み出した結果は3×4行列だった」みたいにデータによって結果がコロコロ変わるようなものは書けない．
-- 外部データとして行列の読み出し -- たとえば，以下のようなデータを読み出してはじめて形が決定される場合， -- 3 3 -- 1 0 0 -- 0 1 0 -- 0 0 1 -- 次のように形を決めておくことはできない --これは毎回2×3行列を読み出すIOアクションになってしまう readMatrix :: IO (Matrix 2 3)
そのため，型レベルに乗っている行列の形についての情報はIOで読み出す場合，隠蔽しなければならない．
--何らかの形の行列は入ってるが，型には情報が現れてこない readMatrix :: IO SomeMatrix
で，この隠蔽を行うのが存在型ということになる．難しいことはよくわからないのでとりあえずAgdaのData.Productからsigma typeを引っ張ってくる．
{- AgdaのData.Product.Σを可能な限りそれっぽく移植 record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where constructor _,_ field proj₁ : A proj₂ : B proj₁ -} data Sigma a (b :: a -> Data.Kind.*) where Sigma :: SingKind a => { proj1 :: Sing (x :: a) , proj2 :: b x } -> Sigma a b
このSigmaは要はタプルなのだが，Haskellの通常のタプルとは異なり，2要素目の型(種)が1要素目の型(種)の値(型)に依存している．とはいえ，Haskellの場合Agdaのようには値レベルと型レベルを奔放に行き来できないので，TypeInTypeとか危険な拡張を使いつつsingleton typeで値レベルと型レベルの一致を取りつつとなっている．型変数xが外に見えない形になるのでSigmaは存在型になる．Agdaでも∃をΣで定義しているので，同様にしてこれもHaskell側に持ってきておく．
{- AgdaのData.Product.∃ ∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b) ∃ = Σ _ -} type Exist t = Sigma k (t :: k -> Data.Kind.*)
Sigmaのproj1にはproj2の型の表す命題を満たす値，proj2には命題を満たす証明に対応する値が入っており，全体として，proj2の型の命題を満たす値が存在するという命題の型及びその証明になる．ちょっとこのSigma(Exist)の動きをもう少し見ておこう．ユーティリティ関数を2つ用意する．
-- Sigmaの1要素目を参照して何かする withProj1 :: Sigma a b -> (DemoteRep a -> r) -> r withProj1 (Sigma {proj1 = p}) f = f . fromSing $ p -- SIgmaの2要素目を参照して何かする，xは外に持ち出せない withProj2 :: Sigma a b -> (forall x . b (x :: a) -> r) -> r withProj2 (Sigma {proj2 = p}) f = f p
たとえば，Sigma(Exist)によって，「0と等しい自然数が存在する」という命題と，その証明を与える．
-- (型レベル)0と等しい(型レベルの)自然数値が，なにかしら存在するという命題の型 existsNatEqualsZero :: Exist ((:~:) 0) -- Sigma Nat ((:~:) 0) と同じ -- と，その証明 existsNatEqualsZero = Sigma SNat Refl -- existsNatEqualsZero = Sigma (SNat :: Sing 0) (Refl :: 0 :~: 0) -- 型注釈を付けると -- existsNatEqualsZero = Sigma (SNat :: Sing 1) (Refl :: 0 :~: 1) -- 間違った型の値だと型エラー
「0と等しい自然数」は0(singleton typeなのでSNat :: Sing 0)であり，「0が0と等しい証明」はReflである．この証明から実際に「0と等しい自然数」と，「それが本当に0と等しいことの証明」を取り出す．
-- 「(型レベル)0と等しい(型レベルの)値」を値レベルで取り出したもの value :: Integer value = withProj1 existsNatEqualsZero id -- 「(型レベル)0と等しい(型レベルの)値」であるvalueが0と等しい証明 proof :: 0 :~: 0 proof = withProj2 existsNatEqualsZero f where f :: 0 :~: x -> 0 :~: 0 f Refl = Refl
本題に戻る．Matrixが型レベルで持っている行列の形の情報を，存在型で隠した型SomeMatrixを定義する．
-- 形を隠す newtype SomeMatrix' row = SomeMatrix' (Exist (Matrix row)) newtype SomeMatrix = SomeMatrix (Exist SomeMatrix')
また，隠しっぱなしだと意味が無いので，SomeMatrixに隠されたMatrixの形を使える環境も用意する．行列の形についての型がからむ情報はこの環境中でしか使えず，外には持ち出せない．持ち出そうとすると型検査で弾かれる．
withSomeMatrix :: SomeMatrix -> (forall row col . Matrix row col -> r) -> r withSomeMatrix (SomeMatrix m) f = withProj2 m $ \(SomeMatrix' m') -> withProj2 m' f
ついでに，Showのインスタンスにもしておく
-- 隠したMatrixのshowを呼び出す instance Show SomeMatrix where show sm = withSomeMatrix sm show
SomeMatrixではデータに依存して決定される型の情報が見えなくなったので読み出しのIOアクションが定義できる．
-- 形だけ読めればいいので"2 3"と空白入れて1行で形を読むだけの定義 readMatrix :: IO SomeMatrix readMatrix = do line <- getLine let [a, b] = map read (words line) :: [DemoteRep Nat] withSomeSing a $ \sa -> withSomeSing b $ \sb -> return $ SomeMatrix (Sigma sa (SomeMatrix' (Sigma sb (Matrix sa sb))))
readMatrixでは"2 3"と入れれば存在型により内部にMatrix 2 3型の値を隠蔽したSomeMatrix型の値が読み出される．読み出し毎に毎回異なるMatrix a b型の値を作ってから隠蔽し，最終的には同一の型SomeMatrixを構成していることに注意．
で，やっとこさ行列積の話になるわけだけど，当然SomeMatrix同士の積は行列の形が内部に隠されてしまっているので，また失敗することがある．「なんだ元々失敗することあったって話だったわけだし，依存型使っても失敗するところが出るんじゃ手間が増えただけで堂々巡りじゃないか」とか思った人がいるんじゃないかなと思う．だけど，それは今回の話が行列積しかしないごく単純なサンプルだからで，本当はもっと大きな計算をリッチな型情報を盛りっぱなしにしたゴージャスな型が付いた状態で安全便利に構築して，外部から値が入ってくるインターフェースの部分にだけ存在型で失敗する部分があるという形になるというのが理想なわけだ．
というわけで気をとりなおしてSomeMatrix同士の積をprodで定義する．
toProxy :: Sing a -> Proxy a toProxy _ = Proxy maybeProd :: SomeMatrix -> SomeMatrix -> Maybe SomeMatrix maybeProd sm1 sm2 = withSomeMatrix sm1 $ \m1 -> withSomeMatrix sm2 $ \m2 -> case (m1, m2) of (Matrix r1 c1, Matrix r2 c2) -> case withKnownNat c1 $ withKnownNat r2 $ sameNat (toProxy c1) (toProxy r2) of Nothing -> Nothing Just Refl -> Just (SomeMatrix (Sigma r1 (SomeMatrix' (Sigma c2 (prod m1 m2)))))
withSomeMatrixで存在型に隠されたSomeMatrixから形付きのMatrixを使える環境に入り，Matrix同士の積を取ってまた存在型にしまいこむ．ミソはsameNatの値をcaseで見てるところで，GADT(今回のはPropositional Equality)のパターンマッチによりユニフィケーションされて積が取れる形であることがわかりprodが使えるようになる．逆に言うと，形付きの行列m1，m2はwithSomeMatrixですぐに見えるようになるが，Reflへのマッチが済んでからでないとm1とm2のprodは取れない．たとえば，NothingのケースをJustケースと同じ結果になるよう書き換えたとしても，型検査に失敗することが確認できるだろう．
これらを使って次のようなmainを記述し実行してみると，
main :: IO () main = do m1 <- readMatrix m2 <- readMatrix case maybeProd m1 m2 of Nothing -> error "Invalid" Just m3 -> print m3
次の2×3行列と3×4行列のような行列積が定義できる入力の場合にのみ積を取れることになり，他はエラーとなる．
*Main> main 2 3 3 4 2 x 4 *Main> main 1 2 1 2 *** Exception: Invalid
証明だけに限った話ではなく，実用，特に入出力(特に入力)込みで依存型をみてみると，その最も大きな影響はメインの処理に入る前段階でのデータ・データ間の性質の検証またはクリーンアップに対する型安全性の導入・強要という形で現れる．値レベルで値だけ見て性質を満たしていなければ目的の関数が実行時に失敗するしそれでも仕方がないという状況であったものが，依存型の導入によって，型レベルでも性質を満たしたことが型検査器にわかる経路でしか目的の関数を使うことができないというように変わる．現実はクソなので，入力されてくるデータがクサレてるのは仕方が無いことで，それを原因として実行時エラーが起きるのは当然のことであり，だからといって何も起きないようにしようとかいう話をしているわけでは決してない．目的の処理に入るより前の段階で，クサレてるデータをちゃんとクサレてると判断し実行時エラーを出す，まさにその判定部分にミスが入り込まないよう型で守ることができるようになる．型合わせゲーが最高めんどくさいけど．
おおまかにまとめると，流れとしては
- 依存型ガチガチで型付け
- 依存型を最大限利用して目的の処理を安全に書いておく
- 依存型を構成する要素のうち，外部データで決まる部分を存在型で隠した型を用意する
- 存在型の中に隠された依存型の値を参照できる関数を用意する，たぶんローンパターンがいい
- 外部からデータを読み，依存型の値を構成，さらに存在型で隠した値を構成する
- 型の上での必要な制約が満たされるようGADT値のパターンマッチでユニフィケーションを発生させる
- 制約に対して型が整合しない経路に対してはデータ形式のエラー，目的の処理は型が合わずうっかりですら使えない
- 制約に対して型が整合した経路では目的の処理を行える
という感じになる．
今回のソースはココ
