极性与变性

(Polarity and Variance)

下一节归纳类型、余归纳类型与递归类型将用到“正位置（positive position）“和“负位置（negative position）”，并出现“负 × 负 = 正“这样的判断。这套极性（polarity）规则背后的概念，就是类型论中的变性（variance）——更具体地说，其中，我们只讨论协变（covariance）与逆变（contravariance）。本节先用嵌套函数参数把它们讲清楚。

变性：什么时候替换是安全的

Koka 的值类型是名义的（后面会澄清），写不出子类型替换的例子，所以本节的示例改用 TypeScript 联合类型来演示——联合类型的成员天然就是子类型：

type Dog = { kind: "dog" }
type Cat = { kind: "cat" }
type Animal = Dog | Cat   // 联合类型：Dog、Cat 都是 Animal 的子类型

返回位置：协变（正位置）

先看“产生动物“的场景——我们需要一个返回 Animal 的函数：

function adoptOne(f: () => Animal): string {
  return "领养了 " + f().kind
}

adoptOne 只会把 f 的返回值当作 Animal 使用，所以返回类型可以比 Animal 更“窄“：

• 提供 () => Dog（返回更“窄“）：Dog 本身就是 Animal，一切消费 Animal 的代码都成立——安全
• 提供返回类型比 Animal 更“宽“的函数：返回值未必是 Animal，kind 属性可能不存在——不安全

输出位置要求“宁窄勿宽“：更窄的值类型仍然能安全替换更宽的，子类型关系的方向保持不变（同向），这种替换称为协变（covariant），对应正位置。

参数位置：逆变（负位置）

再看“消费动物“的场景——我们需要一个“描述任意动物“的函数作为参数：

const dog: Dog = { kind: "dog" }
const cat: Cat = { kind: "cat" }

function describeAll(f: (a: Animal) => string): string {
  return f(dog) + ", " + f(cat)
}

describeAll 在内部会把 Dog 和 Cat 都传给 f，所以 f 的参数类型必须至少能接受 Animal：

• 提供 (a: Dog) => string（参数更“窄“）：f(cat) 时崩溃——不安全
• 提供参数类型更“宽“的函数：任何调用都成立——安全

输入位置要求“宁宽勿窄“：更窄的参数类型反而不能替换更宽的，能站上来的必须是更宽的类型——子类型关系的方向发生反转（反向），这种替换称为逆变（contravariant），对应负位置。

一句话记忆：返回协变、参数逆变。输出位置可以收窄（协变），输入位置必须放宽（逆变）。

嵌套函数参数：极性翻转

(Flipping under nesting)

单个函数类型 a -> b 的规则很简单：参数 a 负位、返回 b 正位。但类型可以层层嵌套，比如 (a -> b) -> c。逐层拆解：

1. 外层是一个函数：它的参数是 (a -> b) 这个整体——所以 (a -> b) 位于负位置；它的返回 c 位于正位置。
2. 内层 (a -> b) 又是一个函数：参数 a 位于内层的负位置，返回 b 位于内层的正位置。

现在数一数 a 的总极性：它先被外层当作参数（乘一个“负“），又在内层被当作参数（再乘一个“负“）：

负 × 负 = 正

为什么这里是“乘法“而不是别的运算？
因为极性可以编码成：正位置 = +1，负位置 = −1；穿过一层“函数参数“就乘一个 −1（翻转），穿过“返回/字段“就乘 +1（不变）。于是嵌套后，一个类型变量最终的极性 = 沿途所有层的符号相乘——负 × 负 = 正 就是 (−1) × (−1) = +1，本质是两次翻转等于不翻转。乘法恰好刻画“翻转奇偶次“的奇偶性，且对任意深度可结合；数学上，极性就是从类型树到乘法群 {+1, −1} 的一个同态。

所以 a 最终处于正位置——尽管它字面上写在“参数里“，但整体上对 a 而言是协变的。这正是下一节中 Foo(f: (foo -> int) -> int) 能通过检查的原因。

一般规则：每穿过一层函数参数，极性翻转一次。用表格概括：

练手：下面这个类型里，a、b、c、d 各处于什么极性？

type ex3
  con F(g : (a -> b) -> c -> d)

g 的类型 (a -> b) -> (c -> d) 解析：外层参数 (a -> b) 负位，外层返回 (c -> d) 正位。于是：

• a：负（外层参数）× 负（内层参数）= 正
• b：负（外层参数）× 正（内层返回）= 负
• c：正（外层返回）× 负（内层参数）= 负
• d：正（外层返回）× 正（内层返回）= 正

澄清：Koka 用的是 替选类型，不是继承

(Koka uses alternatives, not inheritance)

上面的例子用 TypeScript 联合类型展示子类型替换：type Animal = Dog | Cat 里，联合成员 Dog、Cat 是独立的类型，并且是 Animal 的子类型（Dog <: Animal），所以函数类型在参数/返回位置上的协变、逆变可以实际赋值验证（strictFunctionTypes 下，独立声明的函数类型参数逆变、返回协变）。

strictFunctionTypes 是 TypeScript 2.6 引入的编译选项，用于对‌函数类型参数‌启用‌逆变（contravariant）‌检查而非默认的双变（bivariant）检查，防止不安全的函数赋值，属于 strict 严格模式子集 。‌‌

Koka 没有继承，也没有这种子类型关系：type animal 配合 con Dog、con Cat 声明的是一个替选类型，Dog、Cat 只是它的两个构造子，本身并不是独立的类型，彼此之间不存在 <: 子类型关系；int 与 float 之间、函数类型之间同样没有子类型关系。因此上面 TypeScript 的“用更宽参数的函数替换“在 Koka 中写不出来——编译器会直接报类型不匹配。

那么极性在 Koka 里有什么用？答案是：变性的价值在子类型语言里是“替换“，而在 Koka 里是“良构性与终止性分析“。编译器遍历类型声明，计算每个类型变量的极性，据此：

• 判定 type 声明的递归是否合法（只允许正位置）→ 归纳类型的良构性（下一章会详细展开）
• 结合递归结构分析，推断函数是 total 还是 div → 终止性检查
• 为 co type（协归纳）与 div type（任意递归）的放宽提供理论基础

变性（variance） 描述的是：复合类型的子类型与其组成部分的子类型之间的关系。 极性（polarity） 描述的是：类型变量在语法树中出现的位置——正位置（输出）协变，负位置（输入）逆变。

• 嵌套函数参数让极性不断翻转（负 × 负 = 正），这是理解“类型藏在参数里为什么有时反而合法“的关键。

在 Koka 这样没有子类型的语言里，我们关心的不是“能否替换“，而是“递归是否良构、函数是否终止“——极性正是这两项检查的底层语言。