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:ので，コンパイルエラーにならなければ消しても展開結果には影響が無いものだとわかる

ロジックパズルの解説

この記事は Haskell Advent Calendar 2014 6日目の記事です．

関数プログラミング実践入門 第6章 最終節にあるロジックパズルは，一体なにをどうやるとこのインターフェース設計になるのかという話．元々内容的に入門っぽくならないものないんだけど，特徴的なサンプルでもあったし詳解せずに「こういうこともできないようにすることができるよ」と紹介するに留めといた部分になる．

Bottom

まずはBottom型

data Bottom

通常data定義にはコンストラクタとかが伴う．たとえば，

data Bool = False | True

このBool型なら，FalseとTrueとによって真値と偽値相当の値を持つ．Bool型になる値は2つだ．

しかし，Bottom型には何もない．つまり，Bottom型は「ひとつも値を持たない型」だ．Bottom型を持つ値は「存在しない」．

もっと具体的にどういうことかというと，

boolValue :: Bool
boolValue = ?

の?にはBool値になる式を実装すれば型が合う．FalseやTrueでも実装したことになる．同様に，

bottomValue :: Bottom
bottomValue = ?

の?にはBottom値を記述すれば型が合う．しかし，Bottom値は「存在しない」ので，?に型の合う意味ある式を実装することはできない．

ここで「意味ある」式とわざわざ修飾したのは，実装してもあまり嬉しくないものなら実装できるものがあるからだ．

たとえば，止まらない再帰だったり

bottomValue :: Bottom
bottomValue = let loop = loop in loop

エラーだったり

bottomValue :: Bottom
bottomValue = error "dummy"

未定義だったり

bottomValue :: Bottom
bottomValue = undefined

これらは「任意の型になれる」ので，実装して型も合うが別に嬉しくもなんともない．なんだかよくわからないbottomValueはともかくとして，boolValueとしてこれらが実装されてて嬉しいかどうかイメージしてもらえばいい．

要点は，値を持たない型を持つ式はマトモには実装できないということだ．

(:==:)

次は(:==:)について，

data (:==:) :: k -> k -> * where
   Refl :: a :==: a

(:==:)は型の上での演算子であり，GHC拡張TypeOperatorsが必要になる．

また，この(:==:)のdata定義の仕方もまたHaskell標準のdata定義ではなく，GADT(Generalised Algebraic DataType)というGHCの拡張を使ったdata定義になっている．

GADTを使うと

data List a = Nil | Cons a (List a)

のようなリストの定義は，

data List a where
   Nil  :: List a
   Cons :: a -> List a -> List a

という定義になる．

このNilやConsは最終的にList a型の値を作っているが，GADTは，全てのコンストラクタが必ずしも同じ型の値を作らなくてもよい．次のようにコンストラクタによって型変数部分を選ばせることができる．

data Value a where
   IntValue  :: Int  -> Value Int
   BoolValue :: Bool -> Value Bool

この定義では，IntValueによってValue Int型の値を，BoolValueによってValue Bool型の値を，それぞれ作ることができる．逆に言うならば，Value Char型を作る方法は与えられていないので，Value Char型の値は「存在しない」．

話を(:==:)に戻す．

data (:==:) :: k -> k -> * where
   Refl :: a :==: a

(:==:)もGADTによって定義されている．コンストラクタReflがひとつだけ存在しており，(a :==: a)型つまり，(:==:)の左右の型が同じ場合の値になっている．逆に言うならば，(:==:)の左右の型が違う場合，その値は「存在しない」．つまり，(Int :==: Double)型や(Int :==: Int)型という型自体は作れる．しかし，値Reflを持つのは後者のみとなる．

ここで，kや*は種(kind)と呼ばれる「型の型」である．IntやDoubleといった通常の値を持つ型はみんな種*の型だ．kは種変数である．つまり，(:==:)は，両辺に同一の種変数kで表される種を持つ型をそれぞれ取り，種*の型になる．

Not

ある型pからBottom型への関数の型がNot pだと読める．

type Not p = p -> Bottom

しかし，先程Bottom型の値は「存在しない」という話をしたばかりなので，このような関数は定義できそうにない(=Not p型の値も存在しない？)ように思われる．が，実はひとつだけ定義できる条件が存在する，それはp型の値も同様に「存在しない」ときだ．

