タイピング・グリッド

また裏紙に描いた絵。

これは、型付け〈タイピング〉を一般的に考えるときのテンプレートで、kを決めて使う。kをズラしながら使うこともある。これで、無限階層の型理論が考えやすくなるぞ。だいぶ分かりやすい。