型演算子のまとめ

「各レベルの構成子、演算記号」にだいたいまとめたが、別な観点からまとめておく。

型の全体を代数系と考える。これは2ソート代数で、「ラベル型」ソートと「データ型」ソートを持つが、単に「ラベル」と「データ」と言ってしまうこともある。Lをラベル型の全体、Dをデータ型の全体として、色々な演算を持つ。説明欄に×が付いているのは実装がないもの。

演算の説明	演算のプロファイル	演算記号	Catyスキーマ
ラベルの連接×	L×L → L	・	>>
ラベル連接の単位×	1 → L	ε	[]
ラベルのミート×	L×L → L	∧	&
ラベルミートの単位×	1 → L	L	* (string)
タギング	L×D → D	・	@, >@
タギングの右単位×	1 → L	ε	[]
タギングの左擬単位	1 → D	υ	undefined
タグのデータへの埋め込み	L → D	-・υ	単項の @
直積	D×D → D	×	[-, -], >>
公平有限直積	D2+ → D	複数の×	[-, ..., -], 複数の>>
直積の単位	1 → D	1×	null
無限直積×	D*∞ → D	Π	なし
有限台無限直積	D*∞ → D	Π ×	[-, ..., -*]
ラベル付き直積	D×D → D	(×)	++
ラベル付き公平有限直積	D2+ → D	複数の(×)	複数の++
ラベル付き直積の単位	1 → D	1(×)	{}
無限ラベル付き直積×	D*∞ → D	Π	なし
有限台無限ラベル付き直積	D*∞ → D	Π ×	{-:-, ..., *:-}
直和×	D×D ⊃→ D	+	なし
公平有限直和×	D2+ ⊃→ D	複数の+	なし
直和の単位	1 → D	0	never
無限直和×	D*∞ ⊃→ D	Σ	なし
有限台無限直和×	D*∞ ⊃→ D	Σ +	なし
ラベル付き直和	D×D ⊃→ D	(+)	|
ラベル付き公平有限直和	D2+ ⊃→ D	複数の(+)	複数の|
ラベル付き直和の単位	1 → D	0	never
無限ラベル付き直和×	D*∞ ⊃→ D	Π	なし
有限台無限ラベル付き直和	D*∞ ⊃→ D	Π +	(@- -| ..., |@* -)
ミート（集合の共通部分）	D×D → D	∧	&
ミートの単位	1 → D	U	any?
ジョイン（集合の合併）×	D×D → D	∨	||
ジョインの単位	1 → D	0	never
クリーネスター	D → D	-*	[-*]
0のクリーネスター	1 → D	0* = 1	[]

単位だけ取り出してみる。

ラベル連接の単位×	1 → L	ε	[]
ラベルミートの単位×	1 → L	L	* (string)
タギングの右単位×	1 → L	ε	[]
タギングの左擬単位	1 → D	υ	undefined
直積の単位	1 → D	1×	null
ラベル付き直積の単位	1 → D	1(×)	{}
ラベル付き直和の単位	1 → D	0	never
ミートの単位	1 → D	U	any?
ジョインの単位	1 → D	0	never
0のクリーネスター	1 → D	0* = 1	[]

随分とたくさんの演算があるもんんだ。

以上に出てこないが他にも重要な演算がある。

Catyの型演算子	説明
?	オプショナル
!	必須（required）
(, )	スキーマ属性付与
{, }	バッグ型の出現回数

オプショナル'?'は、代数的には x? = x∨υ と書ける。同様に、x! = x - υ （- は集合差として）

他に、Catyスキーマで出てくる記号は：

• >:, >@ 図式順の演算、ただし、>@ は中置二項演算子。
• クリーネスターの'*', プロパティ名ワイルドカードの'*'
• タグ名ワイルドカードの'*' , '*!'
• 疑似タグの '@?'
• 型名タグの '@&'

演算子の構文上の形式から整理すると以下。

Catyの型演算子	説明	形式	備考
>>	連接	中置二項演算子	実装はない
||	合併	中置二項演算子	実装はない
&	ミート	中置二項演算子
++	マージ	中置二項演算子
|	ユニオン（排他的）	中置二項演算子
[ ]	配列	特殊形式多項演算子
[ ,-*]	可変配列	特殊形式多項演算子
{ }	オブジェクト	特殊形式多項演算子
{ ,*:-}	可変オブジェクト	特殊形式多項演算子
do { }	DOオブジェクト	特殊形式多項演算子
do {,:>*}	DO可変オブジェクト	特殊形式多項演算子
@	タグング	前置二項演算子
>@	タグング	中置二項演算子	タグが右
?	オプショナル	後置単項演算子
!	必須（required）	後置単項演算子	未実装
(, )	スキーマ属性付与	後置単項演算子