次のような関数notFuncを考えてみよう．

notFunc :: Not Bottom -- Bottom -> Bottom
notFunc bottomParam = ?

このときbottomParamはBottom型の値なので，引数になっているもののこの引数として入ってくる値は「存在しない」．では，実際には「存在しない」値に対してパターンマッチを行うと実際どうなるだろう．

パターンマッチとは「場合分け」だった．ある場合(=値があるコンストラクタで作られている状況)についてはこれこれこういう定義を与える，また別の場合(=値が別のコンストラクタで作られている状況)についてはこれこれこういう定義を与える．といったように関数を定義する．

「存在しない」値に対してパターンマッチするということは，「これこれこういう定義を与える」べき場合がそもそも「存在しない」ということだ．つまり，それ以上の定義を行わなくて良い．

GHC拡張EmptyCaseを使うと，値が「存在しない」型を認識し，次のようにパターンマッチを行うことができる．

notFunc :: Bottom -> Bottom
notFunc bottomParam = case bottomParam of {}

bottomParamをパターンマッチし「これこれこういう定義を与える」べき必要が無い状況であることを理解してくれる．

実は，「これこれこういう定義を与える」べき必要が無いので，引数に値の「存在しない」型の値があるのであれば，結果の型は何でもいい．

whatever :: Bottom -> a
whatever bottomParam = case bottomParam of {}

なので，Bottomでもいいのだ．

(:/=:)

(:/=:)はNotによって作られる．

type a :/=: b = Not (a :==: b)

aとbの型が異なるとき，(a :==: b)型はBottom型同様に値が「存在しない」ものだった．つまり，aとbの型が異なるとき，(a :==: b)型とは逆にNot (a :/=: b)型の値は存在し，aとbの型が同じとき，(a :==: b)型とは逆にNot (a :/=: b)型の値は存在しない．

PeopleとFood

Peopleは登場人物3人を，Foodはメニュー3品を定義している．どちらも同様なのでPeopleだけピックアップする．

data People = Tonkichi | Chinpei | Kanta

class IsPeople (people :: People)
instance IsPeople Tonkichi
instance IsPeople Chinpei
instance IsPeople Kanta

People型はTonkichi,Chinpei,Kantaを値に持つ型である．しかし，次のIsPeopleクラス定義を見るとTonkichi,Chinpei,Kantaは値ではなくまるで型のように扱われている．これはいったいどうしたことだろう．

実はGHC拡張DataKindsにより，実際にTonkichi,Chinpei,Kantaという型も定義されている．

DataKinds拡張を使うと，data定義時に同名のkindもまた定義したことになる．つまり，今回は，{Tonkichi,Chinpei,Kanta}という値を持つ型Peopleと，{Tonkichi,Chinpei,Kanta}という型を持つ種Peopleを同時に定義している．

TonkichiやChinpeiやKantaはその名前からは値かもしれないし型かもしれない．明示的に値のほうのTonkichiではなく型のほうのTonkichiを示す場合，'Tonkichiと頭に'を付ける．

ちなみに，Tonkichi型やChinpei型，Kanta型を持つ値は無い．値を持つ型は種*を持つ型のみだ．

まとめると，GHC拡張DataKindsによりPeopleのデータ定義から以下のようなものが定義される．

値	型	種
Tonkichi,Chinpei,Kanta	People	*
	Tonkichi	People
	Chinpei	People
	Kanta	People

IsPeople/IsFood

イロイロ推敲してたときの名残リで実際不要．まぁ，あっても何の効果も無い状態なので間違いというわけでもないのだが．

Neq

Neqは(a :/=: b)型の値neqを持つクラスだ．

class (a :: k) `Neq` (b :: k) where
    neq :: a :/=: b
    neq x = case x of {}

a,bは型でkは種．neqにはデフォルト定義がある．Neqは型変数を2つ持つクラスだが，Haskell標準ではこれは許されておらず，GHC拡張MultiParamTypeClassesが必要になる．

たとえば，(Tonkichi `Neq` Tonkichi)はこのクラスのインスタンスにすることはできない．

neq :: Tonkichi :/=: Tonkichi
neq = ?

が実装できないためだ．

各PeopleとFoodについて，以下のように作れるものはNeqのインスタンスにしているが，

