singletonsの型レベル関数を使ってしまうと示せない性質の例
↓の話
実際singletonsが乱舞するんだけど，singletonsから提供されてる型レベル関数の中には使うと「それ以上証明が進まなくなる」やつが結構な割合で含まれてて，面白味のあるない以前に怒りが先行してしまう．あれは型レベル計算のためのライブラリでしかなくて証明のためのライブラリにはなれてない． https://t.co/ckCcUpWQLK
— Noriyuki OHKAWA (@notogawa) January 3, 2019
サンプルコードはここ
サンプルコードでやろうとしていることは「リストの反転はリスト内要素の置換の一種であることを示す」というもの
まず，2つの型レベルリストが置換の関係にあることを定義する．
data Permutation :: [k] -> [k] -> Type where PermutationNil :: Permutation '[] '[] PermutationSkip :: Sing a -> Permutation xs ys -> Permutation (a : xs) (a : ys) PermutationSwap :: Sing a -> Sing b -> Permutation (a : b : xs) (b : a : xs) PermutationTrans :: Permutation xs ys -> Permutation ys zs -> Permutation xs zs
少しこの定義について確認していく．実際にひとつの例について置換関係にあること確認してみる．
testPermutation :: Permutation [1,2,3,4] [2,4,3,1] testPermutation = PermutationTrans (PermutationSwap s1 s2) $ PermutationTrans (PermutationSkip s2 $ PermutationSwap s1 s3) $ PermutationTrans (PermutationSkip s2 $ PermutationSkip s3 $ PermutationSwap s1 s4) $ PermutationSkip s2 $ PermutationSwap s3 s4
置換は同値関係のひとつなので，反射律，
refl :: Sing xs -> Permutation xs xs refl SNil = PermutationNil refl (SCons x xs) = PermutationSkip x $ refl xs
対称律，
sym :: Permutation xs ys -> Permutation ys xs sym PermutationNil = PermutationNil sym (PermutationSkip s p) = PermutationSkip s $ sym p sym (PermutationSwap a b) = PermutationSwap b a sym (PermutationTrans p1 p2) = PermutationTrans (sym p2) (sym p1)
推移律が示せる．
trans :: Permutation xs ys -> Permutation ys zs -> Permutation xs zs trans = PermutationTrans
先頭への要素の追加と，途中への要素の追加は，置換関係的には同じことを意味する．といった性質も示せる．
here :: Sing a -> Sing xs -> Sing ys -> Permutation (a : xs :++ ys) (xs :++ (a : ys)) here a SNil ys = PermutationSkip a $ refl ys here a (SCons x xs) ys = PermutationTrans (PermutationSwap a x) (PermutationSkip x $ here a xs ys)
さて，反転が置換の一種であること reverseIsPermutation は，
reverseIsPermutation :: Sing xs -> Permutation xs (L.Reverse xs)
のような型をしている．しかし，実際にこれの実装(=証明)を与えようとすると，
reverseIsPermutation SNil = PermutationNil reverseIsPermutation (SCons x xs) = _
までしか進められない．このtyped holeを確認すると，
[-Wtyped-holes]
• Found hole:
_ :: Permutation
(n0 : n1)
(Data.Singletons.Prelude.List.Let6989586621679793554Rev
(n0 : n1) n1 '[n0])となっている．Let6989586621679793554Revって何と，singletonsライブラリのreverseの定義を確認すると，
$(singletonsOnly [d| (snip.) reverse :: [a] -> [a] reverse l = rev l [] where rev :: [a] -> [a] -> [a] rev [] a = a rev (x:xs) a = rev xs (x:a) (snip.) |])
であり，このreverseの定義からTHで生成されるReverseはexportされているが，reverse定義中のwhere節にあるrevはexportされていないので，そこを期待した型が現れてしまうと証明が進められずに止まってしまう．
これはもうどうしようもないので，やるなら自前でreverseを定義して補助関数も参照できるようにしなければならない．
$(singletonsOnly [d| myReverse :: [a] -> [a] myReverse l = myReverseAcc l [] myReverseAcc :: [a] -> [a] -> [a] myReverseAcc [] ys = ys myReverseAcc (x:xs) ys = myReverseAcc xs (x:ys) |])
このmyReverseの定義から生成される MyReverse や MyReverseAcc により，同様に反転が置換であることを示すと
myReverseIsPermutation :: Sing xs -> Permutation xs (MyReverse xs) myReverseIsPermutation xs' = gcastWith (nilIsRightIdentityOfAppend xs') (go xs' SNil) where go :: Sing xs -> Sing ys -> Permutation (xs :++ ys) (MyReverseAcc xs ys) go SNil ys = refl ys go (SCons x xs) ys = PermutationTrans (here x xs ys) (go xs (SCons x ys))
のように示すことができる．nilIsRightIdentityOfAppend は [] がリスト結合演算に対する右単位元であることを示している．
nilIsRightIdentityOfAppend :: Sing xs -> (xs :++ '[]) :~: xs nilIsRightIdentityOfAppend SNil = Refl nilIsRightIdentityOfAppend (SCons _ xs) = gcastWith (nilIsRightIdentityOfAppend xs) Refl
といったように，singletonsのSingの定義は別段問題無いが，Data.Singletons.Prelude 以下のモジュールで定義されている型レベル関数を使ったインターフェースは，それだけで証明ができなくなってしまうようなものが多数存在している．whereやletなどの補助関数により定義されているものは恐らく全滅じゃないだろうか．なので，こういったものをライブラリ外にexportする場合は，そのままsingletonsのものを使うのではなく適宜hideした上で，自分で定義した証明可能なもので代替してexportしたほうが親切じゃないかなと．
cerealのgetFloat*多用はメモリ長者にのみ許されし贅沢
約1年も書いてなかったのか．
ここ2,3年はそこそこのサイズの配列をどうこうする機会が多く，そういうとき特に何も考えなければ Data.Vector に突っ込んでおきたいキモチになる．で，実際に大きな配列をHaskellで扱うとメモリ不足でOOM Killerに殺されたりするわけだけど，そんな原因のひとつについて．
サンプルコードはココにあるのでヒマな人はどうぞ．
stack init stack build
まずputterというexecutableがそこそこ大きな要素数を持ったFloatの配列をlittle endianで出力する．
stack exec putter
これでカレントディレクトリにoutput.dat という50MBくらいのファイルができたかと．次にnaive-getterというexecutableでoutput.datを読み出す．やっていることは，Floatの配列に戻して総和を取り，元の配列の総和と一致するかを見ているだけ．
stack exec naive-getter
naive-getterの実装でByteStringからFloatのVectorに変換する部分は，次の通りcerealでgetFloat32leを使った脳直実装になっている．自然
runGetLazy (V.replicateM len getFloat32le) dat
しかし，コイツが想像以上にメモリをバカ食いするので，適当にプロファイルを見てみる．
stack build --profile stack exec -- naive-getter +RTS -hc -p -s stack exec -- hp2ps -c naive-getter.hp open naive-getter.ps
するとこんな感じになる．すごい．
8秒ちょいまではputterが出した配列をgetterでも再度作って総和とか評価してる部分なので無視するとして，Unboxed Vectorではないことを考慮しても以降のメモリ消費は立ち上がり過ぎている．どういうことかとgetFloat32leの実装を見に行くと，次のようになっている．
-- | Read a Float in little endian IEEE-754 format getFloat32le :: Get Float getFloat32le = wordToFloat <$> getWord32le (snip.) {-# INLINE wordToFloat #-} wordToFloat :: Word32 -> Float wordToFloat w = unsafeDupablePerformIO $ alloca $ \(ptr :: Ptr Word32) -> do poke ptr w peek (castPtr ptr)
1要素毎にコレやるわけだが，配列のようなコレクション中の要素を一気にたくさん変換するなら雑に次のような関数でいいかなと別の手段を用意する．
getFloat32leVector :: Int -> Get (V.Vector Float) getFloat32leVector n = do v <- V.replicateM n getWord32le return $ unsafeDupablePerformIO $ alloca $ \ptr -> do V.mapM (\x -> poke ptr x >> peek (castPtr ptr)) v
これでgetFloat32leを置き換えて次のように使ったrevised-getterを作り，
runGetLazy (getFloat32leVector len)
こちらでもnaive-getter同様にprofileを取る．
stack build --profile stack exec -- revised-getter +RTS -hc -p -s stack exec -- hp2ps -c revised-getter.hp open revised-getter.ps
結果はだいぶ減ったことがわかる．それでもまだ大富豪様ではあるわけだが
別に総和くらいだったらストリーム処理すばいいんだろうけどそれは簡単のために総和を置いてるだけで，現実的にはもっと配列全体をガチャガチャする処理が控えているためそういうわけにも．
コンテキストの順番を入れ換えると互換性が崩れることがある
(注:この記事はかなり前に書いて公開し忘れていたことに今日気付いたものです．もう当たり前になってるかもしれないけどもったいないので一応)
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拡張使っているとこういう漏れてきた互換性破壊を踏んでしまうかもしれないという認識を持つべきなのかな．
実世界を扱う依存型プログラミングのたぶん基本～外界から安全な世界までの道
依存型ならさらに安全にプログラミングできちまうんだ！と言ったところで，「無料で遊べちまうんだ！」とか「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系オプションを渡さない)ならば遅くはならない．とはいえ，そういうわけにもねぇ．
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は特にこの業界では何故こんな名前にしたのか正気を疑う程に検索性の低いワードであるため，トラブル情報を漁るのも大変だ．備えよう．
