9.2带类型变量的入类型推断 9.2.1语言入 考虑语言入→的类型推断 语言入 类型由下面文法定义 t::=b t t->t 项由下面文法定义 M:=c|x|入x:x.M|MM ·入→的定型公理和推理规则同入→的相同 限制：项常量的类型一定不含类型变量9.2 带类型变量的→类型推断 9.2.1 语言t → 考虑语言t →的类型推断 • 语言t → – 类型由下面文法定义  ::= b | t |  →  – 项由下面文法定义 M ::= c | x | x: .M | M M • t →的定型公理和推理规则同→的相同 –限制：项常量的类型一定不含类型变量