実世界を扱う依存型プログラミングのたぶん基本～外界から安全な世界までの道

依存型ならさらに安全にプログラミングできちまうんだ！と言ったところで，「無料で遊べちまうんだ！」とか「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

証明だけに限った話ではなく，実用，特に入出力(特に入力)込みで依存型をみてみると，その最も大きな影響はメインの処理に入る前段階でのデータ・データ間の性質の検証またはクリーンアップに対する型安全性の導入・強要という形で現れる．値レベルで値だけ見て性質を満たしていなければ目的の関数が実行時に失敗するしそれでも仕方がないという状況であったものが，依存型の導入によって，型レベルでも性質を満たしたことが型検査器にわかる経路でしか目的の関数を使うことができないというように変わる．現実はクソなので，入力されてくるデータがクサレてるのは仕方が無いことで，それを原因として実行時エラーが起きるのは当然のことであり，だからといって何も起きないようにしようとかいう話をしているわけでは決してない．目的の処理に入るより前の段階で，クサレてるデータをちゃんとクサレてると判断し実行時エラーを出す，まさにその判定部分にミスが入り込まないよう型で守ることができるようになる．型合わせゲーが最高めんどくさいけど．

おおまかにまとめると，流れとしては

1. 依存型ガチガチで型付け
2. 依存型を最大限利用して目的の処理を安全に書いておく
3. 依存型を構成する要素のうち，外部データで決まる部分を存在型で隠した型を用意する
4. 存在型の中に隠された依存型の値を参照できる関数を用意する，たぶんローンパターンがいい
5. 外部からデータを読み，依存型の値を構成，さらに存在型で隠した値を構成する
6. 型の上での必要な制約が満たされるようGADT値のパターンマッチでユニフィケーションを発生させる
7. 制約に対して型が整合しない経路に対してはデータ形式のエラー，目的の処理は型が合わずうっかりですら使えない
8. 制約に対して型が整合した経路では目的の処理を行える

という感じになる．

今回のソースはココ

stackを通してのコンパイルにとても時間がかかる条件

ghc 7.10 からみられるようになった現象で，放置しているうちにやや旬を過ぎてしまっている感もある話題なのだが，その後特に改善してるわけでもないのと最近踏まれたのを見たので念のために記しておこうかなと．

コンパイル時間ghc-7.8で1分40秒なやつがghc-7.10で6分かかるようになってて助けてクーガー兄貴

— Noriyuki OHKAWA (@notogawa) October 31, 2015

結論から言うと，一定レベル以上の最適化付きで，大きな型レベル計算を含んだ型を持つインターフェースを含む場合…となる．このときコンパイルが遅い．厳密には遅いのはコンパイルではないが．

上記ツイートで問題にしてたJinja2サブセットのテンプレートエンジンであるhaijiは，hackageに上げる前のPoC段階で記事にもした．

notogawa.hatenablog.com

なのでここでは概要のみだが，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
↓
49M Nov 5 00:36 tests.dump-hi.ghc-7.10.lts-3.11.with-O
アカンやつ過ぎる

— Noriyuki OHKAWA (@notogawa) November 4, 2015

ファイルサイズも問題無いとは言えないのだが，それ以上にどうも型レベル計算で大きく構成された型に対してはhuman readable dumpの生成か整形あたりが特に遅いようで，これがstackでのコンパイル時間にまるまる乗ってしまう．当然だが，stackを使わない(=dump系オプションを渡さない)ならば遅くはならない．とはいえ，そういうわけにもねぇ．

*1:そのためテンプレートは実行時ではなくコンパイル時にロードされる．

*2:モジュールを跨いだ最適化に使える情報を増やすためか

関数プログラミング実践入門が増補改訂です

関数プログラミング実践入門という本を書きました - ぼくのぬまち 出張版 に引き続き，よろしくおねがいします．

[増補改訂]関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (WEB+DB PRESS plus)

なにがどうなったか

基本的にはトピックの追加となります．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上で編集できるって一体何のための機能なんだ．正直理解できない．

*1:unordered-containersのバージョンが0.3以上になるはず

*2:unordered-containersのバージョンが0.3以上にならないかもしれない，実際0.2.6.0になった

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バイナリの場合，環境によっては次の問題に当たってしまって使えないことがあったりする．

