Type rule とは

タイプ理論では、タイプルールは、タイプシステムがどのようにタイプを構文構造に割り当てるかを記述する推論ルールです。これらの規則は、プログラムが適切に型付けされているかどうか、型式がどの型式を持っているかを判断するために、型システムによって適用されます。型ルールの使用のプロトタイプの例は、デカルト閉鎖カテゴリの内部言語である単純型のラムダ計算で型推論を定義することです。