正格性解析 (Strictness Analysis) への反応

shelarcy（しぇらーしぃ） @shelarcy

@pokarim Haskell では、関数の引数の正格性を型情報として埋め込むことはできませんが、データ構成子の引数の正格性を埋め込むことはできます。 http://bit.ly/hoX47C

shelarcy（しぇらーしぃ） @shelarcy

@pokarim あと、未実装の GHC plugins と strict-ghc-plugin を利用すれば、ANN 指示文を使ったメタ情報で正格用であることをコンパイラに伝えることができますね。 http://j.mp/gP0Lb0 http://j.mp/eptz7y

shelarcy（しぇらーしぃ） @shelarcy

@pokarim 現時点ではメタ情報を埋め込むための機能は提供されていますが、GHC の側で正格性に関するメタ情報を解釈してくれないので、ユーザー側で独自に「メタ情報を解釈し、それに基づいて行なう」処理を追加するための plugin 機能（未実装）が必要になります。

pokarim @pokarim

@keigoi そうですね。よりすっきりしました。評価順序を指定することで、停止できたものが停止しなくなることもあるってことですね。

pokarim @pokarim

@shelarcy 詳しい情報をありがとうございます！やるなClean。。。。

pokarim @pokarim

なるほどなー。 "通常の値を「絶対に停止しない事を表す値0」と「停止するかもしれない事を表す値1」の二値からなる領域{0,1}で解釈し、関数をこの領域の上の関数として解釈するという手法" http://bit.ly/fEJ1xh

pokarim @pokarim

関数型言語な式って、グラフをごにょごにょしなくても、通常の値を別のものとして解釈して評価するだけで色々なことがわかったりするね。なんでかな。評価に別の意味を持たせられるってことかな。求む圏論的な説明。

pokarim @pokarim

単純にfunctorってことか。

Κeіsuke Νakanο @ksknac

.@masahiro_sakai 「error は引数に関わらず結果が undefined なので正格」というのは不正確ですね． この論理だと「 f x = error "" で定義される関数も引数に関わらず結果が undefined なので正格」ということになってしまいます．

Κeіsuke Νakanο @ksknac

.@masahiro_sakai error が正格なのは引数を使うからというのが正確な正格性の理由だと思います．

S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください) @esumii

「id は id undefined = undefined なので正格」「error は引数に関わらず結果が undefined なので、error undefined = undefined が成り立ち、正格」 http://j.mp/ifdemr

Masahiro Sakai @masahiro_sakai

.@pokarim 関数型言語に限らず結構使われている手法で、抽象解釈(abstract interpretation)として研究されてます。以前に @ranha さんの紹介してた http://j.mp/iaRdcr とかが分かりやすいかも。

Masahiro Sakai @masahiro_sakai

.@ksknac 正格性の定義上は f x = error "" で定義される関数も正格だと理解しています。そして、正格だからといって、GHCがこのfの引数を先に評価しないのは、GHCの「正格性解析」が(名前に反して)単なる正格性以上の情報を計算しているからだと思ってます。

Masahiro Sakai @masahiro_sakai

.@ksknac いずれにしても補足しておいた方が良さそうですね。ありがとうございます。

Κeіsuke Νakanο @ksknac

.@masahiro_sakai f が正格というのは，error の返す値を ⊥ としているからだと思うんですが， そもそも error と停止しない関数は一緒にしてしまってもいいものなんでしょうか？

pokarim @pokarim

@masahiro_sakai ありがとうございます！ちゃんと名前があったんですね。＞抽象解釈　資料も今読んでいますが、すごく面白いです。

pokarim @pokarim

抽象解釈か。面白いなあ。PDF> http://j.mp/iaRdcr

Masahiro Sakai @masahiro_sakai

.@ksknac A semantics for imprecise exceptions のようなより詳細な意味論を使えば区別できるし、区別した方が良い場面もあると思います。

Masahiro Sakai @masahiro_sakai

.@ksknac ただ、先行評価による最適化の観点から意味があるのは、(単なる正格性では捉えられない)引数の実際の使われ方であって、errorを⊥とするかではないと思います。

Masahiro Sakai @masahiro_sakai

.@ksknac 例えば、f1 x = error x, f2 x = error "", f3 x = fix id のf1とf2で引数の評価戦略を変えることに意味はあっても、f2とf3で引数の評価戦略を変える意味はないでしょうから。

Κeіsuke Νakanο @ksknac

.@masahiro_sakai なるほど．遅延評価を先行評価で最適化するという文脈では，それでいいんですね．ところで，「GHC が正格性以上の情報を計算をしている」というのは正格性解析とは別物なんでしょうか？