渐进类型

静态信息不够时，把义务放在边界上 ​

对于函数 $f:A\to B$ 与实参 $u:C$，普通静态应用要求实参符合参数类型。渐进类型可以在 $C\sim A$ 时接受应用，并插入从 $C$ 到 $A$ 的转换。若已知实参是 Bool、参数是 Int，一致性仍会立即拒绝；若一侧是 $?$，则由运行时值决定检查能否通过。

转换称为 cast。它不是把布尔值计算成整数，而是检查或记录值的类型。把整数送入未知类型区域时，附上 Int 标签；把未知值送回整数区域时，检查标签是否为 Int。这样，动态区域仍能保存值的真实类别，静态区域也不会被迫接受一个伪装成整数的布尔值。

先把源程序翻译清楚 ​

为了完整推演两个例子，取源项

$n$ 是整数常量，inc 是整数加一原语。沿用类型判断公理库类型判断Typing judgment由类型规则推导的上下文判断，记录项在给定变量假设下具有的静态类型。，把带翻译结果的判断写成 $\mathrm{\Gamma }⊢s:T⇝e$，表示源项有类型 $T$，并翻译成显式含 cast 的目标项 $e$。

对任何 $S\sim T$，定义转换构造器

$p$ 记录源代码边界及责任方向。同类型转换在翻译时省略，其他转换全部交给下文的目标核心。定义函数匹配 $\mathrm{fun}(A\to B)=A\to B$、$\mathrm{fun}(?)=?\to ?$；它在基础类型上未定义，因而不会静态接受已知整数的应用。

变量从环境取类型并原样翻译，整数与布尔常量也原样翻译为各自基础类型。抽象、应用和 inc 的规则是

应用边界的位置记为 $a$，inc 参数边界的位置记为 $b$。未知类型出现在函数位置时，翻译先插入到 $?\to ?$ 的检查；已知箭头的同类型转换由 $K$ 省略。类型推导归纳可知所有插入转换均满足一致性前提。

在环境 $x:?$ 下，$?\sim \mathrm{Int}$ 允许检查 inc x，翻译时插入投影。因此

且该函数具有 $?\to \mathrm{Int}$ 类型。把整数 7 或布尔 true 传给它时，应用规则分别插入 Int 或 Bool 到 $?$ 的注入。静态接受不是跳过检查，而是生成明确的检查位置。

函数 cast 核心的值与全部求值规则 ​

使用小步语义公理库小步操作语义Small-step operational semantics · Structural operational semantics用配置间的一步转移及有限或无限路径精确描述执行顺序、终止、卡住与发散。，按值、从左到右求值。记 $F=?\to ?$，ground 标签只有

$F$ 表示“可调用的函数”，并不编码它所有未来输入输出的类型。边界标签带极性 $p,\overline{p}$，满足 $\bar{\overline{p}}=p$；它们标识源边界的两侧，和三个运行时 ground 标签不同。沿用 $a,b$ 作为正标签。目标项与值为

后两类分别是 ground 注入和函数包装；内部项先成为值，整体才是值。包装先保存契约，等调用时检查。目标应用要求实参类型与参数类型精确相等，inc 要求 Int，其余常量、变量与 λ 使用通常规则。cast 与受控失败的规则是

$G$ 只是失败时所期望的标签诊断，不是 blame 的唯一静态类型；否则将失败传播出上下文时会破坏保持。类型规则保证每个注入的内容确实有其 ground 类型。

普通计算与基础身份转换为

替换避免捕获。箭头到相同箭头的显式 cast 仍是包装值；源翻译的 $K_{T,T}$ 可以直接省略它，因而不会出现“既是值又必须执行身份归约”的冲突。对 ground 投影，全部三种标签统一使用

非 ground 箭头 $A=S_1\to S_2\ne F$ 与未知类型之间必须经过 $F$：

$A\sim F$ 总成立，所以这些中间项良型。最后，函数包装的应用展开为

