型解析：雑多な予備知識
用語法の注意
型検査、型推論、型解析は同義語として使う、特に明確な区別はない。あるCatyスクリプト式（Caty式とも略称）に対する型解析が失敗するとは、否定的な結果を出して解析が成功することである。型解析は、成功する（肯定的な結果を出して終了する）か失敗する（否定的な結果を出して終了する）かのどちらかであり、型解析処理自体が例外を出したり無限走行することはない。（したら困る。）
型解析が“失敗した”場合は、当該のCaty式に、型の不整合があるので、この式は実行されない。型解析は、最初に発見した型不整合の場所と原因を報告することができる。
型解析が成功する場合は、完全に成功するときと条件付きで成功するときがある。条件付きで成功するとは、式内のパイプに実行時型チェック条件が付与されることである。
実行時型チェックを単にチェック、実行時型チェック条件を単に条件と呼ぶことがある。
ほとんどはスキーマ構文領域での話だから、型表現（型項）を単に型、型変数を単に変数とも呼ぶ。値変数はここでは出てこない。
タグ付き値、タグ付き型と言った場合は、暗黙タグのことは考えない。明示タグが付いた値、明示タグが付いた型のことである。暗黙タグに言及するときは、必ずその旨を記す。
記号法と若干の用語
次のようなメタ変数を使う。
- a, b など： スカラー定数（リテラル）
- x, y, u, v など：型変数
- α, β など：プロパティ名、タグ名
- E, F など：Catyスクリプト式
- A, B など：これもCatyスクリプト式
- S, T など：型（の表現、項）
- X, Y など：これも型
- f, g など：コマンド呼び出し
- n, m, i, j など：非負整数
- p, q など：JSONパス式
型Tに含まれる変数をVar(T)と書く。Var(S->T) = Var(S)∪Var(T) として、これをプロファイルS->Tの変数と呼ぶ。プロファイルの右辺Tの側にだけ出現する変数を制御不可変数、左辺Sにだけ出現する変数を制御可能変数、両側に出現する変数を伝搬変数と呼ぶ。read-some-file :: void -> _T の _T は制御不可変数である。length :: list<_T> -> integer(minimum=0) における _T は制御可能変数、 first :: list<_T> -> T throws IndexOutOfRange における _T は伝搬変数である。
左辺型と右辺型
型解析では、通常のスキーマ言語の型と少し違う型も使う。プロファイル S->T の左辺に使える型を左辺型、右辺に使える型を右辺型と呼ぶ。
左辺型は、スキーマ言語の型と同じである。左辺型で使える型演算：
- [, ] （配列構成、クリーニスター使用可能）
- {, } （オブジェクト構成、ワイルドカード使用可能）
- @
- ?
- | （制限有り、排他的）
- &
一方、右辺型で使える型演算は次のとおり。
- [, ]
- {, }
- @
- ?
- ∪ （制限なし）
制限付きの排他的ユニオン演算'|'の代わりに無制限のユニオン（集合の合併、ジョイン）演算∪が使える。インターセクション&は使えないが、これは消去不可能なインターセクション（次節）が使えないことを意味し、消去可能なインターセクションは自由に使ってよい。
消去不可能なインターセクション
インターセクション演算子&は分配法則を使って、式の内側へと移動することが出来る。この計算によって最終的に消えてしまうインターセクションは消去可能と呼ぶ。消去不可能なインターセクションとは、&の左右どちらか（両方かも）が変数であるものである。&は可換演算なので、左に変数があると仮定して一般性を失わない。つまり、x&T の形が消去不可能なインターセクションである。
次の制約を置く。
- プロファイルの右辺型には、消去不可能なインターセクションを書けない。
この制約は、コマンドプロファイルに対して検査される。コマンドプロファイルの右辺は、インターセクションを持たないか、消去可能なインターセクションだけを持つことになる。消去可能なインターセクションは前もって消去しておくとする。そして、右辺に出現する記号'|'をすべて∪に置き換えておく。
型の分類
型を次の12種に分類する。
- never型
- any型
- シングルトン型（数値リテラル、文字列リテラル、true, false, null）
- スカラー型（integer, number, string, boolean）
- 配列型
- オブジェクト型
- タグ（明示的タグ）付き型
- オプショナル型
- 排他的ユニオン型
- インターセクション型
- ジョイン型（無制限ユニオン型）
- 変数（不定型）
左辺型は、ジョイン型を除く11種、右辺型は、インターセクション型と排他的ユニオン型を除く10種である。変数はさらに、制御不可変数、制御可能変数、伝搬変数で扱いが少し異なる。
パイプ番号と条件
式Eが与えられたとき、そのなかに出現するパイプ記号に1以上の整数で番号を付けておく。この番号は一意識別できればなんでもよく、番号の大小は意味を持たない。特定の式のなかで、1番パイプ、2番パイプなどで特定パイプを指示できればそれでよい。
Eが与えられた式、Aがダミーの式として、便宜上 A | E という式を考えて、Eの左に出現するパイプ（Eのなかのパイプではない）を0番パイプと呼ぶ。0番パイプは「式の入り口」とまったく同じ意味である。
n番パイプに付与された実行時型チェック条件をn番条件と呼ぶ。特に0番条件は入り口条件である。型解析が完全に成功すると、実行時型チェック条件は不要になるが、0番条件だけは別で、多くの場合は0番条件を省略はできない。
