正格性解析

GHC

以前から気にしていたのだけど、strictness analysisってstrictかどうか解析するんだよねーというくらいしか知識がないので(そのままやんけ。型推論も型を推論するんだよねーというくらいしか分かってないけど、あれはひたすら単一化するんかね)、適当に調べて見ることに。

まずGHCの実装を眺めて見る。前にちょろっと書いたcore2coreの流れを見ると

doCorePass CoreDoStrictness	       = _scc_ "Stranal"       trBinds  dmdAnalPgm

となってる。trBindsは第一引数の関数にほぼ処理を丸投げなので、結局、dmdAnalPgmというのを見ればいいらしい。その下に

#ifdef OLD_STRICTNESS		       
doCorePass CoreDoOldStrictness	       = _scc_ "OldStrictness" trBinds doOldStrictness
#endif

#ifdef OLD_STRICTNESS
doOldStrictness dfs binds
  = do binds1 <- saBinds dfs binds
       binds2 <- cprAnalyse dfs binds1
       return binds2
#endif

とあるんだけど、OLD_STRICTNESSってことは多分もう使われてないんだよね。ううん知らないけどきっとそう。dmdAnalPgmは、compiler/Stranal/DmdAnal.lhsで定義されてる。

しかし、これを読んでも何をやってるか全く分からなかったので、助けて！ドラえもん！

The strictness analyzer does demand analysis, absence analysis, and box-demand analysis in a single pass. (ToDo: explain what these are.)

役に立たなかった


とりあえず、Demand analysisとやらの論文
Analyzing demand in non-strict functional programming languages
148ページもあるよ！やる気を失った


他のアルゴリズム。OLD_STRICTNESSで使われてるsaBindsは、StrictAnal.lhsにMycroft-style strictness analyserと書いてあって、WikipediaのStrictness analysisの項見ると、(Mycroftのabstract interpretationに基づくstrictness analysis(?)とDemand analysisの)他にProjection-based strictness analysisっつーのがあるみたいだな。一杯ありすぎなんだよ！


ついでに、CLEANはどうしてるのか。http://www.st.cs.ru.nl/Onderzoek/Projecten/Clean_System/clean_system.htmlより(正確には、つながらないのでGoogleキャッシュから)

We have decided that it was therefore needed to recode a huge part of the Clean compiler, this time in Clean of course. From the old compiler only the backend will be reused, the code generation part that generates platform independent ABC-code (this can be compared with byte code) and the strictness analyzer based on abstract reduction (explained in Nocker's PhD thesis).

Nockerさんとやらのstrictness analyzer based on abstract reductionというのらしい。また違うヤツかよ！(今もこのアルゴリズムを利用してるのかは知らんが。NockerってCLEANのエライ人っぽい？)

結論:正格性解析は奥が深い(情報量0)


う〜ん、とりあえず、一番古いAbstract interpretationベースのStrictness analysisとやらを理解しようと思って、WadlerのStrictness Analysis on Non-Flat Domains (by Abstract Interpretation over Finite Domains)を読んで見たけど、よくわからん。domainと呼んでるのは、領域理論をよく知らんので正確な定義が分からんけど、最小元と最大元を持つ半順序集合とかそんな感じ？型tに対応する有限domainをt#とすると、例えば一引数関数h::a->bに、h#::a#->b#を対応させることができて、#の性質から、h#がstrict(h#(⊥)=⊥)なら、hもstrictになることが言えるとか、そういうシナリオっぽい(a#とb#は有限なので、少なくとも原理的には、h#がstrictかどうかは決定可能)

で、各データ型に対して、有限domainを与えるんだけど、そこのやり方がなんかわかんないな。リストについては何か説明あるけど、∞が謎だし、例えば、二分木に対して、どういう有限domainを考えればいいのかわかんない気が(あるいは、「ある程度の一貫性」が成り立てば何でもいいんだろうか)。まあ、別に難しい話ではないんだろうと思うけど。あと高階関数