2006-11-07

■

Stgマシンの細部のイメージが全然つかめぬー。Stgマシンについてまともに書いたものが、Peyton Jonesのオリジナル論文くらいしか見当たらないので、つまり、これを読んで分からないバカは死ねってことですか、うぅ。というか、ページ数が多すぎです！10ページ以内くらいにしてください。まあ、なんかruntime周りのコードを読んでないのが敗因という気がしないでもない

2006-11-07

Core Simplifier

GHC

とりあえず、分からないものは放置の方向で!コメントでツッコミをもらって、GHCはやっぱり賢かったということに気付いたよ。最適化オプション付けると、全然ちげー。"main = return(1)"程度なら、型宣言してもしないでも、生成されるコードは一緒だとか、関数テーブル辿るの無駄っぽいなーと思ったのも、ちゃんと静的に解決されるとか、ぬー。

test = sin(2.3)+3.1
main = return(test)

こんなのを書くと、-fext-core出力が

  lvl :: GHCziNum.Integer = GHCziNum.Szh (31::GHCziPrim.Intzh);
  lvl1 :: GHCziNum.Integer = GHCziNum.Szh (10::GHCziPrim.Intzh);
  lvl2 :: GHCziNum.Integer = GHCziNum.Szh (23::GHCziPrim.Intzh);
  x :: GHCziFloat.Double =
    %case (GHCziFloat.Double) (GHCziFloat.zdwzdsfromRat Main.lvl2 Main.lvl1)
    %of (wild::GHCziFloat.Double)
      {GHCziFloat.Dzh (x1::GHCziPrim.Doublezh) ->
	 %case (GHCziFloat.Double) (GHCziFloat.zdwzdsfromRat Main.lvl Main.lvl1)
	 %of (wild1::GHCziFloat.Double)
	   {GHCziFloat.Dzh (y::GHCziPrim.Doublezh) ->
	      GHCziFloat.Dzh (GHCziPrim.zpzhzh (GHCziPrim.sinDoublezh x1) y)}};

こんな感じになる。やった！これくらいなら手で書けるよ！けど、この浮動小数点の扱いはどうなんだろう。

"map f (map g x) -> map (f.g) x"程度の最適化も普通にされるっぽいなー。GHC.Base見ると、直接、こういうRULESは定義されてない。けど、

