System Fω

System F能够写“对任何元素类型A都可用”的函数。Fω还可以写“对任何容器形状F都可用”的接口。区别不是把类型变量名字换成大写，而是F本身具有输入kind：F A才是完整类型。

同时，类型表达式现在会计算。PairWith Int Bool可以先展开一个类型函数，化成Int×Bool，再与二元组值的类型比较。项级检查器必须知道这些不同写法何时表示同一个类型。

先检查类型算子，再检查项 ​

定义

它的kind为 $\ast \to \ast \to \ast$。再定义一个在任意F上工作的恒等操作：

在F、A的假设下，F A具有kind $\ast$，所以z的声明合法；项抽象后类型为 $FA\to FA$；依次作两次类型抽象，得到

检查应用

第一步，PairWith Int的kind是 $\ast \to \ast$，满足F的参数要求。第二步实例化A为Bool，待接收参数的类型成为

值 (7,true)恰有这个类型。因此整个应用类型为Int×Bool，求值结果还是 (7,true)。没有在运行时对Int或Bool作分支；类型应用只告诉检查器这次使用什么实例。

若把第一次参数改成Int，kind检查立即拒绝，因为 $\ast$ 不等于 $\ast \to \ast$。若参数是 (7,8)，kind全部合法，但项级类型不匹配：Int×Int不是Int×Bool。这两个错误属于不同层。

高kind不自动提供容器操作 ​

映射操作可以有如下接口：

这个类型是kind正确的，却不意味着任意F都自带满足容器规律的map。例如固定 $F=\lambda A:\ast .A\to \mathrm{Bool}$，给定 $f:A\to B$，预合成自然产生的是 $(B\to \mathrm{Bool})\to (A\to \mathrm{Bool})$，方向与上述map相反。忽略输入、总返回恒false谓词，确实可以凑出某个 $(A\to B)\to FA\to FB$ 函数；但即使f是恒等函数，它也会丢掉原谓词，不满足map应保持恒等操作的规律。

Kind只说明F怎样接收类型参数，不提供运行时映射操作，更不提供它保持恒等与复合的证据。若要写容器通用算法，通常把已经实现的map作为额外参数传入，并根据需要另声明或证明相应规律。

同样，两个算子都有kind $\ast \to \ast$，不表示它们定义相等。$\lambda A:\ast .A$ 与 $\lambda A:\ast .\mathrm{Bool}$ 分别是恒等算子和常量算子，在Int上得到不同类型。

与依赖类型、隐式推断的边界 ​

Fω不让类型读取任意运行时项。$\mathrm{\forall }F:\ast \to \ast$ 对类型算子量化，不是对自然数值量化。基础系统也没有一般类型级递归；若加入任意不终止的类型计算，就不能继续沿用这里的conversion判定过程。

本页的项是显式标注的。删除所有类型抽象、应用和注解后，重新恢复它们是另一个问题，不能从“显式类型检查可判定”推出“隐式推断只需扩展Algorithm W”。

显式检查的关键步骤是类型相等判定。类型层可视为带构造器的简单kind λ演算；良kind类型计算的正规化公理库简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个良类型简单 λ 项都强正规化：任意完整 β-归约路径都在有限步后结束。与类型级β的合流性公理库Church–Rosser 定理Church–Rosser theorem · Confluence theorem for beta-reduction完整 β-归约的合流定理：任意有限分叉都能继续归约到共同后继。给出可比的β正规形。检查器先验证kind，再将需要比较的类型正规化并作α等价比较；因此本页固定核心的检查会终止。正规化可能制造很大的中间类型，终止不等于具有小的多项式成本。

类型保持证明中多了一个重要引理：若 $\mathrm{\Delta },X:\kappa ;\mathrm{\Gamma }⊢t:T$ 且 $\mathrm{\Delta }⊢U:\kappa$，把U一致地替换进t、Γ和T，仍得到合法判断。这个类型替换引理支持项级类型应用的消去；不能只替换返回类型而遗漏项内参数注解。

Fω适合表达高kind库接口和显式多态编译核心。它把“接口需要什么类型构造器”“程序需要什么运行时操作”“哪些类型写法可通过计算互换”分成三个可检查问题，使后续加入字典或其他证据时有清晰边界。