A?? → A? (A?|B) → (A|B)? など A? & B → A & B など A? & B? → (A & B)? bag [A?] → bag [A] (ハテナ定理には不要) @name A? → @name A (ハテナ定理には不要) ハテナ定理に必要なのは、演算子?, |, & に関する正規化だけ。

制限の追加ではなくて、領域（型の意味）の構成となっている演算は7種。 配列構成 オブジェクト構成 バッグ構成 （追加） ?演算 オプショナル構成 |演算 ユニオン構成 @演算 タギング構成 （追加） &演算 インターセクション構成 （追加） 配列、オブジェク…

たいした内容ではないけど、名前を付けておこう。 タグ排他性の原理：α≠β ⇒ (@α A)∩(@β B) = 0 単調性の原理：S ⊆T ⇒ tags(S)⊆tags(T) ハテナ定理：正規形の式なら、一番外側の'?'で確定型か不確定型か判断できる。 ν（nu）定理：ν(T) ≧ 1、ν(T) = n なら、T…

タグの基本はラベル（マーカー）。型情報としての利用は付随的／二次的であり、ラベルをインスタンス型情報として流用しているに過ぎない。利用可能な範囲も限定的である。バリデータをvalidateとすると： 基本は、validate(x, T) Tは型表現 validate(x) → v…

module public provides [person]; // personは公開型名となるtype person = @person object { "name" : string, "age" : integer(minimum=0), * : any } & // インターセクション演算子 personExt // 拡張ポイント ;// 拡張ポイントの実体を外部参照にする …