stackで行く地獄巡りの旅

Haskell

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を使う

Haskell

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

Haskell

年末年始なので何か作ろうかなと思い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

この記事は 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を試せるサイトを作ってみた

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)

関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (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:ありがとうございました