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

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

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

参照用 記事

Erlangのコーディングから、述語、ガード、レトラクト、そしてモナド

Erlangの話題は別なブログ「檜山正幸のErlang未確認情報」に分けました。久々に本編でErlangの話をしてみます。とはいっても、Erlang導入に使うだけで、言いたいことは「日常プログラミングでも、いたるところにモナドが顔を出すよ」ってこと。

ここでモナド自体の説明はしないので、モナドの事例をひとつくらいは事前に知っておいたほうがいいでしょう。僕が書いたモナド関係エントリーは「予告:セミナー「モナド」シリーズを開始します」に列挙されています。

内容:

  1. Erlangでも引数チェックが必要なとき
  2. ボトム付き集合
  3. 部分関数と例外
  4. 関数を部分集合へ制限すること
  5. 述語を使う方法
  6. ガードを使う方法
  7. レトラクトを使う方法
  8. どこがモナドなの?

Erlangでも引数チェックが必要なとき

Erlangにおけるエラーの考え方と取り扱い方は独特のものがあります(「Erlang実験室:武士道と云ふは死ぬ事と見付けたり」参照)。Erlangでは、原則的にエラー関連処理はしません。しかし、次の点は注意すべきです。

アームストロングも注意してますが、ユーザーインターフェースを経由してくるイベント(人間が起源)や、WebのPOSTデータなどを、検査なしで受け入れ、自分の都合に合わないと死んでしまうようなプログラムは、「潔く死ぬ」プログラムではありません。単にアホタレのダメプログラムです。

信頼できない起源を持つデータはキチンとチェックする必要があります。例えば、foo(Arg) の引数Argが信用できないなら、

  1. まずArgをチェックする。
  2. Argが正しいことが分かったときだけ次の処理に進む。

という手順になります。Argをチェックする関数の仕様としては、次のような案があるでしょう。

  1. Argが正しいかどうかの真偽値を返す。
  2. Argが正しいときは何も返さず(習慣により戻り値はok)、まずいときは例外を投げる。
  3. Argが正しいときはArgをそのまま返し、まずいときは例外を投げる。

それぞれの場合のコーディングは:


foo_1(Arg) ->
case check_arg_1(Arg) of
true -> do_foo(Arg);
false -> throw(error)
end.

foo_2(Arg) ->
check_arg_2(Arg), % 例外の可能性あり
do_foo(Arg).

foo_3(Arg) ->
do_foo(check_arg_3(Arg)). % 例外の可能性あり

コーディングとしての良し悪しを云々することはしないで(そっちに興味がある場合は「「Erlang実験室:ok/error方式はやっぱりダメなんだよ」を参照)、3つのケースの挙動を探ってみます。以下の説明では、Erlangの構文は使わず、普通の集合と関数(写像)の記法を使います。

ボトム付き集合

話を単純化するために、例外のときは、常にアトムerrorを投げることにします。関数fooの引数の集合をA、戻り値の集合をBとします。この事実は、foo:A→B と書けますが、次の2点に注意すべきです。

  1. 関数fooは、Aの全ての値に対して定義されているとは限らない。
  2. なにか問題があったときは、Bの値が得られるのではなくて、例外が投げられる。

errorを、正常値/通常値(normal values)とは区別される特殊な値と考えて、throw(error) の代わりに単に error (関数型でない多くの言語なら return error)を使いましょう。えっ? 紛らわしいし気持ち悪いって、んじゃ、アトムerrorじゃなくて記号⊥を使いますね。

⊥は「ボトム」と呼ばれ、「正常値/通常値とは区別される特殊な値」を表現します。⊥を含むような集合をここではボトム付き集合と呼んでおきます。正式な用語は平坦束です(今の文脈では束じゃないから適切じゃない)。

部分関数と例外

プログラムが定義する関数はたいていは部分関数(部分写像)です。foo:A→B と書いても、一部分は未定義かもしれません。このことを強調するために foo:A⊃→B という書き方もあります。「関数は部分関数」と了解した上で単に A→B と書いてもいいのですが、A⊃→B も併用することにします。それと、fooがホントに定義されているところを D(foo) と書くことにします。D(foo)は、Aの部分集合です。

部分関数 foo:A⊃→B を、ボトム付き集合 B = B∪{⊥} への関数だと思いましょう。つまり:

  1. a∈D(A) ならば、f(a) は B の値として確定する
  2. そうでない(戻り値が未定義)なら、f(a) = ⊥

