ブラウザ上で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.
選択した言語・環境に許された手段の中で,直面している問題に対し,どの程度の「正しさ」をどの程度のコストを払って保証したいかによって選択すべき手段が変わる.言語や環境の選択時点で,取れる手段が多様であればトレードオフに合った適切なバランスのものを選択し易い.逆に手段が限られるのは恐しいことだ.本来もっと網羅的な検証を行う価値が認められるクリティカルな項目に対してさえも,テストしか手段が無ければテストにより検証する他ない.
改めて,副題に「美しい」でなく「正しい」を使った.その理由は,ひとつはコードの価値がどちらにあるかと言えば「正しい」であるため.もうひとつは,関数プログラミング及びそれを主目的とした関数型言語達は,その性質の良さから,「美しさ」に依存しない「正しさ」の保証に比較的強みを持たせ易いため.
関数プログラミング実践入門という本を書きました
是非手に取ってみて下さい.よろしくおねがいします.
関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (WEB+DB PRESS plus)
- 作者: 大川徳之
- 出版社/メーカー: 技術評論社
- 発売日: 2014/11/14
- メディア: 単行本(ソフトカバー)
- この商品を含むブログ (1件) を見る
どのような本?
これまで何らかの命令型言語に触れてきた人が「なにかと耳にするし,そろそろ関数プログラミングでも」と思いたったとき,その基本的な部分を押さえるための本です.関数型言語としては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界隈は原理主義者っぽい人も多いし,わかんないこと調べるとすぐに論文に案内されるハーコーっぷりもキツいよね.ニュービーに優しいコンテンツじゃないと良い循環にならないし,実用のためのプラクティスを積んで共有して広めていかないと働き口も思うように増えない.
今更何を当然なことをと思われるかもしれないけれど,それでも感想としてこういうことを記しておきたいと思う.
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にすることができ,期待通りの証明を与えることができる.らしい(まだリリースされてないので試してもいない)
ghc-mod-4 でfaceを反映させる
ghc-mod-4以降ではghc-modiを使うためにflymakeへの依存を切っており,flymake的な挙動は自前で実現している.
そのため,今まで反映されていたflymake用のface設定が反映されなくなるので,バージョンアップ後急にさびしい絵面になったりする.
もし,
(set-face-background 'flymake-errline "red4") (set-face-foreground 'flymake-errline "black") (set-face-background 'flymake-warnline "yellow") (set-face-foreground 'flymake-warnline "black")
のようにflymakeのfaceを設定していたのなら,これを反映させるには,ghc-modが独自に持っているfaceに対しても同様に設定しなければならない.
;; ghc-mod (autoload 'ghc-init "ghc" nil t) (add-hook 'haskell-mode-hook (lambda () (ghc-init) (set-face-background 'ghc-face-error "red4") (set-face-foreground 'ghc-face-error "black") (set-face-background 'ghc-face-warn "yellow") (set-face-foreground 'ghc-face-warn "black")))
みんなきおつけろ!
IOアクションひとつひとつを利用許諾し・テスト可能にする
IOのテストってたいへんだ.これをどうにかするために,先人たちは色々考え,
- 利用対象の特定IOアクションを慎重に取捨選択し,MonadHogeIOのような型クラスによりインターフェースを与えてからそのインターフェース上のアクションとして実装する.実行時は目的のインスタンスの上で走らせるし,テスト時はMock用インスタンスの上で走らせる
- 同様に特定IOアクションを慎重に取捨選択し,FreeモナドやOperationalモナドによりインターフェースを与えて以下略.目的のランナーで走らせたり,テスト用のランナーで走らせたりする
といった手段を取る.
で,普通テスト用のものはピュアになるように実装し,テストしやすくする.具体的には,型クラスとモナドと Free モナド - あどけない話や,Freeモナドを超えた!?operationalモナドを使ってみよう - モナドとわたしとコモナドがわかりやすいかな.
でも,どちらの方法を取るにせよ,IOアクションが適切に取捨選択された状態になければならない.IOアクションaとIOアクションbだけ使うIOアクションx (x = a >> b)と,IOアクションbとIOアクションcだけ使うIOアクションy (y = b >> c)があるとき,a,b,cそれぞれに相当するインターフェースを持った型クラスやらデータ型のコンストラクタやらを用意することになる.もくは,aとbだけ,bとcだけにそれぞれ相当するやつだけ持ったものを用意するだろうか?いずれにせよ,特定のものに限定した環境を作ってその上で戦うことになる.というのがこのあたりの話
すべての IO を呼ぶ関数を後から注入するようにすればいいのかなあ
— matsumoto (@daimatz) 2014, 2月 18
IOのテストのためにFree使うことはどの程度合理的かなあ
— ruicc (@ruicc) 2014, 2月 18
IOのテストって考えてるうちはどの方法にも合理性は無いのでは?やりたいIOは本当はどんなのか制限できて初めて輝くというか
— Noriyuki OHKAWA (@notogawa) 2014, 2月 18
IO制限するためにFree使いましょう
— ruicc (@ruicc) 2014, 2月 18
IO の種類を制限するというの、テストの文脈でどう嬉しいのかあまりわかっていない。 QuickCheck できるのが嬉しいのはわかるが。
— matsumoto (@daimatz) 2014, 2月 18
MonadHogeIO型クラスを作ってHogeとHogeMockをインスタンスにして本番はHogeテストはHogeMockが推論されるようにするとアクションがさしかわる,Freeモナド作るときもアクションの種類は限定する,どっちでも結局IOの種類は制限されてなければならない
— Noriyuki OHKAWA (@notogawa) 2014, 2月 18
流れは大体わかっているつもりなのだけど手を動かす元気が無い
— matsumoto (@daimatz) 2014, 2月 18
で,この記事の本題.上のツイートで「制限されてなければ(義務感)」みたいに自分でも言っておいて,果たして今でも本当にそんな状態なのかとちょろっと考えてみた結果を簡単にライブラリ(まだhackageに上げてない)にしてみた.
このライブラリは,ザックリ言うとIOアクションの利用制限及びモック差し替えを自由に行うための,インターフェース・型クラス制約生成系及び,それを利用した例としてのPreludeの置き換えモジュールとなっている.
TemplateHaskellにより任意のIOアクションからextensible-effectsのEffアクションを生成し,あるIOアクションに対応して生成された特定の型クラス制約がコンテキストに無い場所ではそのIOアクションを元に生成されたEffアクションは使えないという制約を付けることができる.加えて,Effアクションがコンテキストに持つ型クラス制約に対するインターフェースだけをモック実装すればそのEffアクションはテスト可能になる.というものだ.
自分で上手く言えてないのわかってるのでたぶん何言ってるかわからないと思う.さっさとサンプル示そう.
まず,IOアクションからEffアクションを生成するTemplateHaskellについてだが,たとえば,Control.Genjitsu.THのgenjitsuを使い,
import qualified Prelude as P $(genjitsu 'P.putStrLn)
のようにすると,これにより次のようなコードが生成される.
class AllowPutStrLn m where allowPutStrLn :: String -> m a instance AllowPutStrLn IO where allowPutStrLn = putStrLn putStrLn :: ( Typeable1 m , AllowPutStrLn m , Member (Lift m) r , SetMember Lift (Lift m) r) => String -> Eff r () putStrLn x = lift (allowPutStrLn x)
Prelude.Genjitsuモジュールは,これをPreludeのIOアクション全てに行い,元の名前の関数を新たに生成された同じ名前の関数で置き換えているだけだ.
実際にPrelude.Genjitsuを使うと次のようなコードになる.
sample1 :: ( Typeable1 m , AllowReadLn m -- readLnが使える , AllowPutStrLn m -- putStrLnが使える , Member (Lift m) r , SetMember Lift (Lift m) r ) => Eff r () sample1 = do n <- readLn let s = n + 1 :: Int -- putStr "is denied" putStrLn (show s)
sample1は型の部分に目を潰ると,中身はただのIOモナドのように見える.ただし,このsample1のコンテキストでは,readLnとputStrLnしか許されていない.そのため,readLnとputStrLnは使えるが,putStrを使おうとするとコンパイルエラーになる.
また,別のケースも見てみよう.
sample2 :: ( Typeable1 m , AllowPutStr m -- putStrが使える , AllowPutStrLn m -- putStrLnが使える , Member (Lift m) r , SetMember Lift (Lift m) r ) => Eff r () sample2 = do putStr "Start..." putStrLn "Done"
こちらのsample2では,putStrが使えるようにコンテキスト指定されているのでputStrが使える.
さて,これらを実際にIOアクションに還元してあげるのは簡単だ.extensible-effectsのLiftを使っているのでrunLiftしてあげればいい.
sample1IO :: IO () sample1IO = runLift sample1 sample2IO :: IO () sample2IO = runLift sample2
また,sample1/sample2に対してテストを書く場合,これらの各コンテキストにある型クラス制約で許可されたものだけインスタンス実装すればいい.たとえば,sample1をテストするのにStateモナドを使ってみると,
-- 各自適切なGHC拡張は補完してネ newtype Mock1 a = Mock1 { runMock1 :: State String a } deriving ( Functor, Applicative , Monad, MonadState String, Typeable) -- sample1はAllowReadLnをコンテキストに持つのでMock実装が要求されている instance AllowReadLn Mock1 where allowReadLn = fmap read get -- sample1はAllowPutStrLnをコンテキストに持つのでMock実装する instance AllowPutStrLn Mock1 where allowPutStrLn = put test1 = ((),"3") == runState (runMock1 $ runLift sample1) "2"
sample2のほうも同様にしてpureなテストを書くことができる.sample2についてはsample1と異なりテスト対象として入力のアクションを含まないのでWriterモナドでモック実装してあげれば十分だろう.ここまでのサンプルコード
genjitsuがMonadHogeIOインターフェースやFree/Operationalモナド方式に対して持つ利点は,
- 必要なクラスやらの生成がTemplateHaskellでだいぶラク
- runLiftでIOアクションに戻したものを再度genjitsuしておくようなことも簡単
- あらかじめ利用したいアクションを取捨選択して制限しておく必要が無い
- その場その場で本当に必要ならコンテキストとして与えればよい
- アクション単位の利用許可を型で表すことができる
- ウカツにいろんな種類のIOアクションを使ってしまうようなことを防げる
- 何を実装すれば走らせることができるかが型レベルで明確になる
- 許可されているものに対してのみ実装を与えれば走る
- モック書いたりするときに着目しているテスト対象に対して余計なインターフェースを気にしなくてよい
とか.そのへん.
感覚的にだいぶ楽だと思うんだけどどうだろうか?正直なところ言うとコンセプトにイマイチ自信が無いのでhackageには上げてない.