在类型论中, 构造规则是指一类推导规则, 这些规则描述如何构造出某个类型的实例的规则, 类似于生成元.
极性为正的类型的构造规则往往可以表达为函数, 这些形如函数的表达式一般被称为构造子.
每个形成规则都会配备一组构造规则. 构造规则可以有 0 个, 例如空类型, 也可以有数个, 例如自然数类型.
与之对应的是消去规则.
构造规则 • 英文 introduction rule • 法文 règle d’introduction • 拉丁文 regula introductionis
构造子 • 英文 constructor