Catyはなんか潜伏状態です。活発に潜伏(?)しています。MITランセンスの公開部分を整備したり、解説文書を揃えたりする時間と余裕がなかなか取れないのですが、現実的なシステムのベースにCatyを使っています。
Catyの技術的な特徴は、型システム、スクリプト・インタプリタ、モナド方式のIOサブシステムとかでしょう。今日は最近のCaty型システムの状況と問題点を書こうと思います（って、思っただけで出来てないです。後述）。昨日、「Catyでは部分的にミート付きクリーネ代数を実装しているのですが、なかなか使い勝手はいいです。少し詳しく紹介したいな、とは思ってます」なんて書いてますし。それと偶然なんですが、今朝、型システム仕様の見落としを発見したりして。この機会に少し形式的にまとめておかないといかんなー、っと。
そう思って書き始めたら長くなって終わりそうもないので、とりあえず次の集合達を定義することにします、今回は。
- J -- 単純化したJSONデータの全体
- S -- J* ： 単純化したJSONデータのシーケンスの全体
- K -- Pow(S) = Pow(J*) ： シーケンス領域の部分集合の全体
- T -- Pow(J) ： 単純化したJSONデータ領域の部分集合の全体
内容：
単純化したJSONデータの領域
Catyが使っているデータは、JSONを少しだけ拡張したXJSONです。XJSONデータは、特定のルールに従って普通のJSONとして書き出せます。コメントが削除される以外は可逆的な相互変換「XJSON←→JSON」が可能です。
JSONにはオブジェクト型がありますが、話を簡単にするために、ここではスカラー型と配列型（リスト型）だけを考えることにします。スカラー型も string と null だけにしておきます。それでも本質は変わりません。それと、配列型とは別にシーケンス型を導入します。配列型とシーケンス型の違いは微妙なのですが、外側のブラケット（'['と']'）を付ける前の単なる並びがシーケンスだと思ってください。長さが1以外のシーケンスはJSONデータではありません。
ここから先は、順番にキチンと（でもないか）データ領域を定義していきます。
すぐ上で述べたように単純化したJSONデータ全体の集合を、Jとします。混乱を避けるために、string型、null型のデータ全体の集合をそれぞれ、String, Null と大文字始まりにします。
- Null = {null}
- Scalar = String ∪ Null
JSONでは、string型にnullが含まれないので、String ∩ Null は空です。よって、J = String + Null と直和の形に書くことが許されます。集合Jは、BNF風の再帰的定義により次のように定義されます。
- J ::= Scalar | Array
- Array ::= [J*]
ここで、[J*] は、Jの要素を有限個（0個でもいい）を並べて外側をブラケットで囲ったデータを意味します。外側をブラケットで囲んで一纏まりにしていることがポイントです。
シーケンス・データの領域
単純化したJSONデータの領域Jだけでは不足です。Jの要素からなるシーケンスデータの全体をSとしましょう。コンピュータが実際に扱うのはJなんですが、概念上はSも絶対に必要です。SはJにJはSに最初から埋め込まれているし、JをSにSをJに（写像で）埋め込むこともできます。
Sの定義は次のようになります。
- S ::= J*
Array ::= [J*] と似てるんですが、外側をブラケットで囲んでないのです。JとSの定義を一緒にすると：
- J ::= Scalar | Array
- Array ::= [J*]
- S ::= J*
あるいはもっと簡略化して：
- J ::= Scalar | [S]
- S ::= J*
長さがnであるシーケンス全体は Sn を書きましょう。すると：
- S = S0 ∪ S1 ∪ S2 ∪ ...
nとmが異なる整数なら Sn∩Sm は空なので、S = S0 + S1 + S2 + ... と書いてもいいでしょう。各n（n = 0, 1, 2, ...）は次のようにも書けます。
- S0 = {ε}
- S1 = J
- S2 = J・J
- S3 = J・J・J
- ...
ここで、εは空列ですが、ほんとに何も無い空虚な記号で、外側を囲むブラケットさえありません。「・」は連接を表します； 連接はカンマを区切りとしてデータ達を並べる行為だと思えばいいでしょう。
JとSの関係をハッキリさせるために、ブラケティング brk:S→Array とアンブラケティング unbrk:Array→S を導入します。ブラケティングは、シーケンスの外側にブラケットを付けて配列とみなす操作、アンブラケティングはその逆で、配列の内容であるシーケンスを取り出す操作です。
J⊆S なので、JはSの一部分です。しかし、ブラケティングは単射なので、brk:S→Array, Array⊆J によりSはJに埋め込まれます。外側の広い世界が、自分自身の内部にソックリ閉じ込められるという、再帰的データ領域ではよくある現象です。
ミート付きクリーネ代数
先を急ぎましょう。集合Kを、K = Pow(S) = Pow(J*) とします。この定義から、Kは、Jをアルファベットとする言語の集合となります。「言語」に深い意味はまったなくて、シーケンスの集合を言語と呼ぶだけです。「正規表現の意味論とその拡張」で触れたように、Pow(J*)はクリーネ代数となります。
もちろん、K上に演算と定数を定義しないとクリーネ代数とは言えません。Kの演算と定数を書き下します。
- 加法「+」-- 集合の合併
- 乗法「・」 -- 連接。Sの連接を集合に対して拡張した演算
- クリーネ・スター「*」 -- 任意回の連接をすべて寄せ集める演算
- 定数「0」 -- 空集合
- 定数「1」-- 単元集合 {ε}
さらに、ミート演算∧とミートの単位元∞*1を、集合の共通部分をとる演算と全体集合Sとして入れます。K = (K, +, ・, *, ∧, 0, 1, ∞) が型の計算を行う舞台となります。
Kは、整合的な計算を行うには向いてますが、コンピュータが扱う型はKより狭くなります。T = Pow(J) と置きましょう。つまり、Tは、（単純化した）JSONデータ領域の部分集合の集合です。Tの要素（Jの部分集合）を型とみなします。J⊆S なので、Pow(J)⊆Pow(S) となり、TはK（=Pow(S)）の部分集合となります。別な言い方をすると、型の集合Tは、より広いミート付きクリーネ代数Kの一部です。
TはKの部分ですが、部分クリーネ代数にはなりません。例えば、1（={ε}）はTに含まれないし、t∈T でも、t* がTに含まれることは保証できません。ところが、T上に別な演算と定数を定義すると、Tをミート付きクリーネ代数にすることができます。つまり、TはKの部分としての姿と、それ自身で自立した姿の2つを持つのです。
型の集合Tが二面性を持つところが混乱しがちで難しいところでもあり、また面白いところでもあります。続きはまた。（「続き」のバックログがまた溜まった。）