instance Tonkichi `Neq` Chinpei
instance Tonkichi `Neq` Kanta
instance Chinpei `Neq` Kanta
instance Chinpei `Neq` Tonkichi
instance Kanta `Neq` Tonkichi
instance Kanta `Neq` Chinpei

インターフェースを簡略化するために定義しているだけで，本当はNeq共々不要とすることもできる．理由は後述．

Eat/NotEat

data Eat :: People -> Food -> * where
    EatRemainFood   :: ( f1 `Neq` f2
                       , f2 `Neq` f3
                       , f3 `Neq` f1
                       ) =>
                       p `NotEat` f1
                    -> p `NotEat` f2
                    -> p `Eat` f3
(snip.)

Eatは「誰かが何かを食べた」ことを意味するdata定義で，これもGADTを使っている．各コンストラクタが，人間がこのパズルを解く際の推論規則に対応する．

EatRemainFoodの型クラス制約では，「f1/f2/f3が全て違う食べものであること」を要請している，そのため同じだったら型が合わない．

実際には型クラス制約を使わず，以下のような形を取ってもいい．

data Eat :: People -> Food -> * where
    EatRemainFood   :: f1 :/=: f2
                    -> f2 :/=: f3
                    -> f3 :/=: f1
                    -> p `NotEat` f1
                    -> p `NotEat` f2
                    -> p `Eat` f3

この場合，Neq型クラスは不要になるが，実際にこのインターフェースを使う箇所で，

-- kantaEatRamen = EatRemainFood kantaHateCurry kantaHateSoba
kantaEatRamen = EatRemainFood (\x -> case x of {}) (\x -> case x of {}) (\x -> case x of {}) kantaHateCurry kantaHateSoba

と，自明なEmptyCaseを書き並べる必要が生じる．

型クラス制約は，型情報と定義されている型クラスのインスタンスから，適切な処理(型情報から自明な何か)を選んでくれる．型クラスを利用したインターフェースにしたほうがよいか，あるいはそのままにしたほうがよいかは実際は状況次第となる．

今回のケースではinstance定義時に組み合わせ爆発が起こる．3人で3種類の食べものだったので，組み合わせは3!=6通りずつだったが，もっと増えるとinstance定義の数がひどいことになる．なので，型クラスにしないのが普通だと思うが，自明なEmptyCase実装を並べなきゃならないのがサンプルコード的に見栄えがよろしくないのではと判断し，あえて型クラスNeqを用意した．

correctAnswer/wrongAnswer

correctAnswerの型を持つ関数は定義できる．wrongAnswerの型を持つ関数は，どこかで型が合わず型検査でエラーになる．もしくは，これまで説明したような値が「存在しない」部分が出てきてしまい，実装できなくなる．

まとめ

このネタ自体は明らかに定理証明寄りのネタなので，マトモに説明するともっとムキムキになってしまう．今回はできるだけそっちっぽさを出さずに説明してみた．なので，こういうのもっと詳しくやりたい人は定理証明やるのがいいんじゃないかな．Try Agda もヨロシク．

ブラウザ上でAgdaを試せるサイトを作ってみた

この記事は Theorem Prover Advent Calendar 2014 の4日目の記事です．

Agdaがコンパイルできないんだがとか，agda-modeってEmacsだけなんでしょ？とか，そういった話をちょくちょく耳にするし，ProofSummit2014で明日の記事担当のamutakeくんがブラウザからCoq使えるやつを発表してたりしたので，Try Agda というサイトを作ってみた．

リポジトリはここ https://github.com/notogawa/agda-interactive-server

バックエンドはHaskellでwai+warp+websocketでAgdaのライブラリからAgdaを直に利用．フロントはjquery+ACE editor．画面レイアウトはもちろんbiim兄貴リスペクトだ．

サーバ強くないし，あんまりデカい証明に使ったりするとガバガバなリロードのせいで激重になったりするかもしれないので，あくまでもお試し用で．

あと，Agdaやる場合は文字の都合上フォントがとても重要なので，DejaVu Sans Monoフォントを推奨する．フォントによっては，Unicode文字の幅とかがACE上での認識とズレるため，表示位置とカーソル位置が離れているといったことが起こる．

ACEに限らず大体のJavaScript製エディタが持つsyntax highlighting機構は，AgdaTopが提供するsyntax highlighting情報を適切に食ってキープできるカンジじゃなさそうで，編集中はhighlightingが消えてしまうがここは割り切っている*1．代わりに適当なタイミングでサーバ側とWS通信し，リロードが入ってhighlightingを復活させるようにしている．

