为何逆变规则在[b]→Int < a→Int这类场景中不适用？

首先明确几个核心概念：

• 类型子关系S < T的本质：所有具有类型S的表达式都能安全替换到需要T的上下文。
• 函数类型的逆变规则仅适用于同层级的类型比较：S₁→R < T₁→R 当且仅当 T₁ < S₁（参数逆变），且该规则针对的是单态类型或已实例化的多态类型，而非未实例化的多态类型本身。

逐一澄清你的例子与困惑 #

1. 高阶多态函数的子类型关系

(∀b. [b]→[b])→Bool < (∀a. a→a)→Bool 成立的逻辑：
这里比较的是以多态类型为参数的函数类型。根据逆变规则，函数F₁→Bool < F₂→Bool等价于参数类型的子关系反转（即F₂ < F₁）。

• F₁是∀b. [b]→[b]（仅能处理列表的多态函数），F₂是∀a. a→a（能处理任意类型的多态函数）。
• F₂的表达式可以安全替换F₁的位置（比如id函数可实例化为[b]→[b]），但反过来不行，因此F₁ < F₂。
• 结合逆变规则，F₁→Bool < F₂→Bool成立：当你把F₁→Bool类型的函数当作F₂→Bool使用时，传入的F₂类型参数可被安全适配为F₁类型（因为F₂更通用，满足F₁的参数要求）。

2. 一阶多态函数的子类型困惑

你疑惑的[b]→Int < a→Int不成立，而a→Int < [b]→Int看似合理，核心问题是混淆了多态类型的全称量化与单态类型的自由变量：

• 实际中[b]→Int是多态类型∀b. [b]→Int（比如length的类型），而a→Int如果是单态类型（a是某个固定类型，比如Int），两者无任何子类型关系——[Int]→Int不能替换Int→Int，反之亦然。
• 如果a→Int是多态类型∀a. a→Int（比如const 5的类型）：
  • ∀b. [b]→Int < ∀a. a→Int不成立：length无法接受任意类型参数（比如Int），不能替换const 5的位置。
  • ∀a. a→Int < ∀b. [b]→Int也并非严格子类型关系，但∀a. a→Int的表达式可被实例化为∀b. [b]→Int（把a绑定为[b]），因此const 5可安全替换length的位置——这是多态实例化，而非子类型关系。

你对逆变规则的误解点 #

你认为[b]是特定类型、a是任意类型，所以[b]→Int应该是a→Int的子类型，这忽略了：

• 逆变规则针对的是参数类型的子关系，而非“具体/通用”的直觉判断。对于单态类型[U]→Int和U→Int，要满足[U]→Int < U→Int，需要U < [U]（逆变要求参数类型U是[U]的子类型），这显然不成立（比如Int不是[Int]的子类型）。
• 多态类型的子关系需要对所有实例都成立，而非单个实例。∀b. [b]→Int要成为∀a. a→Int的子类型，必须对所有类型U，[U]→Int < U→Int都成立，这显然做不到。

关于length的类型注解 #

length无法用a→Int做注解，是因为a→Int是单态类型（a是固定类型），而length是多态函数，必须用多态类型∀b. [b]→Int注解——它只能接受列表类型参数，无法适配任意类型的a。

内容的提问来源于stack exchange，提问作者NisNis