このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

単一代入のモノイド、スタンピングモナド、モナド工場

昨日モニャドセミナー3を開催しました。僕(檜山)がどうも熱暴走していた(熱で暴走したんじゃなくて、暴走して熱を出したのかも)きらいがありました。とりあえず、説明があやふやだったところを補足します。

次の話をしました; 「破壊的代入と単一代入を自明モノイドで定式化できる。ただし、単一代入のモデル化は実際にやってみると微妙にうまくいかない」と。で、「どこがうまくいかないのか?」とのご質問。「昔やってみたとき、うまくいかなかった記憶がある」と要領を得ない返答をしたのですが、何がうまくいかなかったかサッパリ思い出せません

という事情なので、最初から全部計算し直してみることにしました。僕は1桁の足し算とかしょっちゅう間違うので、そのテのミスで「うまくいかない」と思い込んでいた可能性もあります。以下に、確認の過程を全部書き下すので、ご興味がある方は(いるのか?)チェックしてみてください。なにか間違いがあれば教えてくださいませ。

単一代入の定式化:実例と計算

単一代入規則に従う変数をひとつ考えて、その値は 1, 2, 3 のいずれかだとします。値が束縛されてないときは、便宜上、値は「?」(この疑問符はundefinedを意味する)だと解釈することにします。^1, ^2, ^3は変数に値1, 2, 3を束縛しようとする作用、^?は、変数を未束縛に戻そうとする作用だとします。

Erlangだと、変数への値の束縛(パターンマッチとその副作用)を X = 1 のように書くので、束縛を行う作用(オペレータ)は =1 とか書くと感じがでるのですが、こんなところにイコールを使うと混乱のもとなので、^1 と記しました。

今考えている変数は単一代入変数なので、変数に一度値が束縛されると、違う値に再束縛はできないし、未束縛に戻すこともできません*1。結果的に、束縛済み変数の束縛状態はなにがあっても変化しません。今束縛されているのと同じ値への再束縛(というよりむしろパターンマッチ)は成功しますが、状態の変更はやっぱり起こりません。

^?(未束縛にする作用)が成功するのは、変数が未束縛のときだけです。なぜなら、未束縛から未束縛への変更(実際は変更されない)は許されますが、いったん具体値に束縛された変数は元の未束縛状態には戻せないと考えているからです。以下に、変数の最初の状態(before)に対し束縛作用が働くと、結果(after)がどうなるかを完全に書き下してみます。

最初の状態 束縛作用 結果の状態
? ^1 1
? ^2 2
? ^3 3
? ^? ?
1 ^1 1
1 ^2 1
1 ^3 1
1 ^? 1
2 ^1 2
2 ^2 2
2 ^3 2
2 ^? 2
3 ^1 3
3 ^2 3
3 ^3 3
3 ^? 3

同じことですが並び順を変えた表。

最初の状態 束縛作用 結果の状態
1 ^1 1
2 ^1 2
3 ^1 3
? ^1 1
1 ^2 1
2 ^2 2
3 ^2 3
? ^2 2
1 ^3 1
2 ^3 2
3 ^3 3
? ^3 3
1 ^? 1
2 ^? 2
3 ^? 3
? ^? ?

