2002-12-28
λ. 朝
「おはようボンジュール」で俺を起こすのは止めてくれー。いやマジで鳥肌が……
λ. Ruby-CPL (仮称)
CDTから conditional equation を得る部分を書いた。こないだは無駄かもと書いたけど、自分が理解するのが目的なのだから、無駄だって全然構わないのである。
例えば、直積(product)の宣言、
right object prod(X,Y) with pair is pi1: prod -> X pi2: prod -> Y end object
からは以下のような(条件付き)等式が得られ、この宣言がproductの定義になっていることが確認できる。(あ、「.」は関数結合ね。メソッド呼び出しぢゃないぞっ♥)
- pi1.pair(f0,f1) = f0
- pi2.pair(f0,f1) = f1
- pi1.g = f0 ∧ pi2.g = f1 ⇒ g = pair(f0,f1)
- prod(f0,f1) = pair(f0.pi1,f1.pi2)
同様にleft objectの例として、自然数の宣言、
left object nat with pr is zero: 1 -> nat succ: nat -> nat end object
からは、以下のような(条件付き)等式が得られ、自然数の定義になっていることがわかる。
- pr(f0,f1).zero = f0
- pr(f0,f1).succ = f1.pr(f0,f1)
- g.zero = f0 ∧ g.succ = f1.g ⇒ g = pr(f0,f1)
λ. RHG
少し余裕が出来たので、RHGをパラパラとめくってみたり。たしかに難しいけど、脳の奥が痺れて気が遠くなるようなconceptualな難しさではないようなので、とりあえず安心。じっくり読めば何とかなりそう。
ところで、参考文献が随分マニアックな気が……。『プログラム意味論』(横内寛文[著])まで入ってるよ……
2004-12-28
λ. 可変長引数の関数?
multi-parameter class を使って可変長引数っぽいことが出来ないかと思って、ちょっと試してみた。引数の型を明示する必要があるのがイヤだな。
class VAFun arg result x | x -> result where collectVAList :: ([arg] -> result) -> [arg] -> x instance VAFun arg Int Int where collectVAList k xs = k (reverse xs) instance VAFun arg result x => VAFun arg result (arg -> x) where collectVAList k xs x = collectVAList k (x:xs) withVAList :: VAFun arg result x => ([arg] -> result) -> x withVAList k = collectVAList k [] vaSum :: VAFun Int Int x => x vaSum = withVAList sum
*Main> vaSum
<interactive>:1:
No instance for (VAFun Int Int x)
arising from use of `vaSum' at <interactive>:1
In the definition of `it': it = vaSum
*Main> vaSum :: Int
0
*Main> vaSum 3 2 :: Int
<interactive>:1:
No instance for (VAFun Int Int (t -> t1 -> Int))
arising from use of `vaSum' at <interactive>:1
When checking the type signature of the expression:
vaSum 3 2 :: Int
In the definition of `it': it = vaSum 3 2 :: Int
*Main> vaSum (3::Int) (2::Int) :: Int
5
[追記] collectVAListではなくwithVAListをVAFunのメソッドにしてしまえる。ytsの日記(2005-01-02) を参照のこと。
2007-12-28
λ. ローソンで Edy! キャンペーン
「今ならローソンでのEdy2,000円分の利用またはチャージで、ソニー“ウォークマン”を抽選でプレゼント！」とのことなので、今Edyへのチャージでポイントの付くクレジットカードを持っていないこともあり、一応¥2000だけチャージしてみた。
【追記】 まあ、当選しなかったけどさ。
2008-12-28
λ. 「伊藤洋一のRound Up World Now!」休止するのか
もう二年以上聴いている「伊藤洋一のRound Up World Now!」だけど、12月26日の放送を最後にいったん番組を休止するのか。 そのアナウンスで10年3ヶ月間も続いていた番組だと知り、そんなに長く続いていた番組なのかと驚いた*1。 とりあえず、これまでありがとうございました。 有料化されても月500円くらいだったら聴き続けたいとは思うが、どうなるやら……
【2009-01-11追記】 土日の勉強会への行き帰りで聞くことが多かったので、今日圏論勉強会に行くとき、ああ今週はないんだなと実感して、少し寂しかった。
*1 Podcastでしか聴いていなかったので……
2010-12-28
λ. 正格性解析 (Strictness Analysis)
この記事はHaskell Advent Calendarのために書かれたものです。(22日目)
正格性解析(strictness analysis)は、Haskellのような遅延評価を行う純粋関数型言語での最も基本的な最適化のひとつの割に、あまり知られていないようなので、簡単に紹介してみることに。
動機
よくある例だけど、末尾再帰で書かれた
sum' :: Int → [Int] → Int sum' s [] = s sum' s (x:xs) = sum' (s+x) xs
というプログラムは、Haskellでは最適化が行われない限り悲惨なことになる。
sum' 0 [1,2,3,4] を計算すると、sum' 0 [1,2,3] ⇒ sum' (0+1) [2,3] ⇒ sum' ((0+1)+2) [3] ⇒ sum' (((0+1)+2)+3) [] ⇒ (((0+1)+2)+3) という風に実行が進む。引数のsが未評価のまま蓄積されていき、だんだんと大きな式になってしまっている。
この例だとどうってことはないけど、入力がもっと大きい場合にはヒープを圧迫するし、最終的に (((0+1)+2)+3) を評価するときも、+3と+2をスタックに積んでから0+1を評価するという風になるので、入力が大きい場合にはスタックを大量に消費してしまう。
seqとBangPatterns
この問題は sum' が引数sを評価しなかったからで、引数を評価するようにすれば、sum' 0 [1,2,3] ⇒ sum' 1 [2,3] ⇒ sum' 3 [3] ⇒ sum' 6 [] ⇒ 6 という風に実行が進むようになり、ヒープを消費してしまう問題もスタックを消費してしまう問題も解決する。
そのようにするにはseqを使って
sum' :: Int → [Int] → Int sum' s [] = s sum' s (x:xs) = seq s $ sum' (s+x) xs
とすれば良い。 seq x y の直観的な意味は「xを評価してからyを返す」というもの。 なので、上の例では再帰呼び出しの前にsが評価されるようになり、問題が解決する。
もしくは、seqの代わりにBangPatterns拡張を使って
sum' :: Int → [Int] → Int sum' s [] = s sum' !s (x:xs) = sum' (s+x) xs
と書けば良い。 BangPatternsはseqのシンタックスシュガーと思って良い。もっとも、完全に構文的に変換するのは大変そうだけど。
正格性解析
「…と書けば良い」って、そりゃ書けば良いんだけど、そんなのイチイチ書きたくないので、GHCとかはそれを自動的にやってくれるようになっていて、それが正格性解析とその結果を利用した最適化。
そもそも上のsum'の場合だと、引数sは後で絶対評価されるのだから、それを先に評価してしまっても、結果は変わらないはず(停止するはずのプログラムが停止しなくなったりはしないはず)。正格性解析はこういう「先に評価してしまっても構わない引数」というのを発見してくる。で、コンパイラはそういう引数を先に評価したりとか、あるいはこの情報をworker-wrapper変換のような他の最適化のために利用する。
この「先に評価してしまっても構わない引数」というのをもう少し数学的に考えたのが関数の正格性で、正格性解析というのは文字通り、関数の正格性を解析する。
関数の正格性
関数fが正格なのは f ⊥ = ⊥ が成り立つとき。 ここで ⊥ は停止しない計算とかエラーとかを表した値である。Haskellでは典型的にはundefinedとかerror関数がこの値を持つ。MLなどの関数は全て正格な関数になっているけど、Haskellの関数は正格とは限らないので、Haskellは非正格関数型言語(non-strict functional language)と呼ばれたりもする。
上の正格性の定義は一引数関数に対してのものだったけど、多引数関数に対しても拡張できる。例えば、3引数関数fが 第二引数に対して正格というのは、任意のx,zについて f x ⊥ z = ⊥ が成り立つとき。
幾つかお馴染みの関数の正格性を考えてみる:
- notは not undefined = undefined なので明らかに正格。
- id は id undefined = undefined なので正格。その関数自身が評価を行わなくても正格な場合もあるので注意。
- error は引数に関わらず結果が undefined なので、error undefined = undefined が成り立ち、正格。
- 整数の加算 (+) は undefiend + b = undefined かつ a + undefined = undefined なので、どちらの引数に対しても正格。
- (&&) は undefined && y = undefined なので第一引数に対して正格だけど、False && y = False ≠ undefined なので第二引数については非正格。
- 同様に const も第一引数に対して正格で、第二引数に対して非正格。
- seqの意味は以下の等式で定義されているので、どちらの引数に対しても正格。
- seq ⊥ b = ⊥
- seq a b = b, if a ≠ ⊥
上のsum'を考えると、sum' undefined xs = undefined でかつ sum' s undefined なので、この関数はどちらの引数に対しても正格である。したがって、どちらの引数も呼び出す前に評価してしまって構わないことが分かる。
正格性の計算方法
お次はこの正格性の情報を具体的にどうやって計算するか。方法は幾つかあるのだけど、私がちゃんと読んだことがあるのは「Strictness analysis — a practical approach」(Chris Clack and Simon L Peyton Jones)という論文だけなので、これを簡単に紹介する。
- <URL:ftp://cs.ucl.ac.uk/functional/papers/Published/strict.ps.gz>
- <URL:http://www.springerlink.com/content/f066h27646531051/>
この論文の方法は、通常の値を「絶対に停止しない事を表す値0」と「停止するかもしれない事を表す値1」の二値からなる領域{0,1}で解釈し、関数をこの領域の上の関数として解釈するという手法を使っている。値からこの領域上への関数を ABS と書くことにする。
関数 f に対して、この領域上で解釈した関数 f# は ABS (f x) = f# (ABS x) を満たす。これは「計算後に抽象化したもの」が、「抽象化してから抽象化した領域の上で計算した結果」と一致するということを言っていて、抽象化に求められる条件になっている。
例えば以下のような関数を考える。ただし、if' p t e = if p then t else e とする。
- g p q r = if' (p == 0) (q + r) (q + p)
この関数を{0,1}上で解釈した関数 g# に期待される条件を考えると、
- g# (ABS p) (ABS q) (ABS r) = ABS (if' (p == 0) (q + r) (q + p)) = if'# (ABS p ==# ABS 0) (ABS q +# ABS r) (ABS q +# ABS p)
となる。引数を書き換えると、
- g# p q r = if'# (p ==# ABS 0) (q +# r) (q +# p)
となる。
ここで、0は必ず停止するので ABS 0 = 1。また、「x==y が停止するかもしれない」のは、xが停止するかもしれなくて、かつyも停止するかもしれないときだけなので、(==#) = (&&) となる。同様に (+#) = (&&) 。また、「if' x y z が停止するかも知れない」のは、xが停止するかもしれなくて、かつyとzのいずれかが定義するかもしれないときだけなので、if'# x y z = x && (y || z) となる。
これらを g# の定義に当てはめると、
- g# p q r = (p && 1) && ((q && r) || (q && p)) = p && q && (r || p)
となる。ここから、
- g# 0 1 1 = 0 && 1 && (0 || 1) = 0 なので、pが停止しない場合、q, r が停止しても、全体は停止しない。すなわち、ｇはpに関して正格。
- g# 1 0 1 = 0 なので、qが停止しない場合、p, r が停止しても全体は停止しない。すなわち、gはqに関して正格。
- g# 1 1 0 = 1 なので、rが停止しない場合でも、p, q が停止すれば全体は停止するかもしれないことがわかる。すなわち、ｇはrに関して正格ではない。
ということが分かる。
再帰や高階関数を扱うこともできるけど、それは論文を参照してくださいな。といっても、多分もっと新しい論文を読んだほうが整理されているとは思う。この論文は抽象解釈といいつつ、あまり抽象解釈っぽくないし、もっと整理された論文があるんじゃないかと予想。ただ、この論文は束のフロンティアの概念とそれを利用したアルゴリズムを提案していて、そこは結構面白いと思うんで、読んで損はないと思う。
実験
正格性解析は最適化を有効にすると有効になるけど、 -fstrictness で明示的に有効にしたり、-fno-strictness で明示的に無効にしたりできる。以下のプログラムを -O と -O -fno-strictness でそれぞれコンパイルして比較してみると、違いが分かるはず。
main = print $ sum' 0 [1..10000000]
限界
このように素晴らしい正格性解析なのだけど、いつもうまく行くわけではない。
例えばsum'の定義が
sum' = foldl (+)
だったら、foldlがインライン化されない限り、正格性解析による最適化は期待できない。
というのは、foldlの定義が以下のようなものだとして、cの定義が分からないままでは、cが第一引数に関して正格かどうかわからず、結果としてfoldlもnに対して正格かどうかが分からないため。
foldl :: (a -> b -> a) -> a -> [b] -> a foldl c n [] = n foldl c n (x:xs) = foldl' c (c n x) xs
昔から思っているんだけど、こういう時って「cが正格なときとcが非正格なときようのコードを両方生成しておいて、さらにcの実行時のクロージャに正格性の情報を格納しておいて、実行時にcの正格性情報を見てどっちのコードか選ぶ」なんてことはできないものなのかな。
追記
Togetter - 「正格性解析 (Strictness Analysis) への反応」 で頂いた反応などをまとめてみます。
他の参加記事へはこちらから
2011-12-28
λ. Haskell Program Coverage ツールキットを試してみる
この記事は、Haskell Advent Calendar 2011 の15日目の記事として書かれました。
色々書きたいことはあったはずなのだけど、いざ書こうと思うと、ちょうど良いネタはなかなかなく悩んでしまい、大幅に遅延してしまいました。 最初は、category-extrasの紹介でもしようかと思ったのだけれど、どうも圏論の知識をある程度前提にしないと面白い部分が書けなさそうだし。 悩んだんだけど、そういえば ICFP Programming Contest 2009 に参加した際 にカバレッジ機能を使ってみたくなったのを思い出し、GHCのカバレッジ測定機能について試して、簡単に紹介してみることに。
カバレッジとは
コードカバレッジ(Code Coverage)とは、プログラムのテスト時に使われる指標で、プログラムがどれだけ網羅的にテストされたのかの度合いを表すものです。 コードカバレッジには幾つか種類があり、メジャーなものでは、命令網羅(statement coverage)、分岐網羅(branch coverage)、決定網羅(decision coverage)、パス網羅(path coverage)といったものがあります。 例えば、命令網羅であれば、プログラムの全行数中、テストによって実行(カバー)された行数の割合を現してます。 コードカバレッジが低いということは、プログラムをちゃんとテストできていないということであり、コードカバレッジの高さはテストの品質の必要条件になります。
Haskell Program Coverage (HPC) ツールキット
gccにはgcovが付属していてカバレッジの測定ができますが、GHC にも Haskell Program Coverage (HPC) ツールキットというのが付属していて、GHCのドキュメントでも使い方が解説されてます。
今回はこれを参考にHPCを少しだけ試してみることにします。
ターゲット
今回は拙作のPTQパッケージで試してみます。 これは英語の平叙文を受け取って一種の論理式へと変換するツールで、様々な文法や変換規則を扱う部分がそれぞれあるため、色々な種類の入力を与えてみないとプログラムの全体は駆動できないはずです。
コンパイル
ドキュメントによると-fhpc オプションを指定して「ghc -fhpc Recip.hs --make」などとコンパイルすれば、カバレッジ測定機能を有効にしてコンパイルできるようだ。
そこで、tarballを展開して「cabal configure --ghc-options=-fhpc && cabal build」としてコンパイルしてみる。
コンパイルの様子は普通の場合と特に変わらないですが、.hpcディレクトリに*.mixファイルというのが沢山できてました。
ドキュメントによるとこれはHPCにとっての.hiファイルのようなものだそう。
% ls .hpc CGI.mix Main.mix Report.mix URLEncoding.mix IL.mix P.mix ReportHTML.mix Version.mix MP.mix Parser.mix Translation.mix
実行
で、実行してみる。
% dist/build/ptq/ptq PTQ version 0.0.5 Type :quit to quit PTQ> Every man loves a woman such that she loves him. Parsed: F10 0 (F2 every man) (F4 (He 0) (F5 love (F2 a (F3 1 woman (F4 (He 1) (F5 love (He 0))))))) : t (中略) Translation (MP applied): forall x0 : e. man x0 -> (exists x1 : e. woman x1 && love* x0 x1 && love* x1 x0) : t (中略) PTQ> :quit % ls -l *.tix -rw-r--r-- 1 sakai staff 7991 12 29 00:28 ptq.tix
ptq.tix というファイルが出来ていた。
レポート機能
測定できているはずなので、測定結果をもとにレポートを生成する機能を試してみる。
% hpc report ptq.tix hpc: can not find IL in ["./.hpc"]
あれれ、怒られてしまった。 ILというのは実際には使っていないモジュールだったので、そのせいかも……
気をとりなおして、モジュール名を指定して試す。
% hpc report ptq.tix Parser
73% expressions used (858/1171)
80% boolean coverage (4/5)
100% guards (0/0)
66% 'if' conditions (2/3), 1 always False
100% qualifiers (2/2)
52% alternatives used (32/61)
85% local declarations used (17/20)
89% top-level declarations used (105/117)
% hpc report ptq.tix Translation
22% expressions used (143/623)
100% boolean coverage (0/0)
100% guards (0/0)
100% 'if' conditions (0/0)
100% qualifiers (0/0)
26% alternatives used (13/50)
16% local declarations used (5/30)
80% top-level declarations used (4/5)
なんか、 色々出てきたけれど、項目の意味は大体以下のようなものでしょうか。
- expression used
- ソース中のどれくらいの割合の式が評価されたかというもので、命令型言語での命令カバレッジに相当。
- boolean coverage
- ガード、if式の条件、リスト内包表記のガード(qualifier)が、真に評価される場合と、偽に評価される場合の両方が実行されたか。
- alternatives used
- 複数の節からなる定義や、case式、if式などで各分岐が実行されたか。 古典的な命令型言語での分岐カバレッジ(branch coverage)に近い?
- local declarations used
- 局所定義のどのくらいが使われたか。 古典的な命令型言語での関数カバレッジ(Function coverage)に近い?
- top-level declarations used
- トップレベル定義のどのくらいが使われたか。 古典的な命令型言語での関数カバレッジ(Function coverage)に近い?
1文を翻訳させただけなので、カバレッジは非常に低いのではないかと思っていたけど、パーサの方は案外高かったのでビックリ。 これは翻訳機の方は構文木にあう部分しか実行されないのに対して、パーサの方はマッチするかどうか色々な構文を試行しているためでしょうか。
マークアップ機能
hpc markup コマンドを使うと、表のHTMLと、ソースファイルをマークアップして色付きHTMLを作ってくれます。
ここでは hpc markup ptq Parser Translation としたところ、以下のファイルが生成されました。
- 表
- マークアップされたソースファイル
表の情報はレポートと同じ。 ソースファイルのマークアップの方は、実行されなかった箇所が黄色でマークアップされ、条件式等でTrueにしか評価されなかった箇所は緑、Falseにしか評価されなった箇所は赤で表示されている。 これは結構分かりやすそうです。
まとめ
GHC にはHaskell Program Coverage (HPC) ツールキットが付属していて、コードカバレッジを非常に簡単に測れて、測定結果も見やすく表示することができます。
日本のHaskellコミュニティではHPCの事を聞いたことはこれまであまりなかったけれど、簡単に使えるので、「テストがちゃんと出来ているかどうか」の確認の一助に使ってみるとか、あるいは「プログラムをミスって実行されるべき箇所が実行されていない」なんてことが起こっていないか確かめるとかに使ってみると良いと思います。
ただし、HPCでサポートされているカバレッジは、命令型言語でいう命令カバレッジや分岐カバレッジに相当する緩い基準であり、高い信頼性が要求される分野で用いられているModified condition/decision coverage (MC/DC)といった基準に相当するものではありません。 なので、HPCでのカバレッジが高いからといって十分テストされていると過信するのは危険です。
あと、ちょっと気になったのは、HPCはGHCiでは使えないので、HUnitやQuickCheckをGHCi上で使う際にはカバレッジの測定ができないこと。 コンパイルして実行すれば良いのだけど、そうなるとテスト自動化のためのちゃんとした仕組みが欲しくなるね。
追記
shelarcyさんから以下の補足をもらいました。
@masahiro_sakai GHC7.2.x に付属の Cabal 1.12.0 の test 機能は、HPCと連携できるようになっていますね。 twitter.com/#!/shelarcy/st… > テストの自動化
— shelarcy（しぇらーしぃ） (@shelarcy) December 29, 2011
@masahiro_sakai c.f. haskell.org/ghc/docs/7.2.2… haskell.org/ghc/docs/7.2.2…
— shelarcy（しぇらーしぃ） (@shelarcy) December 29, 2011
@masahiro_sakai あと、HPC への正式対応のない GHC 7.0.x の Cabal 1.10.x.x でも、新しくなった test 機能を使ってある程度自動化させることはできますね。 voqn.blogspot.com/2011/12/bdd-on…
— shelarcy（しぇらーしぃ） (@shelarcy) December 29, 2011
リンク
- Haskell Advent Calendar 2011 | Gihyo Digital Publishing (Gihyo Digital Publishing からの電子書籍(epub)としての配信)
