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

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


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

といっても，大抵の人は経験などから「美しい*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:ありがとうございました

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だけにそれぞれ相当するやつだけ持ったものを用意するだろうか？いずれにせよ，特定のものに限定した環境を作ってその上で戦うことになる．というのがこのあたりの話

で，この記事の本題．上のツイートで「制限されてなければ（義務感）」みたいに自分でも言っておいて，果たして今でも本当にそんな状態なのかとちょろっと考えてみた結果を簡単にライブラリ(まだhackageに上げてない)にしてみた．

notogawa/genjitsu · GitHub

このライブラリは，ザックリ言うと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には上げてない．

CPS変換もいいけど融合変換もね

継続渡しなHaskellライフ - モナドとわたしとコモナド の流れで．

要約すると，元々

fb :: Int -> Either Int String
fb n = case n `gcd` 15 of
         15 -> Right "FizzBuzz"
         5  -> Right "Buzz"
         3  -> Right "Fizz"
         _  -> Left n

fizzbuzz1 :: Int -> String
fizzbuzz1 n = either show id (fb n)

みたいなコードだったのを，

fbCPS :: (Int -> t) -> (String -> t) -> Int -> t
fbCPS left right n = case n `gcd` 15 of
                       15 -> right "FizzBuzz"
                       5  -> right "Buzz"
                       3  -> right "Fizz"
                       _  -> left n

fizzbuzz2 :: Int -> String
fizzbuzz2 n = fbCPS show id n

みたいにCPS変換しておいて使えば，

条件分岐の結果を一旦代数的データに押し込み、それに対してさらに条件分岐を行おうとしているのだ……

と問題視していたデータの構成及びパターンマッチが

計算の結果を代数的データ型を介さずに受け渡しできる

ことになって無くなってくれるのでイイねぇという話．

たしかに高速化にCPS変換が効果的なのは正しい．けど，fizzbuzz1とfizzbuzz2を見比べたときにちょっとアレ？って思うところ無いだろうか．というのは，CPS変換前ではfbという部品を作りeitherという別の部品と組み合わせて全体の処理fizzbuzz1を構成していたのが，CPS変換後のものを使ったfizzbuzz2では妙に強く結合してしまったナァという印象を受ける．まぁ，元のfbと同じものはfbCPS Left Rightだからそれでいいっちゃいい．でも，Haskellは関数適用と型システムによる強くて硬いcomposabilityに裏打ちされたmodularityがウリのひとつではなかったか．それともイザ速いプログラムを書くにあたっては仕方のないことなのだろうか？

いや我々にごはんを食べさせてくれているHaskellさんはさすがにそんなことはないはずなのだ．要は代数的データ型に対し，それを消費するeitherやfoldrみたいなものと，代数的データ型の生成が自動的に打ち消されてくれればいい．ぱよえーん

たとえば次のような関数buildEを考えよう．要RankNTypes

buildE :: (forall x . (a -> x) -> (b -> x) -> x) -> Either a b
buildE g = g Left Right

buildEは，Leftに対応する変換であるa to xの関数と，Rightに対応する変換であるb to xの関数を受けてxになる関数gを受け，Either a bとなる関数である．まぁ，型をそのまま読むとそう書いてある．このbuildEを使うと，とりあえず適切なgさえ与えてあげれば，fbのような関数はなんとなく書けそうな気分になる．

さて，Either a bを生成するこの関数buildEと，Either a bを消費する関数eitherを組み合わせると，

either l r (buildE g) = g l r

という等価な式がなりたってeitherとbuildEが消える．という最適化ができる．この等式の右辺を構成する要素g,l,rの型にはEither a bは一切出現しないので右辺の処理ではEither a bの値は作られない．この最適化規則はghcではRULESプラグマとして次のようにコンパイラに教えてあげることができる．

{-# RULES "either/buildE" forall l r (g :: forall x . (a -> x) -> (b -> x) -> x) . either l r (buildE g) = g l r #-}

こうしておくと，buildEで書かれたEither a bを生じる関数は，eitherされると最適化によりEither a bの生成・パターンマッチなどが勝手に消えたコードになってくれるはずだ．

あとは実際にbuildEでfbを書き直す．

fbBuildE :: Int -> Either Int String
fbBuildE n = buildE g where
    g l r = case n `gcd` 15 of
              15 -> r "FizzBuzz"
              5  -> r "Buzz"
              3  -> r "Fizz"
              _  -> l n

この関数fbBuildEはfbと同じ型と同じ結果を持ち，CPS変換済みのコードをbuildEを介して内部に隠し持ったような形になっている．これをfizzbuzz1と同様にeitherと組み合わせ，

fizzbuzz3 :: Int -> String
fizzbuzz3 n = either show id (fbBuildE n)

とすると，fizzbuzz1と部品化の度合いは同じままで済んでおりコードの見た目は変わらない．それでいて，先程の変換規則に合致するので中間的なEither Int Stringは作らないよう最適化される．

Eitherみたいに構造が小さい代数的データ型に対してはあまり強い効果は持たないが，リストのように再帰的に大きくなる代数的データ型に対してはとても強い効果を発揮する．実際，同じようなことをするリスト用の変換規則"fold/build"などはGHC.Baseに入っている．

と，ここまで書いたけど，実際にはこれで完全に最適化がキモチよく決まるかというとghcの他の最適化機構やらイロイロなアレやコレやによって，案外そういうわけでもなかったりすることもある．加えて，正しさがよくわかってない規則であるならRULESプラグマをウカツに書くのはとてもよろしくない結果をもたらす．本当に間違った規則を書くこともできるし，変換が停止しない規則を書くこともできる．変換に関わる関数の正格性などによって正しい/正しくないが変わってしまうということもある．いまのところ，確実に何かしたい場合はCPS変換を手で書くのもアリなのだろう．CPS変換する目的自体もいろいろあるだろうし．

ただ，果たして本当にCPS変換はニンゲンがやるようなサギョウなのかというのはコードいっぱい書く前に一考する必要がある．効率化全般に言えることだけど全体からみて本当にソレがボトルネックなのかとかは最初は案外わかんない．CPS変換も人手で正しく変換してあげる必要はあるわけだし，CPS変換によって本当に変換前と意味が変わってないかはそんなにスンナリとわからないんじゃないかな．

折角Haskell使ってるんだからコンパイラとか頭いい研究者達に任せられる分はガンガン任せて，私としてはあんまり難しいこと考えずに楽したい．というかメンドクサイのであんまりやりたくない．