スタートHaskell第0回に行ってきた+最後にやってたあの難解なLTの解説
スタートHaskell 第0回に行ってきました｡
「初心者向けで環境構築から始まりハローワールド程度しかやらない勉強会､Haskellに多少触ったことのある人間が行く意味あるのだろうか……」と思いつつ行ってみたものの､予想以上に向こうの想定している「初心者」がハイレベルだったため行く意味大あり､TAPL
実際面白かったので､次回以降もぜひ参加したいですね｡
LTの最後にやった､型から項を作る話についての解説
【注意】私はあの発表をした人とは関係ないです｡しかも実際素人なので､間違ったことを書いている可能性があります!!【ツッコミ希望】
一部の人々のHaskellをストップしそうになったこの発表､実はそれほど難しいことはやっていない―― 正確に言うと､「何のためにやるか」「どうやってやるか」は難しいけど､「何をしたいのか」はシンプルだ｡ただ､いろいろと前提となる知識が要求されるので多くの人が置いてけぼりになってしまったようだが……｡
この発表は､一体全体なにをしたかったのだろう?
一言で言うと､タイトル通り「型から項を得る」ことなのだが､それは一体何を意味するのか､まずはHaskellの基礎から説明してみよう｡
項というのは､Haskellの式みたいなものだ｡たとえば､
1 [1, 2, 3] "ABC" \x -> x + 1
のような｡
これらはそれぞれ､型を持っている｡たとえば､1は数字型だ｡[1,2,3]は数字のリスト型だ｡"ABC"は文字のリスト型､\x -> x + 1は数字をひとつ受け取って数字を返す関数の型だ｡
型というのが正確にはどういうものなのかというのは､この解説の範疇を越えている(筆者の能力も)｡でも､この例でなんとなくわかるんじゃないかな｡
さて､型から項を得る前に､項から型を得る話をしよう｡これはつまり､「Haskellの式を入力したときに､その式がどういう型を持っているのかを得る」ということだ｡これはHaskell処理系がいつもやっていることだ*1｡実行してみるには､ghciで:tコマンドを使うのがてっとりばやい｡
Prelude> :t 1 ;; 式「1」の型を表示せよ 1 :: Num a => a ;; 「数字」型です Prelude> :t [1, 2, 3] ;; これは? [1, 2, 3] :: Num t => [t] ;; 「数字のリスト」型です Prelude> :t "ABC" ;; 文字列はどんな型? "ABC" :: [Char] ;; 「文字のリスト」型です Prelude> :t \x -> x + 1 ;; この関数は? \x -> x + 1 :: Num a => a -> a ;; 「数字をひとつとって数字を返す関数」型です
数字型がなぜNum a => aなんてへんてこな表現をになっているのか気になる人もいるだろうけど､今回の解説にはそれほど関係ないので詳細は飛ばす｡まあ､Haskellを学んでいれば近いうちにわかるはずだ｡
「項から型を得る」と､一体何が嬉しいのだろう?
実のところ､それはHaskellがちゃんと動くための基本となる操作だ｡
「数字をひとつ取る関数」に「数字のリスト」を渡すようなソースコードを書くと､コンパイルエラーになる｡
let f = \x -> x + 1 in f [1,2,3] ;; おおっと､こんなことはできないぞ
変なことをすると､コンパイルする時点で間違いを検出してくれる｡これがHaskellのいいところだ｡
そして､そのためには､fが「数字をひとつ取る関数」型であるということと､[1, 2, 3]が「数字のリスト」型であることがわからないといけない｡そうじゃないと間違っているかどうかわからないからね｡
さて､ようやく本題の「型から項を得る」件についてだ｡これはさっきとは逆のことをやる｡つまり､
Prelude> :型から項 Num a => a 1 Prelude> :型から項 [Char] "ABC"
みたいに｡
もちろん､「数字」型なのは1だけじゃないし「文字列のリスト」型なのは"ABC"だけじゃない｡実際には無数の式があてはまるだろう｡そこで､与えられた型を持つ式を､何でもいいからひとつ返せばいいということにしよう｡「Num a => a」に対して､1を返してもいいし100+500を返してもいい｡
さて､このような事をするには､いったいどうすればいいのだろうか…… というのが､この発表の内容だ｡
実際どうやるかについては､なかなか難しい話なので詳しくは触れない(スタートしたばかりの諸君には実際荷が重いよ!)｡ざっくり言うと､こんなかんじだ｡
- Haskellはあまりにも複雑なので､もうちょっと単純な言語で考えてみる｡ここで出てくるのが「単純型付きラムダ計算」という代物｡これは実際単純だ!!
- 「単純型付きラムダ計算」には､項から型を得るルールが含まれている｡これを元に､型から項を得るルールを構築する(単純に逆にすればいいんだろうって?残念ながらもうちょっと複雑なことをする必要がある)
- ルールができたのでバンザイと思ったら､このままだと無限ループに突入してしまうことがある｡これを回避するために処理の仕組みにもうひとひねり加える｡
- いいかんじの処理ができたので､Haskellで実装してみたらこんなにシンプルに書けた!!Haskellべんり!!!!!(おわり)
それにしても､型から項を得ると一体何が嬉しいんだろう?
この質問に分かりやすく答えるのは難しい｡でも､「バグのないすごく高品質なソフトウェアを作るために､実際便利」ということは確かなんだ｡発表の最後に紹介されていた「Curry-Howard対応」や「定理証明」「形式手法」などがキーワードなので､興味があったら調べてみるといいんじゃないかな(おわり)