参数沿 $T_1\Rightarrow S_1$ 反向进入被包装函数，并翻转责任标签；结果沿 $S_2\Rightarrow T_2$ 出来，保留标签。运行时没有遍历所有函数输入来判断整个箭头契约，而是每次调用履行这两个义务。[3, §3.2]

求值上下文和失败传播为

传播保持原标签及其极性。允许从嵌套上下文直接传播或逐层传播时，步数可以不同，最终错误一致；下面的安全性不依赖选择哪一种传播步。

从两个源程序走到值与 blame ​

成功程序是 $(\lambda x:?.\mathrm{inc}x)7$。翻译后，入口注入和函数体投影都显式出现：

第一步是 $\beta$ 归约：带标签的实参已经是值。第二步比较标签后解包，第三步执行整数原语。

把源实参换成 true，静态阶段仍接受，因为 $\mathrm{Bool}\sim ?$。目标程序则保留布尔标签：

错误属于要求整数的投影位置 $b$。它发生在布尔值进入整数原语之前，因而不会形成没有归约规则的 inc true。

若将源函数注解改成 $\lambda x:\mathrm{Int}.\mathrm{inc}x$，调用 7 仍能通过，调用 true 则在源程序的应用规则处被拒绝：现在需要 $\mathrm{Bool}\sim \mathrm{Int}$，而该关系不成立。增加注解把这次错误从运行时边界提前到了静态检查。

函数边界：参数与结果在不同一侧负责 ​

令 $f=\lambda x:\mathrm{Int}.\mathrm{inc}x$，把它交给允许未知参数的调用者：

$w$ 已是值，但没有检验任一未来实参。写 $d_B(v)=⟨B\Rightarrow ?{⟩}^{a}v$。调用整数成功：

调用布尔则在进入 $f$ 之前得到 ${\mathrm{blame}}_{\mathrm{Int}}(\overline{p})$。这里是边界外的调用者给了不合要求的参数，故标签反转。

反过来，令 $g=\lambda x:?.d_{\mathrm{Bool}}(\mathrm{true})$，并要求它返回整数：

输入注入成功，失败在提供者返回的布尔值，因此保留正标签。这两条推导说明当前边界的责任方向；它们没有证明含任意多个共享标签的程序都满足某个全局 blame 定理。

把 $f$ 存入未知类型也不能只写一个任意箭头标签：

外部只有统一的函数标签 $F$，内部包装保留 Int 输入输出义务。投影回箭头时先检查 $F$，随后创建所需的箭头包装；若动态值装的是整数，则在 $?$ 到 $F$ 的投影处立即 blame，根本不会执行整数应用。

完整函数 cast 核心的安全性 ​

沿用进展与保持公理库进展与保持定理Progress and preservation · Type safety对按值调用的简单类型 lambda 演算逐层解释规范形、替换、进展与保持，以及类型安全的准确结论。的结构，先证明翻译保类型：若 $\mathrm{\Gamma }⊢s:T⇝e$，则目标判断 $\mathrm{\Gamma }⊢e:T$。对翻译推导归纳，变量、常量和 λ 直接成立；应用的两个 $K$ 分别把函数变为 $A\to B$、实参变为 $A$，于是目标应用得到 $B$；inc 的参数转换到 Int。恒等 $K$ 保留类型，其余由一致性和 cast 规则成立。

规范形。 对良型闭值反演其最后规则可得：Int 值是整数，Bool 值是布尔常量，$?$ 值是且只能是某个 $⟨G\Rightarrow ?{⟩}^{p}v$，箭头值是 λ 或函数包装。包装内部仍为箭头值，所以它可以形成有限栈；不能遗漏这一类而只为 λ 写应用进展。

保持。 替换引理按类型推导归纳，cast 分支重用内部归纳假设及同一一致性前提，blame 分支可在任何环境赋予所需类型。于是 β 归约保持结果类型。整数加一与身份规则直接保持；成功 ground 投影返回其类型前提已保证的 $G$ 值，失败则用 blame 的任意类型规则。两种经 $F$ 分解的规则中，内外转换的中间类型恰好相接。

