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

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

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

参照用 記事

分配法則を与える同型

「Catyとデカルト分配圏」より:

[追記]以下の記述で、間違いと説明不足がありました。とりあえず、「(b=> object {α: A, β: B} | c=> object {α: A, γ: C})」と書いてあったところを「(object {α: A, β: B} | object {α: A, γ: C})」に直しました。これで理屈の上のツジツマはあいます。が、実際には「(@b object {α: A, β: B} | @c object {α: A, γ: C})」じゃないと、実装上は不都合があります。そのへんの説明は長くなるので別な機会にします。[/追記]

こんな話に興味がある人はあんまりいない(つうか、説明がされてないから興味の持ちようがない)と思いますが。自分用メモとして。

分配法則をJSONの世界で考える

圏の分配法則の成立は、次の同型の存在で保証されます。

  • A×(B + C) → A×B + A×C (右からの分配法則もあります)

A, B, C は型だとして、デカルト積(直積)「×」はJSONのオブジェクト構成により、デカルト和(直和、余積)「+」は接頭辞(タグ)による場合分けで与えられるとします。そうすると、分配法則のJSON版は、次の3つの型のあいだに同型があることを意味します。

  1. object {α: A, δ: (b=>B | c=>C)}
  2. (object {α: A, β: B} | object {α: A, γ: C})
  3. (@b object {α: A, β: B} | @c object {α: A, γ: C})

1番目の型(JSONデータ領域)を2番目の型に移すスクリプトは次で与えられます。


[
{getv α >: α},
getv δ | {b=> {cat >:β}, c=> {cat >:γ}}
] | merge

ここで、catはUNIXのcatコマンドにちなんだ命名ですが、普通に考えると、何もしないコマンドにcatって名前もひどいもんだ、と思うので、pass にします。圏論風のidでもいいけど、「ユーザーID」とかと勘違いされそうだし。

pass を使って書き換えると:


[
{getv α >: α},
getv δ | {b=> {pass >:β}, c=> {pass >:γ}}
] | merge

Catyスクリプト構文や基本コマンド名は、これからもフラフラ変わるかもしれません(Kuwataさん、ごめんね)。

さて、(object {α: A, β: B} | object {α: A, γ: C}) という型は、「|」を直和と解釈すれば、集合論圏論の観点からは特に問題ありませんが、プログラムによる処理では扱いにくいので、直和成分(direct summand)を区別するタグを付けて、(@b object {α: A, β: B} | @c object {α: A, γ: C}) としたいのです。

出力の一番外側にタグを付けるので、puttコマンドを最後に呼ぶことになります。putt b または putt c です。どっちを呼ぶかの情報を伝達する必要があります。いくつかの伝達方法が考えられるので、それについて述べます。

変数を使う

「set 名前 値」というコマンドで変数に値をセットできるとします。なにも珍しいことはないですよね。でも、setコマンドは、passコマンド(旧catコマンド)と同じように、入力をそのまま出力に流すとします。副作用として、変数のセットをするわけですね。セットした変数値は $名前 で参照できるとしましょう。

以上の仮定のもとで:


[
{getv α >: α},
getv δ | {b=> {set tag b >:β}, c=> {set tag c >:γ}}
] | merge | putt $tag

こうすると、次のどちらかのデータが出力されることになります。

  • @b object {α: A, β: B}
  • @c object {α: A, γ: C}

タグを直接操作する

タグが、実際は "$tag" という名前のプロパティにより実現されているという内部事情を使えば、次のようにも書けます。


[
{getv α >: α},
{getv δ | {b=> {pass >:β}, c=> {pass >:γ}},
{getv δ | getv "$tag" >:"$tag"}
] | merge

見た目が醜いので、一見スジが悪そうですが、お化粧すれば悪い方法ではありません。型推論の観点からは、一番扱いやすい気がします。

単純JSONパス式を使って分岐する

もともと、タグによる分岐の構文は dispatch {tag1=> pipeline1, tag2=> pipeline2} のように、予約語dispatchを伴っていました。このdispatchを復活させましょう。ただし、dispatch (単純JSONパス式) という形で、単純パス式が指すデータのタグを見て分岐するとします。

すると、次のように書けます。


dispatch (δ) {
b=> {getv α >:α, getv δ >:β} | putt b,
c=> {getv α >:α, getv δ >:γ} | putt c
}

この方式のいいところは、(書き方によっては)出力されるJSONオブジェクトに近い形式で書けることです。


dispatch (δ) {
b=> @b {α: getv α, β: getv δ},
c=> @c {α: getv α, γ: getv δ}
}