#9007 (fails to build with hardening flags enabled (relocation R_X86_64_32 against `stg_CHARLIKE_closure'...)) – GHC

$ 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は特にこの業界では何故こんな名前にしたのか正気を疑う程に検索性の低いワードであるため，トラブル情報を漁るのも大変だ．備えよう．

Travis CI等でstackのresolverにstackage latest nightlyを使う

stackでstackage nightlyのresolverを使おうとしても，stack.yamlには

resolver: nightly-2015-10-27

のように日付まで用意しないと使えない．lts-2やlts-3についても同様で，lts-3.*まで指定する必要がある．

Travis CI等で各resolverについてマトリクステストする場合，ltsのほうはともかくnightlyについてはビルド時点で最新のものを常に見るようにして欲しい．どうにかなりませんかという話は出ているのだが，とりあえずこの件がどうにかなるまでのツナギ

stackageのリダイレクトがnightlyやlts-*の最新を知ってるので，次のようなスクリプト用意しておいて，

#!/bin/bash

LATEST_VERSION=$(wget -O/dev/null https://www.stackage.org/$1 2>&1 |
                     grep "https://www.stackage.org/$1" |
                     tail -n1 |
                     sed "s/.*$1/$1/")
sed "s/^resolver: .*/resolver: ${LATEST_VERSION}/" stack.yaml

元となるstack.yamlからresolverを書き変えたものを生成して使わせるようにする，

before_install:
  - ./latest $RESOLVER > stack-travis.yaml
  - export STACK_YAML=stack-travis.yaml

あとはマトリクス指定で

matrix:
  include:
    - env: RESOLVER=lts-2
    - env: RESOLVER=ghc-7.10.2
    - env: RESOLVER=lts-3
    - env: RESOLVER=lts-3.10
    - env: RESOLVER=nightly
  allow_failures:
    - env: RESOLVER=nightly

のようにしておくと，lts-2(の最新)，ghc-7.10.2，lts-3(の最新)，lts-3.10，nightly(の最新)という設定になる．現時点で具体的には，lts-2 → lts-2.22，lts-3 → lts-3.11，nightly → nightly-2015-10-27 となる．

Jinja2サブセット的な型付きテンプレートエンジンhaiji

年末年始なので何か作ろうかなと思いhaiji*1というライブラリを作ってみてる．

まぁ，なんというか最近ansible*2よく使ってたこともあってイロイロ思うトコロあったりなかったり．

大概のテンプレートエンジンにおいて，個人的にイマイチ気に入らないトコロは未定義変数の扱いだ．ある変数の値を展開しようとして，「テンプレートを展開しようとした環境でその変数の値が未定義なとき」を考えるなんてハッキリ言って正気とは思えないし，未定義なときは空文字列と同じになるとかもお前ホントそれでいいのかと．．

具体的には，テンプレートの展開を行っている環境からある変数を消す，あるいは，変数名を変更するといった変更に伴い，展開結果が変わってしまうかどうかが実際に動かすまでは簡単にはわからなくなるという点が嫌．これは，erbのrender partialやJinja2のincludeといったテンプレート自体の部品化を促進する程，メンテナンス性にダメージもまた与えることに繋がっていく．

プロダクトが大きくなり「実際にいろんな箇所で展開されているテンプレート部品」があるときに，先程のような変数名やら何やらの変更を行っても本当に望み通りの展開結果を保っているか簡単に確認できるだろうか？変更によってある変数が未定義になっても「未定義時の動作」が定義されていたり空文字になったりであれば，未定義であること自体がプログラマの意図していない事態だとしても，テンプレートは正常に展開されて意図しない結果を無批判に作り出してしまう．

結果として

• 変数名がなんとなく不適切なものになってきちゃったけどテンプレートの展開結果を壊すかもしれないから変更したくない
• 最早不要かもしれないけど実際にテンプレートのどこかで使われているかもしれないからコードを消したいけど消せない
• テンプレート側に変数の参照を追加したときに，ある箇所からは定義されて渡されてくるけどある処理からはそうでない．具体的にどれが実際ソレなのか

など後ろ向きな力がかかることになる．メンテナンスのハードルが高くなり，またひとつ地獄の釜の蓋が開く．

無自覚に何かを余計なことを引き起こしてしまいかねない要因は極力排除したい．