エディタ上でバックスラッシュ叩くとUnicode文字入力モードになる．agda-modeのやつを移植しているので，大体同じようにUnicode文字入力できるはずだ．モジュールはMainのみ決め打ち．

右上のウィンドウは各ゴールに対する入力窓と，Agdaコマンド，エディタコマンドになっている．プルダウンメニューでゴールを選択すると，Contextが勝手に走ってゴールの型や前提条件の型が確認できる．テキストフィールドに入力してRefineすることで穴埋めが進む．Caseは場合分けの生成だけど，まだ関数ケースのみ対応でラムダケースには非対応．なので，ラムダケースに対して使うと悲しみを背負うと思う．SaveとLoadはlocalStorageへエディタのバッファ内容を保存・読み出しをする．

右のウィンドウは情報表示ウィンドウになっており，型エラーの情報や，Context情報などを表示する．

下のウィンドウはWS通信によるサーバ側のAgdaTop挙動を表示している．あまり気にしなくてよい．

目下一番の問題は，biimシステムなのに左下を担当する適切なキャラクターがいないことだ．

*1:と言いつつ誰かいいものあったら教えて

「美しい，だから正しい」より「正しくて，あわよくば美しい」がよい

関数プログラミング実践入門．発売されました．電子版もあります．

今回は本書の副題に関する話題．本書の副題には「正しい」を使っている．実際に価値を提供するのは「正しい」コードなのだが，プログラミング関連文書でよく目にするコードに対する修飾は「美しい」なのだ．これは何故だろう．

といっても，大抵の人は経験などから「美しい*1」コードならば読み易く間違えにくいということを知っている．なので，この点についてそう深く考える必要は無いようにも思われる．「美しい」コードは善である．

しかし，「正しさ」についてあまりにも「美しさ」に頼るようでは危険だ．「美しいから正しい」ことがわかる状態はつまり「ヒトが目を凝らすから正しい」ことがわかる状態ということに他ならない．ヒトは間違える．目も頭も疲れる．

通常，「美しい」コードに保つのは存外コストを要する作業である．お仕事であればザックリと事業戦略の正しさがまず前提にあって，プログラムが必要となれば次に仕様や設計自体の正しさがきて，その後にコードの正しさが続き，やっと価値を提供できる．そして，コードの「美しさ」は「正しさ」よりもさらに後の話になる．「正しさ」を「美しさ」に頼り過ぎていると，プライオリティ的に「美しさ」が後回しになったとき，必然的に技術的負債としての程度が大きくなる．適度に返済しない限り次なる価値の提供に支障が出易くなる．

また，「美しさ」はその人の背景知識や主観にも強く左右される．ある種の難しい知識を修めた人にとっては良いコードに見え，そうでない人にとってはただ無駄に難解なコードにしか見えないということもある．即ち，「正しさ」を「美しさ」に頼り過ぎていると，全く同じコードベースに対してさえ「正しい」コードを書き易いと感じる人と書き難いと感じる人がいる，などということが起こり得る．ともすると「美しい」コードとは自己満足の「美しさ」でしかないという可能性もある．

コードの「正しさ」はコードの「美しさ」に依存しない程よい．

実際にテストファーストなどは最初に何らかの正しさを定め・コードの質から切り離そうとする行為だし，さらにCIなどではヒトが何度も目を凝らす代わりにjenkinsおじさんとかががんばってくれる．

強く型を付けることもまた正しさを定め・コードの質から切り離そうとする行為だし，こちらでは型検査がヒトが何度も目を凝らす代わりにがんばってくれる．そして，型で表現できる性質に対しては，一般にテストよりも網羅的な検証効果を持つ．もちろん，型で表現できないものも中にはあるだろう．

さらに，強く型を付けられることの延長線上には定理証明がある．ここに至っては「型さえ合って実装できてるなら正しいんだから書かれてるコードは読まない」と言われるほどコードの質に興味を持たれないケースまである．これはこれで過激派過ぎて駄目な面もあるのだが，コードの「正しさ」の保証が強力になるに伴い，「美しさ」含めたコードの質の重要度が相応に低下したこと示す顕著な発言でもある．

