固定一套类型规则和语境 $\mathrm{\Gamma }$，考虑类型判断 $\mathrm{\Gamma }⊢𝑡:𝑇$。$\mathrm{\Gamma }$ 记录变量的类型假设，记号见 [定义] 类型与类型判断 。三种问题的区别在于给定什么、要找什么，不是另换三套类型规则：

把 [定义] 良类型 的良类型定义写成带语境的形式，问的就是：固定一个项，是否存在类型，即 $\exists 𝑇.\mathrm{\Gamma }⊢𝑡:𝑇$。居留性问的是：固定一个类型，是否存在项，即 $\exists 𝑡.\mathrm{\Gamma }⊢𝑡:𝑇$。不要把两个存在量词的位置看反：推理找的是类型，不是程序；居留性判定只需回答有无，若还要返回一个居留者，就进一步成了构造项的问题。

例如，采用 [定义] 类型与类型判断 的七条规则：

• 检查给定的 $\text{pred }0:\text{ Nat}$，答案是成立；检查同一个项的 $\text{pred }0:\text{ Bool}$，答案是不成立。
• 推理给定项 $\text{pred }0$ 的类型，得到 $\text{Nat}$，不要求调用者先给出这个类型。
• 判断 $\text{Nat}$ 是否可居留，$0:\text{ Nat}$ 就提供了见证；判断 $\text{Bool}$ 是否可居留，$\text{true }:\text{ Bool}$ 就提供了见证。这两种类型都可居留，却不意味着每个项都有类型：$\text{succ }\text{ true}$ 仍然不良类型。

Rust 算法 type_of(t) -> Option<Type> type_of(t) -> Option<Type> 按输入／输出划分是推理接口：给它项，它返回类型。它也常被广义地叫作“类型检查器”，因为它同时判定项是否良类型。带期望类型的检查接口则是 check(t, expected) -> bool check(t, expected) -> bool 。在这套规则下，可以用 type_of(t) == Some(expected) type_of(t) == Some(expected) 实现它；这依赖 [定理] 类型唯一 ，以及算法相对规则的 [定理] 算法可靠性 与 [定理] 算法完备性 。实际的检查器也可以交替使用检查与推理；接口的区分，不要求实现拆成两套互不相干的算法。

常见误区

1. “检查失败，就说明这个项没有任何类型。”检查针对的是一个给定类型。$\text{pred }0:\text{ Bool}$ 不成立，只排除了 $\text{Bool}$；这个项仍有类型 $\text{Nat}$。要说它不良类型，必须排除所有可能的类型，不能把“不是期望的类型”说成“没有类型”。

2. “推理器没有给出类型，就证明规则里不存在类型。”把算法的拒绝解释成“规则无法定型”，需要相对规则的完备性。在 [附注] 算术语言形式化的未展开前提 的实现假设下，这里的 type_of type_of 终止且相对规则完备，所以正常返回 None None 确实表示项不良类型；但在其他系统中，推理器可能只支持规则的一个子集，或要求额外标注。缺少标注、超时、资源不足或搜索尚未结束，都不能直接当作无类型的证明。

3. “类型推理就是运行程序，看看结果是什么类型；不写标注就是动态类型。”这套算术语言的推理按项的语法和类型规则分析，不执行 $⟶$ 来观察结果。静态类型系统也可以推理出省略的类型标注；检查与推理的区别在于是否给定期望类型，静态与动态的区别则在于检查何时发生，见 [附注] 静态类型与动态类型 。

4. “推理返回的就是唯一类型，检查时比较相等总是够用。”唯一性是这套规则已经证明的性质，不是“类型推理”这个词自带的保证。例如，若在七条规则外增加“由 $𝑡:\text{ Nat}$ 推出 $𝑡:\text{ Bool}$”的转换规则，$0$ 就同时具有这两个类型。只返回 $\text{Nat}$ 再与期望的 $\text{Bool}$ 比较，会误拒绝一个在扩展规则下成立的判断。带子类型或多态的系统可能需要子类型判定、实例化等步骤；若还要求推理返回最一般的主类型（principal type），也必须另行定义“更一般”，并证明主类型存在。

5. “能检查或推理，就能判定类型居留性；几个候选都失败，就说明类型不可居留。”检查、推理已经拿到了项，居留性却要问是否存在任何合适的项。否定一个候选不能否定存在性；候选可能有无穷多个，只靠逐一枚举、检查，也未必能在没有居留者时停下来回答“没有”。反过来，这也不说明居留性总是不可判定：这套算术语言的两个类型都有现成见证。三种问题是否可判定，要针对具体系统分别论证。

6. “语境中能找到居留者，就已经找到了不依赖假设的程序。”在含变量的语言中，若 $\mathrm{\Gamma }$ 已有 $𝑥:𝑇$，变量 $𝑥$ 就可在这个语境中居留 $𝑇$；去掉该假设后，判断未必仍成立。没有另外指定语境时，说“$𝑇$ 可居留”通常指存在闭项 $𝑡$（没有自由变量），使 $⊢𝑡:𝑇$。 [定义] 词项的集合 的算术语言没有变量，所有词项都是闭项，因此这里取空语境。

7. “有居留者，就有一个正常的值，而且程序一定能算出它。”这里的居留者是具有类型的项，不要求它已经是值。在允许一般递归或异常的语言中，项有类型也可能永远循环或异常退出，不能据此断言会正常返回该类型的值。相应地，“底类型没有正常值”不等于“没有表达式能具有底类型”，具体例子见 [附注] 显式错误规则与 Kotlin 的底类型 。