Pixel Pedals of Tomakomai

北海道苫小牧市出身の初老の日常

fmap head VS sequence

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`== ()

となり、計算はきちんと停止する。