他にも，静的・動的解析ツールによるバグの検知はそれだけで商売にもなっている*2．HaskellがらみでもLiquidHaskellなどは定めた性質の証明をある程度自動で行ってくれる．

重要なのは「正しさ」のために取れる手段の多様性だ．

「美しさ」を保つのにコストがかかるように「正しさ」を保証するにもコストがかかるし，各手段によって保証できる「正しさ」も度合いが少しずつ異なる．トレードオフは少なからず存在する．

テストは言語に依らず実施可能だが，あまり網羅的な保証することができないし，効率的な自動実施の仕組みも必要となる．強力な型システム上に限られるが，型で表現できる部分はテストよりも網羅的な効果を持ち，検査の仕組みは大抵言語処理系が持っている．定理証明が可能ならば申し分なく強力な保証となるが，証明のための作業コストは馬鹿にならない．自動証明や解析は，可能な範囲や対象言語が限定されるが作業コストはかからない*3．

選択した言語・環境に許された手段の中で，直面している問題に対し，どの程度の「正しさ」をどの程度のコストを払って保証したいかによって選択すべき手段が変わる．言語や環境の選択時点で，取れる手段が多様であればトレードオフに合った適切なバランスのものを選択し易い．逆に手段が限られるのは恐しいことだ．本来もっと網羅的な検証を行う価値が認められるクリティカルな項目に対してさえも，テストしか手段が無ければテストにより検証する他ない．

改めて，副題に「美しい」でなく「正しい」を使った．その理由は，ひとつはコードの価値がどちらにあるかと言えば「正しい」であるため．もうひとつは，関数プログラミング及びそれを主目的とした関数型言語達は，その性質の良さから，「美しさ」に依存しない「正しさ」の保証に比較的強みを持たせ易いため．

*1:「整然とした」などのニュアンス含め

*2:Coverity PreventやKlocworkなどが有名なのかな？

*3:金銭コストはかかるかもしれないが

関数プログラミング実践入門という本を書きました

是非手に取ってみて下さい．よろしくおねがいします．

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

AgdaとかHaskell Golfの本ではない．いいね？

どのような本？

これまで何らかの命令型言語に触れてきた人が「なにかと耳にするし，そろそろ関数プログラミングでも」と思いたったとき，その基本的な部分を押さえるための本です．関数型言語としてはHaskellをとりあげ，またHaskellを使っていくための説明を進めていきます．関数プログラミングからプログラミングに入る人はプログラミングに対する先入観が無いのでともかくとして，既に命令型言語の経験がある人の場合，関数プログラミングの考え方や関数型言語そのものにはなかなか慣れないものです．

関数プログラミングや関数型言語周辺はどうも壁にぶつかり易く，その上何枚も何枚もあるようです．ひとりでの学習は辛いことがあるでしょう*1．この種の学習で一番高効率で手っ取り早いのは「知ってる人にたずねる」ことだと思います．しかし，どんなジャンルでもそうなのですが，最低限ある程度の素養は身に付けないと，誰が「知ってそうな人」なのかも判断できません*2．また，知ってそうな人から効率良く知識や考え方を受け取るためのコミュニケーションにも，共通基盤としての素養があるなしで大分状況が変わってきます．それっぽい勉強会に顔を出しても，そこでの会話内容が何を言っているのかあまりにも理解できないとそれだけでおうちにかえりたくなりますね．

関数プログラミングに関する書籍，特にHaskellに関する入門書は，良書が既に出版されています．そのような中で本書は，上記のような関数プログラミングやHaskellに関する基本の習得に加え，他言語との比較とか設計法・考え方，実用するためのパッケージ管理といった点を重視する立ち位置で執筆しています．特定の問題設定に対しある言語でのアプローチとHaskellでのアプローチがどうなっているかを比較することで特徴*3を明確にしたり，特徴を別の言語に取り入れてみるとどうなるか見てみたり，関数プログラミングっぽい思考・設計方法を使って数独を解いたり，論理パズルを安全に解かせるためのインターフェースデザインを示してみたりします．

Haskellのサンプルコードは現時点最新のHaskell Platform 2014.2.0.0を想定して書かれていますが，基礎的な部分のみなので先々のバージョンアップで動かなくなるようなことも無いと思います．

一方，一部の関数プログラマが好むような高度な数学とか難しい運算*4とかは出てきません．が，そういう一定以上の知識を既に所有している人にとっても最後の2章分については得るところもあると思います．

