証明ターゲット S ⊆ y<

xは変数、Kは変数を含まない型マップ、Tは任意の型（型項、型表現）だとして、証明ターゲット x<

見た目はオブジェクト型（の型項、型表現）とまったく区別できないが、名前と型の対応を型マップと呼ぶことにする。'<<'の右側は型マップ。型マップがオブジェクト型と違う点は： ワイルドカードは現れない。 出現しない名前（プロパティ名）に対する型は単…

型演算'<<'を扱うためには、推論も拡張しなくてはならないが、実行時の検査条件を記述するPCL(path check logic)の変更のほうがむしろ大きい。今までのPCLは、pをパス、'_'を無名変数だとして、次の3つの形の式を原子論理式にすれば十分だった。 (p) exists(…