build 	:: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
{-# INLINE [1] build #-}
	-- The INLINE is important, even though build is tiny,
 	-- because it prevents [] getting inlined in the version that
	-- appears in the interface file.  If [] *is* inlined, it
	-- won't match with [] appearing in rules in an importing module.
	--
	-- The "1" says to inline in phase 1

build g = g (:) []
----------------------------------------------------------------------
{-# RULES
"fold/build" 	forall k z (g::forall b. (a->b->b) -> b -> b) . 
		foldr k z (build g) = g k z
----------------------------------------------------------------------
{-# RULES
"map"	    [~1] forall f xs.	map f xs		= build (\c n -> foldr (mapFB c f) n xs)
"mapList"   [1]  forall f.	foldr (mapFB (:) f) []	= map f
"mapFB"	    forall c f g.	mapFB (mapFB c f) g	= mapFB c (f.g) 
  #-}

あたりを使えばできそう。

map f (map g xs) 
= {apply "map" RULES" twice} 
build (\c n -> foldr (mapFB c f) n (build (\c1 n1 -> foldr (mapFB c1 g) n1 xs)))
= {apply "fold/build" RULES}
build (\c n -> (\c1 n1 -> foldr (mapFB c1 g) n1 xs) (mapFB c f) n)
= {beta-reduction.怪しい･･･}
build (\c n -> (foldr (mapFB (mapFB c f) g) n xs))
= {apply "mapFB" RULES}
build (\c n -> (foldr (mapFB c (f.g)) n xs))
= {build inlining}
(foldr (mapFB (:) (f.g)) [] xs)
= {apply "mapList" RULES}
map (f.g) xs

実際GHCがどういう順序で計算してるかはわからんけど、RULESの適用順序が違うと、正しい結果に辿りつかなくなる可能性もあるような気がするけど、そのへんはどうしてるんだろうか

{-# RULES 
 "length/map" 
   forall f x. length (map f x) = length x #-}

みたいな最適化は、GHCではされないよう。

lengthの定義(base/GHC/List.lhs)は返り値がInt型なので、あれだけど、genericLengthとかあるらしいので、Data.Listを見る。特に、RULESは定義されてないし、genericLength使っても、やっぱしmap消去はされないっぽい。

てことで、自前でLengthを定義

{-# OPTIONS -fglasgow-exts #-}
myLength :: (Num i) => [b] -> i
myLength = foldr (\_ -> (+1)) 0
test =  myLength (map (+1) [1,2,3,4,5])
main = return test

なんか、これだけでいけそうな気がしたので、-O付けて、-ddump-simpl

Rec {
Main.go :: [GHC.Num.Integer] -> GHC.Num.Integer
[GlobalId]
[Arity 1
 NoCafRefs
 Str: DmdType S]
Main.go = \ (ds_a1Nm :: [GHC.Num.Integer]) ->
            case GHC.Num.Integer ds_a1Nm of wild_a29v {
              [] -> z_r2ax; : y_a29t ys_a29u -> GHC.Num.plusInteger (Main.go ys_a29u) Main.lit
            }
end Rec }
----------------------------------------
Main.x :: GHC.Num.Integer
[GlobalId]
[Str: DmdType]
Main.x = Main.go Main.lvl8

長いので途中すっとばしたけど、Main.goがmyLength相当の関数で(goはfoldrの定義内部で使われてる関数だと思う)、Main.xがtest相当の変数っぽいので、map消去できてる。うーむ、あっさりできたな。GHCが確実にmyLengthを展開してくれるかどうかはわからんので、一応INLINE指定しておいた方がいいのかな。

標準ライブラリが、foldr使って定義してないのは、末尾再帰じゃないからとか、そういう話なのかねー。と思ったが、"foldr (\_ -> (+1)) 0" だけでなく、"foldl (\n _ -> n+1) 0" , genericLengthも長さ100万~1000万程度のリストでスタックオーバーフロー起こすな。lengthの定義は

length                  :: [a] -> Int
length l                =  len l 0#
  where
    len :: [a] -> Int# -> Int
    len []     a# = I# a#
    len (_:xs) a# = len xs (a# +# 1#)

となってる。Int#が、即値みたいな感じなのかね(Peyton Jonesの論文に、unboxed typeとか書いてあったけど)。だとすると、Integer使う限り、どうしようもないのかも。でも、genericLengthを普通のlengthにしといて、今のlengthは、別扱いにするのが、Haskell的設計なんでないかという気はするけど

フフ・・・へただなあ・・・カイジ君・・・へたっぴさ・・・・欲望の開放のさせ方がへた・・・　カイジ君が本当に使いたいのは・・・こっちのfoldr・・・!これを融合変換使って・・・・中間データを一気に消去してさ・・・・効率化に頭を悩まさずコードを書きたい・・・・・・・・！だろ・・・・・？だけど・・それはあまりにも高価だから、こっちの・・・Int#使ったlengthでごまかそうって言うんだ・・・・カイジくん・・・ダメなんだよ・・・！そういうのが実にダメ・・！その妥協は痛ましすぎる・・・

一方のgenericLength見ると

genericLength           :: (Num i) => [b] -> i
genericLength []        =  0
genericLength (_:l)     =  1 + genericLength l

と定義されている。いちいちfoldr使って〜とか意識すんのはだるいし、こっから適当に「ラムダ消去」して、foldr使った定義導けると嬉しいわけだけど、そういうのって何とかならんのかねー

あとまあ、どうでもよいが、コンパイラのソースをGHCから気軽に利用できるようになっているといいなーと思った。CoreやStgのダンプが見づらいから自分専用の出力フォーマット定義したいとか、そういう程度の理由なんだけど。

2006-11-07

fold/build/augment/unfold/destroy

圏論

というような話がリストでしか言えないなら、新しくデータ型を作るたびに、ルールを発見せねばならず、大して面白くもないんだけど、foldとかbuildとかaugmentは、圏論的背景を持ってて、Haskellの他のデータ構造でも使えるという話なので、素晴らしいかもしれない。けど、実際には、今のHaskellだと、データ型定義するごとに自分でfold/etc...とルールを定義する必要がある気がする

とりあえず、
http://www.cs.ioc.ee/~tarmo/misc/builds-subm.pdf
あたりを読もうと試みる。Cを圏として、FをCの自己関手、Alg(F)を、F-代数の圏とすると、忘却関手U(F):Alg(F)->Cの極限が存在すれば、F-始代数と同等で、双対的に、F-余代数の圏Coalg(F)に対して、忘却関手V(F):Coalg(F)->Cの余極限が存在すれば、終余代数と同等になる。という話までは理解した。

Haskellで書かないとイメージわかん

{-# OPTIONS -fglasgow-exts #-}
data Mu f = Build (forall x. (f x) -> x -> x)
data NatF x = NatC (x->x)
type Nat = Mu NatF

fold :: (f x) -> x -> (Mu f) -> x
fold s z (Build theta) = theta s z

zeroN :: Nat
zeroN = Build (\_ -> id)

nat_to_int :: Nat -> Integer
nat_to_int n = fold (NatC (+1)) 0  n 

instance Show Nat where
 show n = show (nat_to_int n)

とか、こんな感じですか。Church数として自然数が定義できるのはいいけど、標準的(?)なNatの定義(data NatF x = Zero | Suc x;type Nat = Fix NatF)と、どう繋げればいいんだろう。

(2006/11/21追記)上の構成は一応動くけどおかしい。data NatF x = NatC (x->x);type Nat = Mu NatFとか意味不明。NatFは普通に定義して、*1 -> x -> (Nu f)で、リストの場合は、「f x = 1 + a*x」なので、Maybe (a,x)を使ってるだけだ)

*1:Either () x)->x)->xと(x->x)->x->xの間に、自然な一対一対応があるので、それを介して、data NatF x = Zero | Suc x;type Nat = Fix NatFという定義と繋がる。つまり、Mu NatFとFix NatFの間に一対一対応がつくれる。この対応は、任意の関手について半自動的につくれるけど、Haskellの範疇でそれを自動化するのは多分難しい dinaturalityとかは何が嬉しいのかよく分からないので、多分どうでもいいとして、augmentを書こうとして挫折した。Monadに持ち上げるとこの(>>=)が定義できねー。いや、もう眠いから。多分明日には書ける(かもしれない)!こんな複雑な構成思いつくやつは頭がイカレテルと思いますよ！てかねー、仮に書けても、これ使ってコード書くのは大変だよなー。あとなんか、unfoldrで突然現れるMaybeモナドは何故に？てか、そもそも、Haskellのリストって始代数で終余代数なん？ #(追記)余りにもアホなこと書いてたな〜。私はunfoldの定義を100万回暗誦するべきだと思った。unfold::(x -> (f x

2006-11-07

Parametricity、Genericity

Haskell

GHC.Baseの定義見ると、

foldr            :: (a -> b -> b) -> b -> [a] -> b
build 	:: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]

ってなってんだよね。forall付けていいときとダメな時の差がわかんねーと思って、
Theorems for free(P.Wadler)
http://www.informatik.uni-bonn.de/~loeh/ST-05-2003.pdf
あたりを眺めて見た。よく理解できなかったけど、色々あるのだなーと思った(小学生の感想か

Theorems for freeでは、foldの型が

fold : forall X.(forall Y.(X->Y->Y)->Y->[X]->Y

となってるぜ。なんでだろう。(==)の型が、forall x.x->x->Boolでないというのは、関数とかだと等しいことの判定ができるとは限らないので、当然じゃない？という気もしなくもない。型だけ見て定理が導けるというのは面白いね。全然理解してないが、こういう話はだ〜いすき。型情報利用して、動的にルールを生成するとかいうのも、GHCではやられてるんだろうか。あと、⊥=forall x.xの理由は何となく分かった気がしたよ。つうか、このへんの知識が全然ないよな〜、むー