経緯と執筆中のアレコレ

2013年の7月も終わりの頃，本書の企画と執筆依頼が来て．思わず二度見する．最初執筆依頼と目にしたときは，もしやHaskell Golfについて？と思ったが，関数プログラミングについての入門とのこと

顔合わせと詳しい話を聞くため編集さんとのミーティング．実はこの時点では受けるか半々くらいの気持ちだった．きっかけとしては，どうも孤独のHaskell - ぼくのぬまち 出張版をshinhさんが取り上げたのを目にして声を掛けてくれたとのこと．この経路でなおGolfネタじゃないんだなぁとしみじみした．何を重視するどんな本にするかといった内容をおおまかに詰め，2013/8月から大体1年間になる執筆期間に突入

最初に章・節レベル構成を決めて各章にどのくらい期間を取るかマイルストーンを置く，結果として執筆は概ねオンスケジュールだったと思う

執筆中に，「プログラマのためのコードパズル ~JavaScriptで挑むコードゴルフとアルゴリズム」という書籍が技術評論社から出てて，Golfネタやってるんじゃんと脳内観客が全ツッコミ

新しい Haskell Platform がなかなかリリースされずにヤキモキする．結局1年以上リリースされず，2014/8月にやっと Haskell Platform 2014.2.0.0 が出たのでコード修正と動作確認．

執筆はbitbucketにリポジトリ作ってmarkdownにて行う．styファイルなどがあるならTeXがいいなと思ってたけど，このシリーズの組版や図の清書は出版社側の仕事らしくstyファイルなども特に無かった模様．これのせいというわけでもないけど，感覚がつかめず当初の予定より執筆分量をだいぶ間違えた．

2014/10月前半あたりで著者校正．DPT-S1大活躍．A4対応な画面の大きさと，宙には浮かないものの軽量な本体重量，電子ペーパーならではの電池持ち，移動中の赤入れがメッチャ捗る

感想

本当に小学生並な言い回しになっちゃうけど，やっぱり本が出るまでって大変なんだなぁというのが第一．編集さんにもだいぶ負担かけてしまったと思う*5．

とにかく書籍が出るってこと自体が相当な社会的・文化的基盤に支えられてる行為で，特に専門書は関連書籍の多さが分野・コミュニティの強さや世間的な関心に直結してる．なんだかんだ言って数の力はシンプルかつ強大で，たとえば開発プロジェクトでどの言語を選択するかといった点にもある程度は影響する．数字が大きいことはそれだけでピックアップされる対象になる．そういう面があるから，ある分野が好きなだけではその人にとって幸せな世界はあまり作れない．やっぱりシーンを盛り上げるような各種ムーブやある種の政治力みたいなものも必要になってくる．将を欲っすればまず馬じゃないけど書を欲っすればそれによりウマーと思う人間を増やさないといけない．裾野が広ければこそ頂点もまた安定して高くなっていける余地が生まれる．

この点，気のせいかもしれないけれど，関数プログラミング界隈ってまだ他と比べて裾野が狭いまま頂点のほうは妙に高いとこにある気がする．コミュニティとしては細く削った鋭いエンピツのような歪な構成をしてるように見える．特にHaskell界隈は原理主義者っぽい人も多いし，わかんないこと調べるとすぐに論文に案内されるハーコーっぷりもキツいよね．ニュービーに優しいコンテンツじゃないと良い循環にならないし，実用のためのプラクティスを積んで共有して広めていかないと働き口も思うように増えない．

今更何を当然なことをと思われるかもしれないけれど，それでも感想としてこういうことを記しておきたいと思う．

*1:Agdaつらいんですけど．

*2:最近だとtwitterとかブログで疑問投げておけば解説に自信ニキが教えてくれたりもしますが

*3:優劣という意味ではなく

*4:そういうの求めてる人は同時期発売の「関数プログラミング 珠玉のアルゴリズムデザイン」が歯応えあっていいんじゃないかな？

*5:ありがとうございました

Haskell定理証明士がEmptyCase拡張によって受ける恩恵と効能

EmptyCaseが入ってきた．absurd pattern matchingがHaskellで使えるのでHaskell証明士には朗報だ．

具体的にEmptyCaseの有無で世界がどう変わるかを把握してる範囲で書く．