函数应用是关键分支。原包装有目标类型 $T_1\to T_2$，实参 $v:T_1$；由于一致性对称且箭头逐分量一致，$⟨T_1\Rightarrow S_1{⟩}^{\overline{p}}v:S_1$。内部 $f:S_1\to S_2$ 接受该实参并产生 $S_2$，外部 $⟨S_2\Rightarrow T_2{⟩}^p$ 最后得到 $T_2$。上下文内归约由反演重建外层推导，失败传播则把同一 blame 赋予整个上下文的结果类型。因此 $\mathrm{\Gamma }⊢e:T$ 且 $e\to e^{\prime }$ 蕴含 $\mathrm{\Gamma }⊢e^{\prime }:T$。

进展。 对良型闭项的推导归纳，先沿求值上下文求出子项或传播 blame。应用两侧均为值时，规范形保证函数是 λ 或包装，分别由 β 或包装规则接住；inc 的值参数必为整数。对 cast 的值参数，枚举一致性允许的外形：相同基础类型与 $?$ 使用身份规则；箭头到箭头是包装值；ground 到 $?$ 是注入值；非 ground 箭头与 $?$ 之间使用分解规则；$?$ 到 ground 时，规范形提供唯一标签，以相等或不等两类穷尽检查。除此以外的基础类型冲突或基础/箭头直接转换没有类型推导。故结果是值、blame，或者存在下一步。

把两条定理沿运行组合，得到：源程序的目标执行若有限结束，就以正确类型的值或规定的 blame 结束，绝不会到达 inc true 或 7 8 这样的未定义状态。还允许无限运行；例如在完整源语言中

可以类型检查，未知函数规则使自应用继续展开。没有显式 fix 不意味着这个核心终止。

一个可完整证明渐进保证的片段 ​

现在固定较小的源语言，独立证明擦除绑定注解的保证。基本类型记为 $D::=\mathrm{Int}\mid \mathrm{Bool}\mid ?$，语法为

λ 只出现在立即调用位置，不能作为值存储、传参或返回；环境只含 $D$ 类型。仍可嵌套任意多次调用、重复使用基本变量，并让一个调用的输出进入下一调用。使用前述翻译规则，其源项结果总是基本类型或 $?$，所有插入的非身份转换都是基础注入/投影。此处没有函数包装，下面的渐进保证仅对这个片段证明；完整高阶语言的比较定理需要额外的项精度与模拟关系。[2, §4.3]

记 $s⊑s^{\prime }$ 表示只把一些绑定注解 $B$ 换成 $?$，其余语法、常量与边界位置保持不变；环境 $\mathrm{\Gamma }⊑{\mathrm{\Gamma }}^{\prime }$ 逐变量取相同方向。对整数或布尔原始常量 $k$，记 $\mathrm{tag}(k)$ 为它的基础类型，并定义与某个 $D$ 相容的运行表示

比较表示时忽略注入标签 $a$，不忽略常量或其 ground 标签。$s{\Downarrow }_{D}k$ 表示翻译执行成功，并返回 $k$ 的 $D$ 表示；$s\Downarrow \mathsf{blame}$ 只记录受控失败，不要求两个程序在同一标签失败。

定理。 若闭项 $s⊑s^{\prime }$ 且 $s:D$，则存在 $D^{\prime }$ 满足 $s^{\prime }:D^{\prime }$ 与 $D⊑D^{\prime }$，并且

这个片段的每个良型闭项都结束于值或 blame，故无需另列发散条款。证明分为以下相互依赖的步骤。

静态单调性与 cast 成功的单调性 ​

