コンテキストの順番を入れ換えると互換性が崩れることがある
(注:この記事はかなり前に書いて公開し忘れていたことに今日気付いたものです．もう当たり前になってるかもしれないけどもったいないので一応)
ghc8以降TypeApplications拡張が入ったこともあり一応の注意喚起．
たとえば，次のように関数fとgを定義する．時系列的にはfの型をgの型に変更したような想定で．
data X a b = X a b f :: (Show a, Show b) => X a b -> String f (X a b) = show a ++ show b -- fと比べて型変数aとbに対するShowコンテキストを入れ換えたもの g :: (Show b, Show a) => X a b -> String g = f
普通に使っている分にはfからgの変更に問題無い．
x :: X Int Char x = X 1 '0' fx :: String fx = f x gx :: String gx = g x
だけど，TypeApplications付けて使ってる箇所は型検査に失敗する．
{-# LANGUAGE TypeApplications #-} fx :: String fx = f @Int x gx :: String gx = g @Int x -- Error
といったように，コンテキストの順番変更も型の変化に相当する場合がある．また，コンテキストを減らすことができるケースであっても，それにより型変数の出現順が変わるとTypeApplicationsにより型検査に失敗するようになることがある．
互換性破壊してるのにhackageバージョニングポリシに従ったバージョン上げを行っていないライブラリをアップロードしてしまうことになるかもしれないので，ライブラリ作者はTypeApplications拡張の存在も気にして互換性の管理をするべきだと思われる．逆に，ライブラリ利用者としてはTypeApplications拡張使っているとこういう漏れてきた互換性破壊を踏んでしまうかもしれないという認識を持つべきなのかな．
問題を解決するつもりでキッチリ型を付けた先にある高い壁
null安全おじさんになりかわりそれがしがお見せつかまつる 機械が理解できる複雑な契約の型表現がもたらすものは つまるところこのようなもの ずぶぶ(切った腹から証明オブジェクトを引き摺り出す)
— Noriyuki OHKAWA (@notogawa) 2016年11月18日
過ぎたるは猶及ばざるがごとし．
最近null安全？だかの話のからみで，(静的な)型で契約云々を表現してシアワセになれるんだぜーと言うのをチラホラ見聞きする．たとえば，pythonで統計なり機械学習なりやっててnumpy弄るような人が，ndarray(多次元配列)のshape(多次元配列の形)が合わずエラーで落ちたりとかそういうアレについて云々という．なるほど型があれば実行前に止めることができ，実行時，エラー*1になってファーみたいなことは避けられるだろう．
しかし，これが天国へ続く道かどうかはまた別の話．(依存)型で舗装しているのは地獄への道かもしれないのだ．冒頭ツイートの通り陰腹召してでも諫めておかねば，その希望，容易に絶望に反転し得る．
では実際に見ていこう．内容としては，numpy ndarrayとその上での操作をいくつか取り上げ，配列要素だけでなくshapeまで型レベルで扱うことで，間違えたshapeを持つ操作を禁止できるようにしてみるというもの．サンプルコードはコチラ．全体の流れとしてはndarrayを定義，reshape，dot，transposeを実装，それらを使ってtensordotを実装してみるとどうなるかをみていく．
前回の記事に続き，今回も型レベルでアレコレするのでアタマのほうはこんな感じ．singletonsも使っていく．
{-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} import Data.Singletons import Data.Singletons.Prelude.Enum import Data.Singletons.Prelude.List import Data.Singletons.Prelude.Num import GHC.TypeLits
shapeと中身の型aを型レベルに持つNDArray型を定義する．今回は中身の計算には興味が無いので，shapeに関する情報だけ抱えておくことにする．
data NDArray (shape :: [Nat]) a = NDArray (Sing shape) -- 中身はshape意外省略
まずは，numpy.reshapeを実装してみる．
reshape :: Product from ~ Product to => Sing to -> NDArray from a -> NDArray to a reshape = const . NDArray
要素数が同じでshapeの違う別のndarrayに変換する操作だが，別段不可思議なところは無い．コンテキスト部分により要素数が同じという条件を付けており，以下のように確かに条件に合わない場合は型検査で失敗する．
-- reshape可 reshapeable :: NDArray '[2,3,4] a -> NDArray '[3,8] a reshapeable = reshape sing -- 型検査でreshape不可 (次元の積が合わない) -- unreshapeable :: NDArray '[2,3,4] a -> NDArray '[3,3,4] a -- unreshapeable = reshape sing -- Couldn't match type ‘24’ with ‘36’
次に，numpy.dotを実装する．
dot :: (Last xs ~ Last (Init ys), Num a) => NDArray xs a -> NDArray ys a -> NDArray (Init xs :++ Init (Init ys) :++ '[Last ys]) a NDArray xs `dot` NDArray ys = NDArray (sInit xs %:++ sInit (sInit ys) %:++ SCons (sLast ys) SNil)
dot積を取る2つのndarrayのshapeから結果のshapeが決定する．1つ目のshape最後の要素と，2つ目のshape最後から2番目の要素が同じという条件が付いている．これも，以下のように条件に合わない場合と結果の型が合わない場合は型検査で失敗する．
-- dot可 dottable :: Num a => NDArray '[2,3,4] a -> NDArray '[3,4,2] a -> NDArray '[2,3,3,2] a dottable = dot -- 型検査でdot不可 (結果の型が合わない) -- undottable1 :: Num a => NDArray '[2,3,4] a -> NDArray '[3,4,4] a -> NDArray '[2,3,3,2] a -- undottable1 = dot -- Couldn't match type ‘4’ with ‘2’ -- 型検査でdot不可 (引数の型が合わない) -- undottable2 :: Num a => NDArray '[2,3,4] a -> NDArray '[4,3,2] a -> NDArray '[2,3,4,2] a -- undottable2 = dot -- Couldn't match type ‘4’ with ‘3’
最後に，numpy.transposeを実装する．
transpose :: Sort axes ~ EnumFromTo 0 (Length shape - 1) => Sing axes -> NDArray shape a -> NDArray (Map ((:!!$$) shape) axes) a transpose axes (NDArray shape) = NDArray (sMap (singFun1 (toProxy shape) (shape %:!!)) axes) where toProxy :: Sing (shape :: [Nat]) -> Proxy (Apply (:!!$) shape) toProxy _ = Proxy
条件は少し複雑になり，軸(次元)の転置方法に相当するパラメータaxesが，ちゃんとshape全体のpermutationを意味するパラメータになっていなければならない．これも，次のように各理由で整合しない場合は型検査で失敗する．
transposable :: Sing '[1,0,2] -> NDArray '[2,3,4] a -> NDArray '[3,2,4] a transposable = transpose -- transpose不可 (axesにshapeの長さ以上のものが含まれる) -- untransposable1 :: Sing '[1,0,3] -> NDArray '[2,3,4] a -> NDArray '[3,2,4] a -- untransposable1 = transpose -- Couldn't match type ‘3’ with ‘2’ -- transpose不可 (axesに同じ要素が2つ以上含まれる) -- untransposable2 :: Sing '[1,0,0] -> NDArray '[2,3,4] a -> NDArray '[3,2,2] a -- untransposable2 = transpose -- Couldn't match type ‘1’ with ‘2’ -- transpose不可 (axesの長さとshapeの長さが一致しない) -- untransposable3 :: Sing '[1,0] -> NDArray '[2,3,4] a -> NDArray '[3,2] a -- untransposable3 = transpose -- Couldn't match type ‘'[]’ with ‘'[2]’ -- transpose不可 (結果の型が合わない) -- untransposable4 :: Sing '[1,0,2] -> NDArray '[2,3,4] a -> NDArray '[3,2,5] a -- untransposable4 = transpose -- Couldn't match type ‘4’ with ‘5’
さて，reshape,dot,transposeが定義されたので，これらを使ってnumpy.tensordotが定義できる．はずである．実際に「こうすればいいよね」という感覚に従って実装してみよう．
tensordot :: (Num a, ns ~ Nub ns, ms ~ Nub ms, Map ((:!!$$) xs) ns ~ Map ((:!!$$) ys) ms) => NDArray xs a -> NDArray ys a -> (Sing ns, Sing ms) -> NDArray (Map ((:!!$$) xs) (EnumFromTo 0 (Length xs - 1) :\\ ns) :++ Map ((:!!$$) ys) (EnumFromTo 0 (Length ys - 1) :\\ ms)) a tensordot x@(NDArray xs) y@(NDArray ys) (ns, ms) = result where range n = sEnumFromTo (sing :: Sing 0) (n %:- (sing :: Sing 1)) notinns = range (sLength xs) %:\\ ns notinms = range (sLength ys) %:\\ ms tx = transpose (notinns %:++ ns) x ty = transpose (ms %:++ notinms) y dimsIn xs = sMap (singFun1 (toProxy xs) (xs %:!!)) where toProxy :: Sing (shape :: [Nat]) -> Proxy (Apply (:!!$) shape) toProxy _ = Proxy (oldxs, oldys) = (dimsIn xs notinns, dimsIn ys notinms) where rtx = reshape (SCons (sProduct oldxs) $ SCons (sProduct $ dimsIn xs ns) SNil) tx rty = reshape (SCons (sProduct $ dimsIn ys ms) $ SCons (sProduct oldys) SNil) ty result = reshape (oldxs %:++ oldys) (rtx `dot` rty)
とりあえずだが，コンテキストによる条件の表現としては，tensordotを取る2つのndarrayのshapeに対し，dotを取る部分の軸指定がpermutationの部分列になっており，かつ，指定された軸について同じ形をしているという条件相当を付けておいた．
このtensordotの定義は型検査に失敗し，5件くらいしか無いクセにトータル1200行くらいの長大なエラーメッセージを吐く．もちろん実装者も吐く．そして泣く．これは，ニンゲンには自明なことであっても，機械(型検査器)にはわからないことがあるためだ．それは，
- transpose時の条件，転置方法が正しくpermutationに相当する値(型レベルの)になっているかがわからない．(130行のエラー x txとtyについて2箇所)
- ニンゲンにとって，ある列の中からいくつかを取り出し(notinnsやnotinms)，取り出した後の最初や最後にくっつけて(transposeの引数)も，順番が変わるだけで中身は一緒(=permutation)であることはわかる．
- けど，機械(型検査器)にとっては自明ではない．
- reshape時の条件，reshape前後の要素数が(型レベルで)同じであるかどうかがわからない．(280行のエラー x rtxとrtyについて2箇所 + 400行のエラー x resultについて1箇所)
- ニンゲンにとって，ある正数の列を2グループに分け(xsに対するoldxsとそれ以外，ysに対するoldysとそれ以外)，それぞれの積を取ったものの積は，元の列の積と同じことはわかる．
- けど，機械(型検査器)にとっては自明ではない．
ことからきている．dotの条件についてのエラーが出ていないが，この条件についてはわかっているのかというと，それはtensordot自体の条件(Mapのやつ)から機械(型検査器)にもわかる．また，reshapableやtransposable等で使ったとき問題無かったのは，具体的な型レベルでの値(型レベル自然数リテラル)が入っているためであり，対して今回のtensordotの定義中では(型)変数のままなので，機械(型検査器)が計算を進められるかの状況が異なる．
このエラーを解決するためには，恐らく2つ方法がある．
- 無視する．といってもエラーではどうしようもないので前回の記事と同じような方法を使い，transposeやreshapeを使ってもエラーにならないケースを作り出す．ここで無視するのは以下2点だ，
- (ニンゲンとって自明にunreachableな)エラーケースがコード上発生すること
- これらを使う人には条件を示すことを要請する癖に，自分が使うときは自明だからいいだろと無視するカッコ悪さ
- 使える情報から機械(型検査器)がわかる情報にニンゲンが変換して教えてあげる．
前者について，ニンゲンにとって自明とは言うものの，複雑な条件になると本当に自明かどうかはニンゲンにもわかるか怪しいし，そもそも自明だと思ったこと自体も錯誤かもしれない．わざわざ型レベルでどうにかしようという話自体，そういったニンゲンによるミスをどうにかしようというモチベーションだった筈であり，解決の方向性としてはどうなのソレという感がある．
後者が正攻法となるが，実は，それがこの界隈で何と呼ばれているか私達は既に知っている．それは定理証明と呼ばれるヤツである．こうなるとワンチャン証明器からextractしたほうが使い易いまである．Haskellでも実際GHC.TypeLits.Natはペアノ数ではない*2ようなので，そのままではInductionが効かず証明相当のサギョウがやりにくいことこの上無かったりする．
まとめると，各種契約を型で云々～に期待されるようガチガチに型レベルで設計されたものは，言語にも使う側にも型レベルでガチな取り組みを求められることがある．型レベルへ条件を持ち上げることは「人はミスせずに作業ができるか」という問題を「人は定理証明ができるか」という問題へと変換することなのだ．となると，最近null安全？とかの話から複雑な契約も型でヤッター！と言ってる方々はたぶん皆このへんについても「覚悟完了！当方に迎撃の準備有り！」なので，定理証明についても何でも*3聞いて大丈夫ということになる．やったぜ
実世界を扱う依存型プログラミングのたぶん基本～外界から安全な世界までの道
依存型ならさらに安全にプログラミングできちまうんだ！と言ったところで，「無料で遊べちまうんだ！」とか「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値のパターンマッチでユニフィケーションを発生させる
- 制約に対して型が整合しない経路に対してはデータ形式のエラー，目的の処理は型が合わずうっかりですら使えない
- 制約に対して型が整合した経路では目的の処理を行える
という感じになる．
今回のソースはココ
stackを通してのコンパイルにとても時間がかかる条件
ghc 7.10 からみられるようになった現象で，放置しているうちにやや旬を過ぎてしまっている感もある話題なのだが，その後特に改善してるわけでもないのと最近踏まれたのを見たので念のために記しておこうかなと．
コンパイル時間ghc-7.8で1分40秒なやつがghc-7.10で6分かかるようになってて助けてクーガー兄貴
— Noriyuki OHKAWA (@notogawa) October 31, 2015
結論から言うと，一定レベル以上の最適化付きで，大きな型レベル計算を含んだ型を持つインターフェースを含む場合…となる．このときコンパイルが遅い．厳密には遅いのはコンパイルではないが．
上記ツイートで問題にしてたJinja2サブセットのテンプレートエンジンであるhaijiは，hackageに上げる前のPoC段階で記事にもした．
なのでここでは概要のみだが，haijiは「レンダリングにどんな名前のどんな型の変数を持つ辞書が必要か」をj2テンプレートの型としてTemplate Haskellで型付けし，条件を満たした辞書をレンダラから渡さないと型検査で弾かれるようにしている*1．ここで利用される辞書はテンプレート変数名の型レベル文字列からその変数の型を引けるような型レベル辞書型を持っており，型レベル文字列とか型レベルリスト上での計算をモリモリ行って辞書同士の結合等を実装している．とにかく，型が型レベル計算で生成され，しかもTemplate Haskellでj2テンプレートから自動生成されているため，型検査に失敗したりすると非常に長いエラーが出たりする．
一方でghc側の事情だが，7.8 から 7.10 時の変化として，通常の最適化(-O)有効時，モジュール外に公開されるもののみならずモジュール内で閉じたものであっても詳細な型情報が.hiファイルに吐かれるようになった*2ようだ．これに伴い.hiファイルのサイズも大きくなっている．
次にstack側の事情になる．stackはコンパイルオプションとしてghcに-ddump-hi -ddump-to-fileオプションを渡す．これは，.hiファイルの中身をhuman readableにした.dump-hiファイルを吐かせるオプションだ．.stack-workディレクトリ以下を見てもらえば.dump-hiファイルが確認できるだろう．stackはこのオプションを問答無用でghcに渡し，現時点では渡さないという選択肢は取れない．どうも.dump-hiファイルの情報を使っているとのこと．
これらの事情が絡み合い，「ghc 7.10 以降stackを通してコンパイルすると異常に大きな.ddump-hiファイルが吐かれる」状況が発生する．
コレ-ddump-hiがヤバい
— Noriyuki OHKAWA (@notogawa) November 1, 2015
THで型レベル計算がモリモリ入るようなものを生成させると，stackがビルド時に付けてくる-ddump-hiとによってアホほど大量のinterfece dump吐いてビルド時間が遅くなる．特に最適化付きの場合，露出してないものの情報も吐かれて死
— Noriyuki OHKAWA (@notogawa) November 1, 2015
7.1M Nov 5 00:28 tests.dump-hi.ghc-7.8.lts-2.22.with-O
— Noriyuki OHKAWA (@notogawa) November 4, 2015
↓
49M Nov 5 00:36 tests.dump-hi.ghc-7.10.lts-3.11.with-O
アカンやつ過ぎる
ファイルサイズも問題無いとは言えないのだが，それ以上にどうも型レベル計算で大きく構成された型に対してはhuman readable dumpの生成か整形あたりが特に遅いようで，これがstackでのコンパイル時間にまるまる乗ってしまう．当然だが，stackを使わない(=dump系オプションを渡さない)ならば遅くはならない．とはいえ，そういうわけにもねぇ．
関数プログラミング実践入門が増補改訂です
関数プログラミング実践入門という本を書きました - ぼくのぬまち 出張版 に引き続き，よろしくおねがいします．
![[増補改訂]関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (WEB+DB PRESS plus)](http://ecx.images-amazon.com/images/I/51MNfQJfuUL._SL160_.jpg "[増補改訂]関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (WEB+DB PRESS plus)")
[増補改訂]関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (WEB+DB PRESS plus)
- 作者: 大川徳之
- 出版社/メーカー: 技術評論社
- 発売日: 2016/09/24
- メディア: 単行本（ソフトカバー）
- この商品を含むブログを見る
なにがどうなったか
基本的にはトピックの追加となります．1章のサンプルを追加したり，Strict(GHC8)がらみの話を追加したり，各非関数型言語で関数プログラミングをするにあたって機能や特性などを見てみる章を追加したりといった感じになってます．
逆に言うと，既存トピックに関して大きな変更があるわけではありません．stack使うようにしたりとなります．
経緯と執筆中のアレコレ
2015年10月終わり頃，増補改訂の話が来る．そういうのもあるのか．
執筆自体は新規追加部分については前回とほぼ同じスタイルで行う．既存部分の修正についてはpdf上でイロイロする作業の割合が多かった．
当初予定されていた締め切りが前倒しされてくるという謎現象を目にする．そういうこともあるのね．別の書籍のレビュアしてたり，お仕事のほうも割とビジーになってしまったりと，なかなか苦心しつつ進行していた．
感想
前回エラッタが多かったというのもあり，今回も編集さんには結構負担かけてしまっていたように思う．注意深く確認してくれていたように感じる．
これは今回の感想というより前回からの感想になるかもだが，いくら注意深く取捨選択しても意図通りに伝えることの難しさというものの質が少し違うんだなとの実感があった．意図通りに伝えることが難しいというのは，当然執筆だけではなく開発とかのお仕事でも同じではある．しかし，お仕事のほうでは同僚相手であれお客様相手であれ一度に対する相手が少数であることが多く，従ってどんな知識・背景を持っているかが想定し易い．自然，何をどう伝えると理解してもらえるかの調整が効き易い．対して書籍となると，もちろん想定読者というペルソナはあるにせよ，それにマッチしない人が手にすることも，また，好みが大きく振れてる人が手にとることもある．たとえば，重要ではないと思える部分を削いだものを好む人も，逆に，あえて網羅的に明示するのを好む人も両方いる．「～が書かれていない」と「～がくどい」が同じ項目に対する感想として得られることもある．質が違うというのはこういった意味でのことだ．
最近では個々の関数型言語はそれぞれにメジャーになってきており，採用事例も書籍も勉強会も増えてきている．しかし，Haskellの勉強会における自己紹介等であっても「仕事では～を使っています」に関数型言語が入る比率は微増していると感じはするものの多くはない．特にこの日本だと，「(その言語を)自分たちのサービス・製品で使っている」だけではなく「みんなが知ってる会社から(その言語での)仕事が下りてくる」ということに意味がありそうな気がするので，難しいだろうけどそういうケースがよく見られるレベルまで普及すればいいかなとぼんやり思ったりしている．
ところで，今週は ICFP 2016 があるので，関数プログラミングの深淵に興味がある人は覗いてみるのがよい．深淵もまたあなたを覗いているかもしれないが．
Hackageメタデータの依存関係だけ更新してどうするの？
(追記) cabal update で反映される模様？
Agda-2.4.2.5のDependenciesで，unordered-containersを見て欲しい．依存関係が >=0.2.5.0 && <0.2.6 となっているが，これはHackage上のパッケージメタデータのみをパッケージアップロード後に編集したもので，実際2016/1/25現在見えているメタデータはrev 1となっている．編集前の依存関係では >=0.2.5.0 && <0.3 であり，これはパッケージ登録時の.cabalファイルからのものだ．
実際，unordered-containers-0.2.6.0によりAgda-2.4.2.5のビルドは失敗する．
src/full/Agda/Utils/HashMap.hs:3:5:
Ambiguous occurrence ‘mapMaybe’
It could refer to either ‘Agda.Utils.HashMap.mapMaybe’,
defined at src/full/Agda/Utils/HashMap.hs:17:1
or ‘HashMap.mapMaybe’,
imported from ‘Data.HashMap.Strict’ at src/full/Agda/Utils/HashMap.hs:8:1-37
src/full/Agda/Utils/HashMap.hs:3:5:
Conflicting exports for ‘mapMaybe’:
‘module HashMap’ exports ‘HashMap.mapMaybe’
imported from ‘Data.HashMap.Strict’ at src/full/Agda/Utils/HashMap.hs:8:1-37
‘mapMaybe’ exports ‘Agda.Utils.HashMap.mapMaybe’
defined at src/full/Agda/Utils/HashMap.hs:17:1
src/full/Agda/Utils/HashMap.hs:4:5:
Ambiguous occurrence ‘alter’
It could refer to either ‘Agda.Utils.HashMap.alter’,
defined at src/full/Agda/Utils/HashMap.hs:23:1
or ‘HashMap.alter’,
imported from ‘Data.HashMap.Strict’ at src/full/Agda/Utils/HashMap.hs:8:1-37
src/full/Agda/Utils/HashMap.hs:4:5:
Conflicting exports for ‘alter’:
‘module HashMap’ exports ‘HashMap.alter’
imported from ‘Data.HashMap.Strict’ at src/full/Agda/Utils/HashMap.hs:8:1-37
‘alter’ exports ‘Agda.Utils.HashMap.alter’
defined at src/full/Agda/Utils/HashMap.hs:23:1でも今は，そんな事はどうでもいいんだ．重要なことじゃない．
問題はHackageに登録されたパッケージメタデータで依存関係を編集したところで，そのパッケージそのものの依存関係の実体(つまり，アップロードされたパッケージ内のcabalファイルの中身)には何も関係が無いということだ．このことは古事記とメタデータrevisionのページにもそう書かれている
Package maintainers and Hackage trustees are allowed to edit certain bits of package metadata after a release, without uploading a new tarball. Note that the tarball itself is never changed, just the metadata that is stored separately.
つまり，Agda-2.4.2.5に含まれるAgda.cabalファイルのunordered-containers依存関係は，依然として >=0.2.5.0 && <0.3 である．cabal install時にビルド失敗するunordered-containers-0.2.6.0を引き入れるのに全く躊躇が無い．アップロードしたパッケージを変更できないのだから，メタデータを弄ろうが弄るまいがこのこと自体には変わりは無い．インターフェースが消えた*1ならともかく増えた*2ことでビルド失敗するようになったAgdaは不運だったとも言える．だけど，それならそれで依存関係弄ってバージョン上げるとかするような話であり，Hackageのメタデータだけ弄っても何の解決にもならない．むしろ混乱を招く．
そもそも，.cabal内に入ってないデータならともかく，入ってるデータまでパッケージとは独立にHackage上で編集できるって一体何のための機能なんだ．正直理解できない．
stackで行く地獄巡りの旅
Haskell使い 十戒
一、常に型と共にあれ
一、不要な式より潰すなかれ
一、無益にIOするなかれ
一、つけられたらつけかえせ
一、つけられる前につけろ
一、一日一善
一、遅延を疑ってみよ
一、気を付けよ甘い型付けと暗い道
一、小さなコードで大きな仕事
一、あがめよ讃えよ汝の師匠
ﾁｬﾗﾗﾗﾗｰ ﾁｬﾗﾗﾗﾗｰ ﾁｬﾗﾗｰﾗ ﾗｰﾗ ﾗｰﾗﾗｰ ﾗﾗﾗｰ
この記事はHaskell Advent Calendar 2015 - Qiitaの2日目の記事です．
今回は，stackにも使い慣れてきてそろそろhellが恋しくなってきた方々のため，stackに頼りつつもhellを拝むための方法を紹介する．ここでとりあげてるstackは0.1.6.0時点なので，後々なら何か変わってるかも
やり方はとても簡単で，システムghcの依存するパッケージバージョンがstackのresolverに含まれるものとズレている場合，--system-ghc使っていれば(つまりデフォルトで)既にあなたは地獄に来ている．やったぜ
たとえば，gentooのghc-7.10.2-r1.ebuildではtransformers-0.4.3.0が使われる．しかし，ghc-7.10系resolverであるlts-3ではtransformers-0.4.2.0が使われる．すると，transformersを使うパッケージをビルドするときに，
Warning: This package indirectly depends on multiple versions of the same package. This is highly likely to cause a compile failure. package transformers-compat-0.4.0.4 requires transformers-0.4.2.0 package primitive-0.6.1.0 requires transformers-0.4.2.0 (snip.) package QuickCheck-2.8.1 requires transformers-0.4.2.0 package ghc-7.10.2 requires transformers-0.4.3.0
のように，package DBに複数バージョンの同一パッケージがある状態でビルドが行われてしまう．モノによっては関数とかインスタンスとか型とか見つからなかったりしてコンパイルエラーを生じる．
他にも，システムghcの依存するパッケージバージョンが同じだったとしても，あるディレクトリで--no-system-ghc，別のディレクトリでは--system-ghcを使ったりすると条件によっては壊れる．今のstackは同一のpackage DBに--system-ghcのものも--no-system-ghcのものも区別せずに放り込んでしまう．本来はこれらの条件でも分離しておかなければならないように思う．
あとは，たぶんシステムにフラグ付きのパッケージをデフォルト以外のフラグ設定でインストールして使ってる場合もhellってないか注意が必要となる．
とりあえずstackを使ってhellを見ないようにするためには必ず--no-system-ghcで使うという決め打ちが必要になる．しかし，今lts-3系の--no-system-ghcでダウンロードされてくるghc-7.10.2バイナリの場合，環境によっては次の問題に当たってしまって使えないことがあったりする．
$ stack setup
The GHC located at /home/notogawa/.stack/programs/x86_64-linux/ghc-7.10.2/bin/ghc failed to compile a sanity check. Please see:
https://github.com/commercialhaskell/stack/blob/release/doc/install_and_upgrade.md
for more information. Exception was:
Running /home/notogawa/.stack/programs/x86_64-linux/ghc-7.10.2/bin/ghc /tmp/stack-sanity-check10231/Main.hs -no-user-package-db exited with ExitFailure 1
[1 of 1] Compiling Main ( /tmp/stack-sanity-check10231/Main.hs, /tmp/stack-sanity-check10231/Main.o )
Linking /tmp/stack-sanity-check10231/Main ...
/usr/lib/gcc/x86_64-pc-linux-gnu/4.9.3/../../../../x86_64-pc-linux-gnu/bin/ld: /tmp/stack-sanity-check10231/Main.o: relocation R_X86_64_32S against `stg_bh_upd_frame_info' can not be used when making a shared object; recompile with -fPIC
/tmp/stack-sanity-check10231/Main.o: error adding symbols: Bad value
collect2: エラー: ld はステータス 1 で終了しましたこういった環境では，むしろstack自体を使わないほうがいいまである．というか事実上使えない．
恐らく今後各ディストリビューションで用意するghcも積極的にstackageに合わせた依存関係にシフトするだろうし，--system-ghcについてだけ言えば過渡期にのみ生じるトラブルかもしれない．というか，ghc-7.10系のパッケージ持ってるディストリビューションが今現在そもそもそんなに多くないかもしれない．ただ，自分だけかもしれないとはいえ実際割と踏んでしまうことがある上，stackは特にこの業界では何故こんな名前にしたのか正気を疑う程に検索性の低いワードであるため，トラブル情報を漁るのも大変だ．備えよう．
