sequenceを使えば、複数個あるモナド値を1つのモナド値に集められる。
xs :: (Functor m, Monad m) => m [()] xs = sequence [return x' | x' <- [(),()..]]
xsはモナドに包まったリストなので、fmapを使ってheadを持ち上げれば先頭要素がとれる。
x :: (Functor m, Monad m) => m () x = fmap head xs
これをIdentityモナドとして動かしてみる。
> runIdentity x ()
よし! Writerモナドとして動かしてみる。
> runWriter (x :: Writer () ()) ((),())
よし! ただ、()はMonoidとはいえ何も情報を持てなくてあんまりなので、[()]くらいにしてみる。
> runWriter (x :: Writer [()] ()) ((), C-c C-cInterrupted.
WTF!! なんてこった! どうしてこうなったのか。
検証
直感的には、xsはm [()]という型を持っているが、リストなのは値であって副作用の側には言及してない。headがかかるのも値だけであり、副作用については無限リストすべてから集めてみないとわからず、そのため停止しないってことじゃないかと予想できる。
確かめてみよう。扱うのがモナドであっても、圏論なんて全く関係なくて必要なのは単なるλ計算だ。実際の実装とだいぶ違うが、わかりやすさのために以下の項を定義として調べてみる。headやfst、sndなんかはよく知ってる定義通りとしておく。
return = λv -> (v, []) (>>=) = λ(v,n) f -> (fst (f v),n ++ snd (f v)) sequence = λ((v,n):xs) -> (v,n) >>= (λv -> ((v:fst (sequence xs)),snd (sequence xs))) fmap = λf (v,n) -> (f v,n)
問題の項xに該当するのは以下。
fmap head (sequence [((),[]), ((),[])..])
簡約してみる。
fmap head (sequence [((),[]), ((),[])..]) ↓ (λ(v,n) -> (head v,n)) (sequence [((),[]), ((),[])..]) ↓ F1 = (λ(v,n) -> (head v,n)) と置く F1 (((),[]) >>= (λv -> ((v:fst (sequence [((),[])..])),snd (sequence [((),[])..])))) ↓ F2 = λv -> ((v:fst (sequence [((),[])..])),snd (sequence [((),[])..])) と置く F1 ((λf -> (fst (f ()),[] ++ snd (f ()))) F2) ↓ F1 (fst (F2 ()),[] ++ snd (F2 ())) ↓ F1を展開 (head (fst (F2 ())),[] ++ snd (F2 ()))
これでタプルの状態、すなわちWriterモナドの値にまで簡約できた。先ほど残念な結果となった出力をよく見てみるとわかるが、タプルの1要素目、つまり値の側は実はきちんと計算が終わっている。まずはこちらを簡約してみる。
head (fst (F2 ())) ↓ F2を展開 head (fst ((():fst (sequence [((),[])..])),..略..)) ↓ head (():fst (sequence [((),[])..])) ↓ ()
fmap headが効いてくれてうまく簡約できた。じゃあ、2つ目の要素、つまり副作用を表す側はどうかと言えば・・・。
[] ++ snd (F2 ()) ↓ snd (F2 ()) ↓ F2を展開 snd (..略..,snd (sequence [((),[])..])) ↓ snd (sequence [((),[])..]) ↓ snd (((),[]) >>= F2) ↓ snd (fst (F2 ()), [] ++ snd (F2 ())) ↓ [] ++ snd (F2 ())
戻ってしまった。ということで、第2要素は⊥であることがわかった。
ところで、そうなるともう1つ疑問なのが、なぜ Writer () () に関しては⊥とならず値を求めることができたのか、ということだ。これは()に対する`mappend`の定義を見るとわかる。
_ `mappend` _ = ()
そう、mappendは非正格な関数なのである。よって、
() `mappend` snd (F2 ()) == () `mappend` ⊥ == ()
となり、計算はきちんと停止する。