モナド結合則で大事だけど書かれていないこと

なぜかこのことが書いてある本やブログが見当たらないので書いておく。

モナド結合則は、

m >>= (\x -> k x >>= h)   ==   (m >>= k) >>= h

というもの。有名です。==は、左辺の式と右辺の式は、まったく同じ計算結果を生じるということ。

まず、大事だけど明示されていない第一のことは、ここでのkとhはクライスリ射であるということです。まあ、記号としてfじゃなくてkを選んでいるのはそういう意図なのですが、明示的な説明は無いです。なので、kとhの双方または一方がクライスリ射ではないときは、この法則は成り立たなくてもよいというか適用外です。

実際、

m >>= (\x -> k x >>= (\y -> return (x*y)) 

のように、外側の束縛を自由項として含んでいる関数はクライスリ射ではない。これがコンパイル&実行が成功するときでも、これを結合則に従って変換した

(m >>= k) >>= (\y -> return (x*y))

は、もちろん「xがスコープ外」として常にコンパイルエラーとなります。よってモナド結合則は成立していない。まあ、先に書いたように、これはクライスリ射じゃないので法則の対象外ということです。閉包ですしね。

次に、大事だけど書かれていない第二のことは、実のところ、モナドのdo記法で使われている関数は、クライスリ射じゃないことがほとんどであって閉包もよく使われている、すなわち、「モナドを実践的に使っているときは、モナド結合則の範囲外の使い方をしている」ということです。

例えば、典型的な例である、

main = do
  a <- getLine
  b <- getLine
  putStrLn $ a ++ b

は、解糖すると、

main = getLine >>= (\a -> getLine >>= (\b -> putStrLn (a ++ b)))

となります。これはコンパイルも実行も成功します。ここで、閉包を使って外側の束縛aを最終出力に利用していることは、この処理の本質です。

さて、これをモナド結合則に従って機械的に変換すると、

main = (getLine >>= getLine) >>= (\b -> putStrLn (a ++ b)))

となり、なんのこっちゃ、です。kはgetLineであり、hは(\b -> putStrLn $ a ++ b) であって、外側の束縛aを含んでいるので閉包です。これはどちらもクライスリ射じゃないですし、kの型エラーとhのスコープ外エラーでコンパイルも通りません。

do記法を解糖した形がモナド結合則に似ているので、なんとなくそこでモナド結合則が機能しているのではと考えがちですが、do記法の糖化・解糖はモナド結合則とは独立して定義されていますし、似て非なるものということですね。