こうするとfooは、

  • foo:A→B

と考えられます。バランスを取るために、Aもボトム付き集合 A = A∪{⊥} に置き換えて、

  • foo:A→B (foo(⊥) = ⊥)

としてもいいでしょう。

モナドをご存知の方なら、これはMaybeモナド(一番単純な例外モナド)になっていることが分かるでしょう。


補足:

プログラミングから離れて考えると、Maybeモナドは、集合Aに一点⊥を付け加える操作なので、付点モナドとでも呼ぶべきでしょう。一点を付け加える付点操作は、いくつかの解釈ができます。

  1. 集合圏から、付点集合(pointed set)と特定された点を保存する関数の圏への関手 Pointed:SetSet* ; 定義はほぼ自明
  2. 部分関数の圏から、付点集合の圏への関手 Bottomed:PSetSet* ; 未定義を、⊥とみなす。
  3. 集合圏から、集合圏への関手 AddPoint:SetSet ;最初の関手Pointedに忘却関手をつないだ関手

最後の解釈AddPointはSetの自己関手(endofunctor)となり、Set上の付点モナドを定義します。付点モナドは、随伴対 Pointed -| U : SetSet* から得られたものです(Uは忘却関手)。AddPointのクライスリ圏Kl(AddPoint; Set)が部分関数の圏PSetと同型(圏同値ではなくて同型)となります。このとき、SetPSetに埋め込む関手は、クライスリ圏Kl(AddPoint; Set)の標準的な埋め込みと同一視できます。

SetPSetに埋め込む関手をI、付点集合の特定された点(⊥です)を忘れる忘却関手をUとすると、I;Bottomed;U : SetSet が定義できます。定義を追いかければ、これは自己関手AddPointと同じです。

例外やエラーを特定された点⊥と解釈すれば、プログラムの意味論をSet*上で展開できそうですが、うまくいきません。短絡論理演算子とか、例外の捕捉、エラーからの回復なんかがうまく定式化できないのです。もっと精密な枠組み(領域理論とか)が必要になります。

関数を部分集合へ制限すること

関数fooの入り口で引数チェックをしてからホンチャン処理関数do_fooに渡す -- この手順を定式化しておきます。以下、fooとかdo_fooとか、その他の関数も、特に言及しなくても部分関数と考えます。別な言い方をすると、集合と部分関数の圏で考えます。

f:A→B、S⊆A のとき、関数(部分関数ですよ) f|S を次のように定義します。

  • a∈S のとき (f|S)(a) は f(a) と同じ。f(a) が未定義ならやっぱり未定義
  • a∈S でないときは、もとのfがどうなっていても、(f|S)(a) は未定義

f|S を「fをSに制限した関数」と呼びます。Sが空集合のときは、f|S はまったく未定義な関数になってしまいます。S = A のときは、f|S は f と同じです。

fがチャント定義されている部分を、D(f) と書くのでした。これを使うと:

  • D(f|S) = D(f)∩S

さて、引数チェックとは何であるかというと、次のように定式化できるでしょう。

  • f:A→B が処理関数、ただしA全体でfが定義されている保証はないし、D(f) 全体で望ましい挙動をするとも限らない。
  • Aの部分集合Sは、fにとって安全な値の集合と考えられる。
  • f|S を作ると、fにとって安全でない値に対しては未定義(現実にはエラーや例外)となる。
  • したがって、f' = f|S は、もとのfよりは安全で望ましい関数である。

この定式化を認めるなら、引数チェックするとき考えるべきことは、次の2点です。

  1. 安全な集合Sをはっきりと定義する方法
  2. f と S に対して f|S を構成する方法

述語を使う方法

では、具体例を見ていきましょう。


foo_1(Arg) ->
case check_arg_1(Arg) of
true -> do_foo(Arg);
false -> throw(error)
end.

Erlangでは見にくいですか?


function foo_1(arg) {
if (check_arg_1(arg)) {
return do_foo(arg);
} else {
throw "error";
}
}

関数 check_arg_1 の戻り値は、真偽値(boolean)だと想定されています。真偽値を返す関数は述語と呼ばれます。check_arg_1 が真(true)を返す値の集合がSになります。(以下の式でイコールは代入じゃなくて等号ね。)

  • S = {a∈A | check_arg_1(a) = true}

