型解析：動的なPCL (Path Check Logic)

型演算'<<'を扱うためには、推論も拡張しなくてはならないが、実行時の検査条件を記述するPCL(path check logic)の変更のほうがむしろ大きい。

今までのPCLは、pをパス、'_'を無名変数だとして、次の3つの形の式を原子論理式にすれば十分だった。

1. (p) exists(_) …… 値が存在する
2. (p) _ = スカラー定数 …… スカラー値が等しい
3. (p) _ ∈ スカラー型 …… 値の型が特定のスカラー型である

'<<'の検査にはこれだけでは不十分で、Nを名前の無限集合だとして、

• (p) ∀γ∈N.[(_.γ)∈型]

が必要になる。無限個の名前と無限個の型がでてくるが、型は、オブジェクト型（の型表現）Tを使って T.γ と書ける。つまり、

• (p) ∀γ∈N.[(_.γ)∈T.γ]

名前の無限集合Nは、通常「有限個の名前を除くすべての名前」として与えられる。検査実行時には、具体的なインスタンスが与えられるので、Nのなかの有限個の検査が実行される。だが、この有限個が検査のたびに毎回動的に変わる。この意味で、動的PCLと呼ぶことにする。動的PCLは、効率の観点からはうれしくない。