型解析：動的なPCL (Path Check Logic)
型演算'<<'を扱うためには、推論も拡張しなくてはならないが、実行時の検査条件を記述するPCL(path check logic)の変更のほうがむしろ大きい。
今までのPCLは、pをパス、'_'を無名変数だとして、次の3つの形の式を原子論理式にすれば十分だった。
'<<'の検査にはこれだけでは不十分で、Nを名前の無限集合だとして、
- (p) ∀γ∈N.[(_.γ)∈型]
が必要になる。無限個の名前と無限個の型がでてくるが、型は、オブジェクト型（の型表現）Tを使って T.γ と書ける。つまり、
- (p) ∀γ∈N.[(_.γ)∈T.γ]
名前の無限集合Nは、通常「有限個の名前を除くすべての名前」として与えられる。検査実行時には、具体的なインスタンスが与えられるので、Nのなかの有限個の検査が実行される。だが、この有限個が検査のたびに毎回動的に変わる。この意味で、動的PCLと呼ぶことにする。動的PCLは、効率の観点からはうれしくない。
型解析：用語 型マップ
見た目はオブジェクト型（の型項、型表現）とまったく区別できないが、名前と型の対応を型マップと呼ぶことにする。'<<'の右側は型マップ。型マップがオブジェクト型と違う点は：
- ワイルドカードは現れない。
- 出現しない名前（プロパティ名）に対する型は単に未定義、ほんとに未定義。never?やany?で補完して解釈することは一切しない。
左に型更新演算子が含まれるとき
xは変数、Kは変数を含まない型マップ、Tは任意の型（型項、型表現）だとして、証明ターゲット x<<K ⊆ T を考える。
x<<K は、暗黙に x も x<<K もオブジェクト型（明示的タグもなく、確定（非オプショナル）型）であることを含意しているので、Tがオブジェクト型でないときは証明ターゲット x<<K ⊆ T は成立しない。
したがって、http://d.hatena.ne.jp/m-hiyama-memo/19100110/1263114915 の右側分類で可能性があるのは：
- Tがオブジェクト型
- Tがオプショナル型
- Tが排他的ユニオン型
- Tがインターセクション型
- Tが変数
このなかで、オプショナル型、排他的ユニオン型、インターセクション型は分解還元処理を続けると、Tがオブジェクト型または変数のケースに帰着できる。Tが変数yのときは、証明ターゲットは x<<K ⊆ y で、推論は終り。
残るは、Tがオブジェクト型のとき。
話を簡単にするために、K = {α:U, β:V} とする。まず、
- x.α⊆T.α
- x.β⊆T.β
だが、これは
- U⊆T.α
- V⊆T.β
Tはオブジェクト型なので、T.α、T.βはwell-defined、UとVも決まった型だから、U⊆T.α, V⊆T.β は新しい証明ターゲットとなり、従来と同様な推論を継続（進行）できる。
γをαともβとも違う名前だとして、x.γ⊆T.γ は、T.γ がわかっても、これ以上はどうにもならない。ユニフィケーションの出力としては、α、β以外のすべてのγに対する x.γ⊆T.γ を出力する。Tに型変数が含まれるときは、T内の型が他のユニフィケーションの効果により具体化される可能性がある。最終的に残った (_.γ)∈T.γ をすべて実行時検査条件に加えるしかない。
右に型更新演算子が含まれるとき
証明ターゲット S ⊆ y<<K を考える。
y<<K は、暗黙に y も y<<K もオブジェクト型であることを含意しているので、Sがオブジェクト型でないときは証明ターゲットは成立しない。したがって、http://d.hatena.ne.jp/m-hiyama-memo/19100110/1263114915 の左側分類で可能性があるのは：
- Sがオブジェクト型
- Sが変数
- Sがジョイン型
Sがジョイン型は分解還元処理により、他の2つの場合に帰着する。Sが変数のとき、証明ターゲットは x ⊆ y<<K 。これは、Kをopen-constraintsで解釈した型を K↑ として、x ⊆ (K↑) となり、今までの（<<なしの）推論に帰着できる。
K = {α:U, β:V} とする。まず、
- S.α⊆ y.α
- S.β⊆ y.β
はこのまま出力する。他のユニフィケーションとSIL推論によりyは具体化または消去される可能性がある。γをαともβとも違う名前だとして、S.γ⊆y.γ も同様な扱いになる。yが具体化されないままだと、これらの条件は実行時検査条件としては消去される。
