型解析：細かい注意点
never型、undefined、型変数の値となる領域
never型はいかなるインスタンスも持たない。never?型の唯一のインスタンスはundefinedと書く。undefinedは意味領域に存在する値だが、表層には出てこない。コマンドの入力にundefinedが入ることはなく、コマンドの出力にundefinedが混じることもあり得ない。undefinedはデータとして受け渡されるものではなく、配列の項目（item）、オブジェクトのプロパティ、タグ付き値のvalの不在の目印となるだけである。存在しない項目／プロパティ／valにアクセスした場合、undefinedが取り出せるわけではなく、例外などのエラーとなる。
型変数は、undefinedを含まない領域を表す。つまり、変数xに対して never⊆x は常に成立する（公理だ）が、never?⊆x は成立しない。変数がそのままでオプショナル型になることはなく、'?'を付けてはじめてオプショナル型になる。よって、T? ⊆ x は、Tが何であっても成立しない。
シングルトン型とnull
単にシングルトン型といえば、シングルトンスカラー型を指す。複合データを1つだけ含むシングルトン型は、シングルトンスカラー型と型構成子から作れる。
シングルトン型はスカラーリテラルによって表現される。つまり、
となる。もともと、null値だけからなるシングルトン型がnull型だったので、nullはリテラルと型を同一視する方式に合致している。Catyでは、nullをシングルトンスカラー型として扱う。シングルトンではないスカラー型は、integer, number, string, booleanとなる。
暗黙タグを付与する方法
integer, number, string, boolean, null, array, object は型名として予約されている。arrayとobjectは次の定義を持つと考えてよい。
- type array = [any*];
- type array = {*:any?};
一方で、
- any = (number|string|boolean|null|array|object)
なので、arrayとobjectの定義は再帰的になる（これは余談）。
- type array = [(number|string|boolean|null|array|object)*];
- type array = {*:(number|string|boolean|null|array|object)?};
integer, number, string, boolean, null, array, object のインスタンには、型名と同じタグを付けてよい。@integer 3, @number 3.14, @string "hello", @array [1, 2, 3] など。しかし、これらのタグはすぐに消滅してしまい、そのまま維持されることはない。
タグが付いてない値やデータに、どうしてもタグが必要な場合は、予約型名と同じタグ（暗黙タグ）を付与することができる。暗黙タグを付与する作業が必要になるのは、排他的ユニオンの排他性の検査のときだけである。特に、シングルトン型（スカラーリテラル）には次のルールでタグを付ける。
- 数値リテラルには、@number を付ける。このとき、@integerは使わない。
- 文字列リテラルには、@string を付ける。
- true, false には、@boolean を付ける。
- null には、@null を付ける。
排他的ユニオンの排他性のチェック
(T1 | ... | Tn) の形をしたユニオンが排他的である条件は：
- すべての型のタグ（暗黙でもよい）が異なっていること。ただし、@integerと@numberは異なるとは認めない。
成分の型に明示的なタグが付いている必要はない。例えば、次の例は排他的となっている。
type coord = [number, number]
| {"x":number, "y":number}
| string(remark="座標のテキスト表現");
このcoord では (@array | @object | @string) という3つの暗黙タグが互いに異なる。
新スキーマ構文では、次も許される。
type gender = ("male" | "female");
この例では、(@string | @string) となり、同じタグが含まれる。同じタグを持つシングルトン型をユニオンとして許すため、次の規則を入れる。
- ユニオンの成分に同じタグがあってもよい。
- ただし、同じタグを持つ型はシングルトン型に限り、それらは互いに排他的（異なる値）でなくてはならない。
シングルトン型またはスカラー型は、次のどれかのタグを持つ； @integer, @number, @string, @boolean, @null。これらのタグを持つ型の排他性は容易に判定できる。例えば、(1|integer), (2|2), (integer|number), (true|boolean) などは排他的ではない例。従来の列挙型、例えば (0|1|2) は、新しい排他性の定義から排他的となる。シングルトン型とスカラー型のあいだに明白な区別はないので、次のようなユニオン型も認める； (integer|false), (0|1|2|null), (number|"+inf"|"-inf")。
型変数が含まれるユニオンは排他性が保証されないので認めない。例えば、(_X|string), (@foo _X | @foo _Y) などは認めない。しかし、(@foo _X | @bar _Y) は排他的だとすぐわかるのでOK。
ユニオンの排他性は、一般の古典論理（∨を含む）を使わず、連言論理だけで型解析を済ませるために必要な条件である。古典論理の計算負担は、∨の多段枝分かれにより、ときに手に負えなくなる。連言論理の範囲内に収めることは効率上重要である。