この表をもとに、作用 ^1, ^2, ^3, ^? を写像で表現してみます。ここでいう写像は、集合 {1, 2, 3, ?} から集合 {1, 2, 3, ?} への写像であり、変数の状態遷移(値の変更)を表します。

  1. ^1 の表現:{1→1, 2→2, 3→3, ?→1}
  2. ^2 の表現:{1→1, 2→2, 3→3, ?→2}
  3. ^3 の表現:{1→1, 2→2, 3→3, ?→3}
  4. ^? の表現:{1→1, 2→2, 3→3, ?→?} (恒等写像

上の写像表現を使って、^1, ^2, ^3, ^? を連続して作用させたときの結果を追いかけて、表にまとめます。横軸が最初に、縦軸が2番目に作用するオペレータです。

^1 ^2 ^3 ^?
^1 ^1 ^2 ^3 ^1
^2 ^1 ^2 ^3 ^2
^3 ^1 ^2 ^3 ^3
^? ^1 ^2 ^3 ^?

それとは別に、天下りに次の約束をして、二項演算▼を導入します。

  1. xが何でも、 ^?▼x = x▼^? = x
  2. xが^?でないなら、 x▼y = x

二項演算▼の演算表作ってみます。これは簡単に作れます。横軸が左の項に、縦軸が右の項です。

^1 ^2 ^3 ^?
^1 ^1 ^2 ^3 ^1
^2 ^1 ^2 ^3 ^2
^3 ^1 ^2 ^3 ^3
^? ^1 ^2 ^3 ^?

これらを眺めてみると … … …
… … …
うまくいっているなー。 束縛作用の実際の振る舞いと、天下りの二項演算▼は一致してますね。作用の逐次合成、または二項演算▼により、束縛作用の全体 {^1, ^2, ^3, ^?} がモノイドになるのはすぐ分かるので、バッチリだよなー。やっぱり僕が勘違いして「うまくいかない」と思い込んでいたようです。どこでミスしたかな?*2 思い出せませーん。別に思い出せなくてもいいや。

左自明モノイドと右自明モノイド

上記の例では、束縛オペレータに対して二項演算▼を定義しましたが、一般に集合Mと、Mの特殊な要素uがあると、次のようにして左自明演算が定義できます。

  1. xが何でも、 u▼x = x▼u = x
  2. xがuでないなら、 x▼y = x

同様に、右自明演算▲は次のように定義します。

  1. xが何でも、 u▲x = x▲u = x
  2. yがuでないなら、 x▲y = y

(M, ▼, u) も (M, ▲, u) もモノイドになります。それぞれ、左自明モノイド、右自明モノイドと呼びます。自明(トリビアル)と言っているのは、演算があまりにもバカバカしいからです。単位uとの演算が例外的ですが、それを除けば「答は常に左」、「答は常に右」という計算ルールです。

こんなにバカバカしく異常に単純な自明モノイドですが、左自明モノイドが単一代入のモデル、右自明モノイドが破壊的代入のモデルになっています。もちろん、左と右の違いは約束で決まるもので、作用の時間順を「左から右へ」と決めたときの話をしています。

スタンピングモナドモナド工場

モノイドMがあると、X |→ X×M という直積による掛け算関手をモナドにできます。「できます」とは、モナド乗法とモナド単位が定義できることですが、それぞれモノイドMの乗法(二項演算)、モノイドMの単位から構成します。

与えられたモノイドMから、この方法でモナドを作ることをスタンピングと呼んだりします。「スタンピングモナド」はそれほど一般的な用語ではありませんが、僕はよく使っている言葉です*3。いろんな集合Xに対して、モナドMが刻印された判子をペタペタ押していくような感じだから「スタンピング」なんだろう、と勝手に想像しています*4

スタンピングを使うと、モノイド1個に対して、モナドを1個確実に作れます。モノイドと同じ数だけモナドを作れるわけです。単一代入モナドや破壊的代入モナドはこうして作られます。モノイドの実例は他にも大量にあるので、スタンピングは、モナドの大量生産を可能にします。つまり、スタンピングの技法をマスターすれば、モナド工場を手に入れたことになります。

さー、君もスタンピングでモナドをガシガシ作っちゃおう*5

*1:ちなみにErlangでは、対話的シェルコマンド f (forget)で束縛を解除できます。

*2:今回なんかミスしている可能性もありえますけど。

*3:Googleで見たら、僕しか使ってないよ。僕の造語じゃないのだけど、まーいいや。

*4:ほんとの語源がどうであるかは、今さらもうどうでもいいです。

*5:直和スタンピングってのもありまっせ。