この方法は、述語を使って部分集合Sを確定して、条件分岐により制限を実現するものです。check_arg1 の値と do_foo の値の組み合わせにより foo_1 の値がどうなるかを表にすると:

true false
正常値b b 例外⊥
例外⊥ 例外⊥ 例外⊥

述語 check_arg1 も例外の危険性があるときは:

true false 例外⊥
正常値b b 例外⊥ 例外⊥
例外⊥ 例外⊥ 例外⊥ 例外⊥

ガードを使う方法

先の表を見てると、falseという値はあんまり意味がないのがわかります。いっそのこと、falseを返す代わりに例外を投げてしまってはどうでしょう。

true 例外⊥
正常値b b 例外⊥
例外⊥ 例外⊥ 例外⊥

chek_arg_1 は真か偽を返しましたが、check_arg_2 は真か例外で、check_arg_2(a) が真のときは a∈S だとします。正常値が1つだけなので、別にtrueじゃなくて整数1でも文字列"hello"でも何でもかまいません(Erlangの習慣ではアトムokを返します)。if文で分岐することも意味がないので、コードは次のようです。


function foo_2(arg) {
check_arg_2(arg); // 例外の可能性あり
return do_foo(arg);
}

ホンチャン処理関数 do_foo を check_arg_2 が守っている感じになります。そこで、check_arg_2 をガードと呼びます。いくつかの言語(Erlangも入ります)では、ガードが正式な構文となっています。通常ガードは述語(論理式)ですが、偽は自動的に例外に変換されます。アサーションと似ています。上のcheck_arg_2は、自前で作ったガード機構というわけです。

レトラクトを使う方法

次の方法は一番スマートかも知れません。なにしろ短い。


function foo_3(arg) {
return do_foo(check_arg_3(arg)); // 例外の可能性あり
}

do_fooが A→B だとすると、check_arg_3は、A→A という関数(部分関数を⊥を使って定式化した関数)だと思えます。check_arg_3が定義するところのAの部分集合をSとすると:

  • a∈S のときは、check_arg_3(a) = a
  • a∈S でないときは、check_arg_3(a) = ⊥ (例外を投げる)

check_arg_3は、文字通り引数値をフィルター(濾過)してます。具合が悪そうな値は⊥に直して排除しています。

check_arg_3の値はSの要素か⊥(例外)のどちらかです。よって、check_arg_3:A→S と考えてもかまいません。記号を簡略化するために、A→S と考えたcheck_arg_3 を r:A→S, オリジナルのcheck_arg_3を r':A→A 、そして S をそのまま A に埋め込む関数を i:S→A とすると、次の等式が成り立ちます。

  1. i;r = id (レトラクト性)
  2. r;i = r'
  3. r';r' = r'(ベキ等性)

これは、「レトラクションの起源(かな?)」で述べた状況と同じです。そうです、レトラクト(レトラクション)なのです(他にも、「レトラク」の日記内検索)。つまり、引数値をフィルターして不適切なときは例外を投げる方法は、集合Aの部分集合Sに対してレトラクトを作っているのです。

どこがモナドなの?

こうして見ると、述語、ガード、レトラクトは、やってることがほとんど同じであることが分かります。[追記]相互変換[/追記]実際、集合と部分関数の圏のなかで、述語p:A→Ω (Ωは真偽値の集合)、ガードg:A→11は単元集合)、レトラクト(ベキ等写像のほう)r:A→A の関係をキッチリと述べることができます。

そして、⊥(例外、エラー)を考えることがモナドになっていることも分かります。えっ? あんまりモナドが出てこなかったって。いやっ、背後にずっとモナドがいたんですよ。正常な関数計算が進行する舞台は、集合圏に、集合の直積と直和を考えた分配圏*1です。例外/エラー(⊥で表した)を取り扱うために付点モナド(当エントリーの補足のところを参照)を導入して、例外/エラーを含む計算は付点モナドのクライスリ圏のなかで処理しています。

わざわざそんなこと大げさなこと言わなくてもいいんじゃないの? 言わなくてもいいのですけど、実際にそこにモナドがいるのは事実だから否定のしようはないでしょ。見たくなければ別に見なくてもいいけれど、ともかく、います、そこに、モナドが。

*1:実際には、半環圏(semiringal category)になっています。