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

ロジックパズルの解説

この記事は 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 もヨロシク．