[追記]以下の記述で、間違いと説明不足がありました。とりあえず、「(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つの型のあいだに同型があることを意味します。
- object {α: A, δ: (b=>B | c=>C)}
- (object {α: A, β: B} | object {α: A, γ: C})
- (@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 δ} }