■

正格性解析をなめてた。もっと簡単なもんかと。とりあえず、abstract interpretaionは一応理解したと思う。
・Strictness Analysis Another Methodの前半
・Introduction to Abstract interpreation:　http://akira.ruc.dk/~madsr/webpub/absint.pdf
のstrictness analysisの項が参考に

最も簡単なケースでは、扱うデータは整数やブール値などのプリミティブなものだけ(リストとかは考えない)、高階関数やポリモーフィズムは考えない、という仮定を置いて、二元からなるドメイン{T,U}を考える(TとUには、T>Uという順序を入れる)。で、xの"abstract interpretaion"をx'で表すことにする。整数なんかのプリミティブなデータxに対しては、xがボトムなら、x'=Uで、それ以外の場合は、x'=T。それと、些か天下り的に、a ==' b = min(a,b), a +' b = min(a,b),a -' b=min(a,b),(if a then b else c)' = min(a',max(b',c'))などとする。あと関数適用について、(f x)'=f' x'とか。

で、sum n = if n==0 then 0 else n+(sum n-1)に対して、sum'を計算すると

sum' x 
= min(x ==' 0' , max(0' , x +' (sum' (x -' 1')))) 
= min(min(x,T) , max(T , min(x , sum'(min(x,T))))) 
= min(min(x,T), T)
= min(x,T)

で、sum' T = T ,sum' U = Uとなる。Uがボトムに対応する値で、他にUに対応する値はないので、sumはstrict

sumの場合だと、再帰的定義から、再帰が消えてしまったけど、acc n m = if n==0 then m else acc(n+1,m-1)みたいな例だと、再帰が消えない

acc' a b
= min (min(a,T) , max (b , (acc' min(a,T) , min(b,T)))) 
= {- min(x,T) = x -}
min (a , max(b, (acc' a b)))

で、例えば

acc' T U 
= min(T , max(U,(acc' T U)))
= min(T , acc' T U)
= acc' T U

となって、acc' T U = Tでも、acc' T U = Uでもいい感じだけど、こういう時は、最小解を考えるお約束らしい。もう少し、機械的にやるには、f a b x = min(a,max(b,x))という関数fを考えて、Uに(f a b)を繰り返し適用していき(f a bの)不動点を得られたら終了(fix (f a b) = acc' a bだから)。で、acc' T U = Uが分かったので、accは第二引数についてstrictだと結論する。要するに言語の非常に小さい意味論を与える感じ

けど、まだ実装のイメージがつかめん。疑問点は、
・プリミティブ関数のabstract interpretaionはどうしたらいいのか（全部strictでいい？
・あと、リストみたいなデータに、どういうドメインを対応させるか

abstract interpretaionベースの正格性解析をポリモーフィズムやら、高階関数を扱えるように拡張するのは無理があるかなぁという気がした。あと、abstract interpretaionは正格性解析のための仕組みではなくて、もっといろいろ応用があるらしい

まあ、それはそれとして、GHCだと

foldr (+) 0 [1..1000000]

程度で、Stack Overflow起こすのはアレだよなーというか、これくらい正格性解析してくれよーというのがあるんだけど、CLEANだとどうなるのか見てみたら、foldr (+) 0 [1..1000000]はスタックオーバーフロー起こすのに対して、foldl (+) 0は、[1..100000000]でもOKという結果になった。あとsumでもOK。けど、これ正格性解析のおかげなんかね〜。CLEANとか、さっぱりわかんねぇ。なんかIDEのModule->Module OptionsでStrictness Analyzerのチェックを外すと、foldlの場合だけ挙動が変わって、[1..1000000]とかでもHeap Fullというエラーが出るようになる。foldlの場合は正格性解析が効いてるってことかなぁ。sumの方がStrictness Analyzerのチェック外しても問題起きないのが腑に落ちない

とりあえず定義を見ると(libraries/StdEnv/StdList.icl)

// foldl::(.a -> .(.b -> .a)) .a ![.b] -> .a
foldl op r l
	:==	foldl r l
	where
		foldl r []		= r
		foldl r [a:x]	= foldl (op r a) x

// foldr :: (.a -> .(.b -> .b)) .b ![.a] -> .b	//	op e0 (op e1(...(op r e##)...)
foldr op r l :== foldr l
	where
		foldr []	= r
		foldr [a:x]	= op a (foldr x)

------------
sum:: !.[a] -> a |  + , zero  a
sum xs = accsum xs zero
where
	accsum [x:xs] n = accsum xs (n + x)
	accsum []     n = n

別に変なことはやってない。型になんか一杯くっついててよく分からんけど。んで、

module test

import StdEnv
mysum xs = acc xs zero
where
	acc [x:xs] n = acc xs (n + x)
	acc []     n = n
	
Start ::Int
Start = mysum [1..10000000]

みたいなコードを、strictness analyzerのチェックを外した場合と、外してない場合でそれぞれ走らせると、前者でちゃんとHeap Fullが起こる。なんかライブラリ関数の正格性解析は別枠になってんだろうか。

一方のGHCだと、foldr (+) 0とfoldl (+) 0は失敗するけど、sumを使えばOKっぽい(但し、デフォルトのGHCは超やる気ないので、最適化オプション付けないと、正格性解析はやってくれないので注意)

というとこで、そういやHugsはどうしてるんだろうとかいう宿題が発生。なおGHCではfoldr,foldl,sumの定義はこうなっていた(libraries/base/GHC/Base.lhs,libraries/base/GHC/List.lhs,libraries/base/Data/List.hs)

foldr k z xs = go xs
	     where
	       go []     = z
	       go (y:ys) = y `k` go ys
--------------
foldl        :: (a -> b -> a) -> a -> [b] -> a
foldl f z xs = lgo z xs
	     where
		lgo z []     =  z
		lgo z (x:xs) = lgo (f z x) xs
-----------
{-# SPECIALISE sum     :: [Int] -> Int #-}
{-# SPECIALISE sum     :: [Integer] -> Integer #-}
{-# SPECIALISE product :: [Int] -> Int #-}
{-# SPECIALISE product :: [Integer] -> Integer #-}
-- | The 'sum' function computes the sum of a finite list of numbers.
sum                     :: (Num a) => [a] -> a
-- | The 'product' function computes the product of a finite list of numbers.
product                 :: (Num a) => [a] -> a
#ifdef USE_REPORT_PRELUDE
sum                     =  foldl (+) 0  
product                 =  foldl (*) 1
#else
sum	l	= sum' l 0
  where
    sum' []     a = a
    sum' (x:xs) a = sum' xs (a+x)
product	l	= prod l 1
  where
    prod []     a = a
    prod (x:xs) a = prod xs (a*x)
#endif

ふむ。Cleanと全く同じ。sumに対しては、正格性解析が働いてるんだと思ってたら、-fno-strictnessオプション付けても、普通に動く。むう

けど、

_sum	l	= _sum' l 0
  where
    _sum' []     a = a
    _sum' (x:xs) a = _sum' xs (a+x)

main = print $ _sum [1..10000000]

を、-Oオプションのみでコンパイルした場合と、"-O -fno-strictness"オプションでコンパイルした場合だと、後者では、スタックオーバーフローかヒープ不足が起きる(どっちが先に起きるかは与えるリストの大きさとかに依存するっぽい)。

というわけで、この件については、abstract reductionの方がDemand Analysisより優秀なのか。なんか遅延評価ってどうもよくどうなってるのかわからんのー。どうでもいいけど、CLEANって多倍長整数ないんだなー

(追記)すまんありゃ嘘だった。Cleanがfoldlでうまくいく理由はhttp://d.hatena.ne.jp/m-a-o/#p3