「再びモナドへ」と言って、実際、多少はモナドについて調べているわけです。プログラミング言語の機能としてのモナドというよりは、モナド概念を利用して処理系を構成するほうの話がメインテーマです。
例えば、少し古いですが、
- Sheng Liang, Paul Hudak, Mark Jones "Monad Transformers and Modular Interpreters." http://haskell.cs.yale.edu/wp-content/uploads/2011/02/POPL96-Modular-interpreters.pdf
とか（って、まだ1行も読んでない）。
今は、昨日引用した次の論文を拾い読み。
- Ralf Hinze, "Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick." http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf
このラルフ・ハインズ（発音はヒンズかもしれない [追記]ヒンズに近いですね。[/追記]）の論文は、CPS（continuation passing style）変換によるプログラム最適化の背後にある現象をカン拡張で説明しようとするものです。このなかで、余密度モナド（codensity monad）ってのが出てくるのですが、これがなんだか面白い。
一般に、モナドは随伴対 F -| G （F:C→D, G:D→C）から作られます。ところが、関手 G:D→C だけからC上のモナドを構成できるというのです。それがGの余密度モナドです。このとき、関手Gに左随伴Fの存在を要求しません。
この話は僕にとっては意外なことです。モナドと随伴対は事実上同じものだと思い込んでいたので、「左随伴なしでもモナドが作れる」という言明が正確には理解できてません。もちろん、Gがまったくの無条件というわけではなくて、G:D→C が、自分自身に沿ったカン拡張 K:C→C を持つとき、Kを台関手とするC上のモナドを構成できます。
なーんか腑に落ちないので、ともかく計算して確認してみよう、と。でも、等式的計算は出来そうにないので絵算でチャレンジ中のスナップショットが「なんかのお絵描き」です。
それにしても、モナドって、随伴の左と右が協力して生み出すもんじゃなかったの？ 相方（左随伴）がいなくても、モナドが出来ちゃう？ ウーン。相方の女性がいなくても、男一人で子供が出来ちゃう、みたいな不思議な感じだ。