若 $C\sim D$、$C⊑C^{\prime }$、$D⊑D^{\prime }$，则 $C^{\prime }\sim D^{\prime }$：若两边都未擦除，复用旧判断；只要某一边成为 $?$，一致性直接成立。对源语法归纳，变量的结果类型随环境削弱，常量不变，inc 仍检查一个与 Int 一致的类型并返回 Int。立即调用中，实参和参数注解同时变得不更精确，刚才的事实保留边界一致性；函数体在削弱后的扩展环境中应用归纳假设，给出不更精确的结果类型。这证明定理的静态部分，不能把它误写成一致性本身有传递性。

基础边界处理一个已用 $C$ 表示的 $k$ 时，成功条件恰好是

前提是 $C\sim D$ 且输入表示存在；$C=D$、向 $?$ 注入和从 $?$ 投影三种情况分别给出这条等价式。成功结果就是 ${\mathrm{repr}}_D(k)$，标签选择不影响原始常量。于是当输入和目标均削弱为 $C^{\prime },D^{\prime }$，且两次输入表示同一 $k$，原边界成功就蕴含新边界成功：若 $D^{\prime }=?$ 自动成功；若 $D^{\prime }$ 是基础类型，则精度迫使 $D=D^{\prime }$，旧成功已经保证对应标签。这个引理比较任意允许的两条基础边界，并不限于注入后立刻投影的抵消。

环境求值与成功模拟 ​

用环境 $\rho$ 保存基本值表示。按原语法定义求值：变量查表，常量返回自己；inc 先求子项，再执行其类型到 Int 的 $K$，成功后加一；$(\lambda x:D.t)u$ 先求 $u$，执行实参类型到 $D$ 的 $K$，然后在 $\rho [x\mapsto v]$ 中求 $t$。任何子计算或边界失败就传播 blame。

这是对原始语法的结构递归：$u,t$ 都是真子项，环境只保存基本值，不保存可再调用的函数体。每个基础 $K$ 有限步结束，故该求值器总终止。对语法归纳，并在立即调用处使用避免捕获的值代换引理，可知环境求值与上述目标CBV求值返回相同常量或失败；目标的一次替换不会把环境中的值变成新的源调用。因此片段内的目标执行也终止。

同时归纳建立成功模拟：假设 $\rho ,{\rho }^{\prime }$ 给同名自由变量提供同一原始常量的相应类型表示。变量、常量直接对应；inc 的成功前提使旧投影得到某整数 $k$，子项归纳假设和 cast 单调性使新投影得到同一 $k$，两边都返回 $k+1$。立即调用先由实参归纳假设得到同一常量，再用 cast 单调性使新参数边界成功；扩展环境仍逐变量表示相同常量，于是函数体归纳假设给出相同结果。这得到定理第一条。

总终止性与安全性说明精确程序只有成功或 blame 两种结局。若较弱程序成功而精确程序也成功，第一条与求值结果唯一性迫使常量相同，得到第二条；若较弱程序失败但精确程序成功，第一条会推出较弱程序成功，矛盾，得到第三条。结论允许增加信息引入 blame，也不声称失败位置保持不变。

擦除注解可以移除一个实际失败的边界 ​

取两个语法对应的良型程序

二者内层都把布尔值注入 $?$ 后返回；外层静态实参类型为 $?$，所以两者都可类型检查。$s$ 的外层必须投影到 Int，运行得到 blame，即使函数体没有用到 $x$ 也不能跳过CBV实参检查。$s^{\prime }$ 擦除了这个注解，外层身份边界直接接受原未知值，返回整数 $7$。

这是定理允许的变化：更多信息导致的失败可在擦除后消失，精确程序本来成功的计算则不能因擦除而新增失败。前面 $\lambda x:\mathrm{Int}.\mathrm{inc}x$ 调用整数的成功例，在擦除后仍返回相同整数；调用布尔而直接被静态拒绝的版本，不满足定理要求的“精确程序已经良型”前提。

渐进类型由此把三种问题分开：一致性决定边界是否可延后检查，运行时转换保护每次实际调用，精度与模拟则说明调整静态信息会怎样改变程序行为。安全性只排除未定义卡住，不能单独推出渐进保证。