ひとつの解決策として，テンプレートが要求する環境に対し厳密に型を付けるという策が考えられる．テンプレートの展開を行う環境に「ある変数が定義されているべき」という要求を型で表現する．テンプレート展開時には，その要求を満たすような環境を提供すればいい．そして適合していなければ型検査に失敗してもらうのだ．

haijiはこの考えを基本にして実験的に作ってみたJinja2のサブセット的テンプレートエンジンだ．雰囲気はリポジトリのexample.hsとexapmle.tmplを見てもらうのがよいだろう．実際にJinja2を入れてexample.pyと比べてみればいい．

中身はどうしてもTemplateHaskellと依存型で伊東ライフにはなる．

たとえば，以下のようなhaijiテンプレートは，

{{ foo }}

レンダリングするときに次のような型の値を要求する．これがレンダリングのために最低限必要な環境の型ということだ．

TLDict '[ "foo" :-> TL.Text ]

実際には，型レベルリストに余計な型が入っていても，実際に使っているものが入っていればOKで，次のような型の値でもレンダリングはできる．使われないだけだ．

TLDict '[ "foo" :-> TL.Text, "hoge" :-> Int ]

展開が複数ある以下のようなhaijiテンプレートなら，

{{ foo }}{{ bar }}

レンダリングするときに次のような型の値を要求する．

TLDict '[ "foo" :-> TL.Text, "bar" :-> Int ]

さらに，以下のようなhaijiテンプレートであれば，

{{ foo.bar }}

レンダリングするときに次のような型の値を要求する．

TLDict '[ "foo" :-> TLDict '[ "bar" :-> TL.Text ] ]

他にも，以下のようなhaijiテンプレートであれば，

{% for item in items %}
  <li>{{ item.foo }}</li>
{% endfor %}

レンダリングするときに次のような型の値を要求する．

TLDict '[ "item" :-> [ TLDict '[ "foo" :-> TL.Text ] ] ]

もし，次のように，同じ変数itemsがテキストにもリストにも判断されるような箇所がある場合，このテンプレートはコンパイルエラーになる．

{{ items }}
{% for item in items %}
  <li>{{ item.foo }}</li>
{% endfor %}

他にもif〜(else)〜endifや，includeに対応している．

もし，テンプレート内で使われている変数を変更したり追加したりした場合，そのテンプレートをレンダリングしている箇所で変更後に要求されるようになった変数を与えていなければ，次のように型検査に失敗してコンパイルエラーになる*3．逆に，実際にテンプレートで使っている変数を消してしまってレンダリングしても同様のコンパイルエラーになる*4．

example.hs:14:39:
    No instance for (Retrieve (TLDict '[]) "navigation" [x0])
      arising from a use of ‘retrieve’
    In the second argument of ‘map’, namely
      ‘retrieve dict_a7nS (Key :: Key "navigation")’
    In the second argument of ‘($)’, namely
      ‘(map
          (\ x_a7nT
             -> \ esc_a7nU dict_a7nV -> LT.concat ["    <li><a href=\"", ....]
                  esc_a7nR (Text.Haiji.TH.add x_a7nT (Key :: Key "item") dict_a7nS))
          (retrieve dict_a7nS (Key :: Key "navigation")))’
    In the expression:
      (LT.concat
       $ (map
            (\ x_a7nT
               -> \ esc_a7nU dict_a7nV -> LT.concat ["    <li><a href=\"", ....]
                    esc_a7nR (Text.Haiji.TH.add x_a7nT (Key :: Key "item") dict_a7nS))
            (retrieve dict_a7nS (Key :: Key "navigation"))))
Failed, modules loaded: Text.Haiji, Text.Haiji.Types, Text.Haiji.Parse, Text.Haiji.TH.

Proof of Concept的にザックリ作り始めたばかりなので，まだ機能的に十分ではないし，コレどうしようかと思っている箇所もいくつかあるし，インターフェースも決定し兼ねてる．hackageにも上げてない．そもそもLLやフロントの人からは「こんなゲンミツにしてどうすんだなんとなくでも動いてるのが確認できるからいいんじゃねーか」という意見もあるかもしれない．なお速度は最初から考えないようにしてる模様．

*1:廃寺

*2:テンプレートエンジンはJinja2ね

*3:ので，何かが足りないことなどがわかる

*4:ので，コンパイルエラーにならなければ消しても展開結果には影響が無いものだとわかる