言葉と記号法の問題が色々とある。型代入（type substitution, 行為とオペレータの意味がある）は構文的操作、型環境は意味論的な概念としよう。そう定義する。型環境は型評価に使う。型評価は型計算と言ってもいいが、型項を具体化して結果として具体型を求…