まず，矛盾(bottom)の扱いについて．矛盾は「値を構成できない型」になればよいので，通常次のいずれかになる．

data Bottom

data Bottom = Bottom Bottom

直観主義における「矛盾からは何でも導ける(bottom elimination)」は，型としては，

bottomElimination :: Bottom -> whatever

となるが，今まではこれの実装は，

bottomElimination bot = bottomElimination bot

bottomElimination (Bottom bot) = bottomElimination bot

などにせざるをえなかった．結局のところ値を構成できない型であることを上手く使えておらず，無限ループのbottomに入り込むことによって任意の命題を引き出していたが，これがみんなの健康によくないのは明らかである．CoqやAgdaなどの定理証明系では停止性チェッカがあるため，このような実装は通常与えられない．

そして，これは「Bottomに限らず何からでもよいから何でも引き出せる」という命題を作ってよいのかという話でもある，たとえば，

getWhatYouWantFrom :: a -> whatever
getWhatYouWantFrom anything = getWhatYouWantFrom anything

のように，同様にして任意の命題から任意の命題を引き出せてしまう，そのため，型を証明に使うことを重視するのであればどうみてもunsafeな実装(証明)方法になっている．

計算機においてbottomは「値を持ち得ないもの」や「計算が停止しないもの」に相当するが，証明において後者は本当に秘密道具たっぷりつまった四次元ポケット的ジョーカーなので，定理証明系は停止しない計算が慎重に排除された系として設計されている．

EmptyCaseが入ると，最早このようなunsafeな実装を使う必要は無い(といっても，Haskellである以上書けてはしまうところは変わるわけでもないのだが)

{-# LANGUAGE EmptyCase #-}
data Bottom

bottomElimination :: Bottom -> whatever
bottomElimination bot = case bot of {}

次に，bottomを使う証明オブジェクトの作成，たとえばシンプルなところで命題の否定について．命題の否定Notは次のようになる．

type Not prop = prop -> Bottom

簡単に言うなら「propならば矛盾する」ので「propではない」である．

具体的な話として，TrueとFalseが等しくないという命題は正しいので証明が与えられるはずだ．

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
data Bottom

type Not prop = prop -> Bottom

data a :==: b where -- propositional equality のようなもの
    Refl :: a :==: a

type a :/=: b = Not (a :==: b)

trueNotEqualFalse :: True :/=: False
trueNotEqualFalse = 証明？

しかし，この証明(実装)を上手く与える方法は実はそんなに無い．EmptyCaseのドキュメントではerror関数を与えていたが，これが型の上で証明に用いるに相応しいものでないことは明らかだし，そのように書かれてもいる．

やるとすれば次のようにTypeFamiliesを使う方法があった．

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
data Bottom

type Not prop = prop -> Bottom

data PropEq a b where -- (:==:) をメインに使っていきたいので別に定義
    Refl :: PropEq a a

type family (a :: k) :==: (b :: k)
type instance True  :==: True  = PropEq True True
type instance True  :==: False = Bottom
type instance False :==: True  = Bottom
type instance False :==: False = PropEq False False

type a :/=: b = Not (a :==: b)

trueNotEqualFalse :: True :/=: False
trueNotEqualFalse = id

この方法では，PropEq True FalseがBottomと同じく値を持たないことが(Haskellにも)わかり，Not (PropEq True False)についてもその実体はBottom -> Bottomという型になるため，TrueとFalseが等しくないことをid関数で証明できる．のだが，執拗にtype instanceを作り込んでダメなケースが矛盾なんだよとHaskellに教えてあげなければならない．しかも，この(:==:)は他のものにも使えるはずだが，それらについてもイチイチ何が矛盾かと教えていたらキリが無い．

正直，他に良い方法があるならとても興味があるので教えて頂きたい．

これが，EmptyCase後では単に次のようにすればよい．

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE EmptyCase #-}
data Bottom

type Not prop = prop -> Bottom

data a :==: b where
    Refl :: a :==: a

type a :/=: b = Not (a :==: b)

trueNotEqualFalse :: True :/=: False
trueNotEqualFalse eq = case eq of {}

これまでは，その型には値が無いことはわかっても，それがBottomと同じ型になっているという事実を上手く使えなかったのだが，EmptyCaseによりそれを適切な形で利用できるようになっていることがわかる．

copatterns概要

ghc-7.8でビルドできるAgdaマダカナーとか思いつつ，Agda-2.3.4のリリースノート(まだリリースされてないけど)を眺めてたら，実験的機能としてcopatternsってやつが入ると書かれている．余(co-)がついてるのでたぶん健康によくないやつなんだろうなと思いつつ読むと，なにやらこんなカンジのようだ．

タプルをレコードで定義すると，次のようになる．

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

タプルのフィールドとしては1番目の要素であるfstと2番目の要素であるsndを持っていて，recordをopenすればこれらは普通に関数として使える．

通常，タプルを与えるような関数は最終的にタプルをコンストラクトすることになる．

pair : {A B : Set} → A -> B -> A × B
pair a b = a , b

swap : {A B : Set} → A × B -> B × A
swap p = snd p , fst p

swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
swap3 t = snd (snd t) , (fst (snd t) , fst t)

で，リリースノートによると，copatternsによってこれらが以下のように書けるようになるのだという．ふぁー

pair : {A B : Set} → A → B → A × B
fst (pair a b) = a
snd (pair a b) = b

swap : {A B : Set} → A × B → B × A
fst (swap p) = snd p
snd (swap p) = fst p

swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
fst (swap3 t)       = snd (snd t)
fst (snd (swap3 t)) = fst (snd t)
snd (snd (swap3 t)) = fst t

つまり，タプルというデータをコンストラクトするのではなく，タプルを作る関数に対して，fstとsndを適用したときの外延的な性質だけで定義しようという試みのようだ．実際にpairやswapやswap3が「タプルの構造を作る」かはわからないけど，fstとsndに対してタプルと同じ挙動をする何かになるので「型としてはタプル」でいいのだ．と，ここまでをウカツに圏論に触れてしまった人が見ると「圏論的な定義だ！カッコイイ！」とか言うんだけど，わたしはあまりよくしらないのでホウホウおもしろいとだけ思っておく．

タプルみたいに簡単なやつならともかくとして，たとえば群とか環とかモナドとかイロイロな代数構造もみんなレコードになっているので，「何かがその代数構造を持つ」ことを示すときに，結合則はこうでー交換則はこうでーみたいな証明の書きかたが少々キレイにカッコイイ感じにはなるかもしれない．

が，これがだから何なんだというか普通にcopatternsを使わずに定義するのと見た目以外の一体どこに差があるんだという話なんだけど，そもそもcopatternsは余帰納的データ型を上手く扱うために導入されたものらしい．

通常，Agdaで余帰納的データ型を作ると，たとえばストリームでは次のように余帰納になる部分の型を∞でラップした型を持つコンストラクタを作る．この部分はブラックボックスになっており，♯で閉じたり♭で空けたりしながら扱うことになる．♯は「空けないとわからない状態の値」を作るためのもので，♭は「空けたときに実際入っていた値」を取り出すものだ．

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A  

しかし，この表現では次のような一見自明に見える命題が証明できない．

repeat : ∀ {A} → A → Stream A
repeat x = x ∷ ♯ repeat x

lem : repeat 0 ≡ 0 ∷ ♯ repeat 0

「任意のストリームsに対し，ある値eとストリームs'が存在し，ストリームs = 先頭がeで残りがs'のストリーム 」であるにもかかわらず，この種の命題はヒトの直観と異なりどれも証明できない状態になっている．

これは，データはコンストラクトしなければ(使命感)ということを前提とした場合，等価性の証明もコンストラクトベースになることに起因する．いつか必ず末尾のある帰納的データ型に対してはそれで帰納法(再帰関数)を書いて証明すれば(再帰が停止することがわかるので)全く問題無い．しかし，終わりが無いかもしれない余帰納的データ型に対しては，字面上自明に等価な場合を除き，無限に等価性を追い続ける必要が出てきて決定不能になってしまう．

一方，copatternsを使ったストリームの定義では，同様の命題が，

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream

repeat : {A : Set} (a : A) -> Stream A
head (repeat a) = a
tail (repeat a) = repeat a

lem : repeat 0 ≡ record { head = 0, tail = repeat 0 }

のようになり，ストリームのレコードが持つフィールドheadとtailに関して，観測結果がどちらも同じ式になるため，これらは共に自明にreflにすることができ，期待通りの証明を与えることができる．らしい(まだリリースされてないので試してもいない)