为获得高质量类型错误而设计的类型推断
为获得高质量类型错误而设计的类型推断
Feb 14, 2025 类型推断因在出现类型错误时，导致编译器产生无用的错误消息而臭名昭著。 例如，这是一个典型的评论：
我在工作中使用 flowjs 启动了一个项目，在与根本原因不同的文件中出现了难以理解的类型错误，然后放弃并选择了 typescript。
然而，事情不必如此。类型推断的坏名声是由于现有语言中的设计决策，这些决策牺牲了良好的错误消息以换取其他目标。 类型推断本身并没有阻止您提供良好的错误消息。
我最近发布了 PolySubML，一种将全局类型推断与子类型和高级多态相结合的编程语言，并且支持良好的类型错误消息是开发过程中始终考虑的因素。 在这篇文章中，我将解释我是如何设计 PolySubML 的错误消息的，以及为什么我认为现有语言在这方面往往表现不佳。
但首先，一些免责声明：
首先，这篇文章只关注 **类型错误 ** 的错误消息。处理 _语法错误 _，特别是解析器错误，是一个完全不同的话题，不在本文的范围内。
其次，这里的重点是帮助用户 ** 了解他们的代码为什么不能编译 ** 并识别错误的原因。在某些情况下，编译器也会尝试猜测用户的意图并提出修复建议，但这本质上是基于启发式方法和主观的，不在本文的范围内。
最后，PolySubML 是一种实验性的业余编程语言，从未大规模使用过。 它是我的想法的一个 ** 概念验证 ** 和 _ 演示 _，但它与广泛使用的、经过实战检验的语言截然不同。 由于 PolySubML 是一个单人业余项目，因此重点是 _ 底层算法 _ 和设计方面，而不是像润色这样的方面，润色是时间和人的函数（特别是 Rust 编译器多年来几乎无限地进行了润色，这要归功于其庞大而专注的社区。）
排除了这些，让我们开始讨论那些经常导致编译器错误消息糟糕的陷阱：
规则 1：永远不要猜测或回溯
一般来说，用户在将代码提交给编译器时认为他们的代码是正确的。 有时，人们会尝试推测性地编译以尝试在重构期间识别错误或需要更新的地方，但即便如此，用户也仅仅认为 _ 在抽象层面的某个地方 _ 可能存在错误。 除非编译器提供具体的证据解释哪里以及为什么存在错误，否则他们不会相信存在错误。 （或者更确切地说，违反了语言的类型规则，这 _ 通常 _ 但不一定表明存在错误。）
** 编译器错误消息的作用是向用户证明他们的代码根据语言的规则是无效的 ** ，理想情况下，以一种可以帮助用户识别他们在哪里出错以及如何纠正问题的方式。
从抽象的角度来看，类型检查的过程可以建模为推导关于代码的 _ 一组事实 _，并根据特定的规则从先前的事实中推导出新的事实，这些规则由语言决定。 例如，您可能有如下推理：“4 的类型为 int”，以及“如果 4 的类型为 int，那么在 let x = 4 之后，x 的类型也为 int”，以及“在 x.foo 中，x 必须是一个 record”，以及“如果一个类型为 int 的表达式用作 record，则程序无效”。
规则的一般形式是“如果 A 且 B 且 C，则 D”，其中类型检查器一旦满足左侧，就会不断地从规则的右侧推导出事实。 最终，它要么推导出矛盾并报告类型错误，要么不这样做并且代码编译成功。 这导致证明相对较短且易于理解 - 一旦达到矛盾，您可以轻松地向后工作，并逐步向用户展示一个解释其代码为何无效的序列。 （实际上，出于冗长的原因，您可能不想向用户显示 _ 每个 _ 步骤，但关键是如果需要，您可以这样做。 更多信息请参见第 3 节。）
但是，如果您的语言包含“如果 A 且 B 且 C，则 D ** 或 E **”形式的规则，那么这一切都会出错。 突然，编译器必须 _ 猜测 _ 如何进行，而不是从头到尾单调地进行。 这意味着编译器必须尝试 _ 每一种可能性 _ 才能发现类型错误。 例如，如果您知道 A、B 和 C，这可以让您得出“D 或 E”，但“D 或 E”本身根本没有帮助。 如果说 D 最终导致矛盾，您不能像以前那样立即报告错误 - 相反，您必须回溯并查看 E 是否也导致矛盾 _。
Ad-hoc overloading
上面的描述非常抽象，所以让我们看一个更具体的例子 - 特别是 ad hoc overloading。在某些语言中，您可能有多个具有相同名称和不同类型签名的函数，并且编译器需要依次尝试每个函数，并且只有当 _ 每个可能的选择 _ 都导致错误时才能报告类型错误。
例如，在 Java 中，您可能有类似这样的东西
void foo(A x) {}
void foo(B x) {}
void foo(C x) {}
//...
foo(v);
其中 A、B 和 C 是不同的类型。为了对 foo(v) 进行类型检查，编译器必须尝试所有三个可能的 foo 函数，以查看 _ 任何一个 _ 是否通过类型检查。如果 v 的类型为 C，那么它将首先尝试 A，发现一个类型错误，回溯并尝试 B，发现一个类型错误， _ 再次 _ 回溯并尝试 C，最后找到一个有效的匹配项。如果 v 相反具有 _ 其他 _ 类型，例如 D，那么类型检查器将必须尝试所有三个函数才能证明存在类型错误。
那么为什么这会如此糟糕呢？不得不猜测和回溯会使类型检查非常慢，但它 _ 也 _ 会使编译器错误消息变得非常糟糕。
如果没有猜测，错误消息会很简单且容易，因为有一条直接的推理链会导致矛盾。 但是，当类型检查器必须像 overloading 示例中那样进行猜测时，这一切都会消失。
为了向用户证明 foo(v) 存在类型错误，编译器必须证明 v 没有类型 A（通过一些推理链） _ 并且 _ 证明 v 没有类型 B（通过另一个推理链） _ 并且 _ 还证明 v 没有类型 C。 突然，错误的证明长度是原来的三倍。 但更糟糕的是， _ 这对用户完全无用 _。
_ 用户 _ 不关心 _ 每一种 _ 可能性。 用户打算调用 _ 某个特定的 _ 函数 foo，而不是每个可能的函数。 也许他们 _ 打算 _ 让 v 的类型为 B 并犯了一个错误。 （或者，也许 v 的类型为 D 是正确的，但他们错误地认为有一个版本的 foo 接受 D 作为参数。）
如果用户打算让 v 的类型为 B，那么他们关心的是 v _ 不 _ 具有类型 B 的证明（这样他们就可以弄清楚错误是什么并纠正它）。 他们根本不关心编译器还检查了 A 和 C 的假设可能性并发现这些也不起作用，因为他们从未打算这样做！
** 如果您强制类型检查器进行猜测，它会猜测用户不打算猜测的事情，并且由此产生的错误消息将变得臃肿并且与用户无关。**
指数级增长
从前面的例子中，你可能会同意 overloading 不好，但没有 _ 那么 _ 糟糕。 毕竟，在这种情况下，检查参数的类型应该是微不足道的，因为所涉及的类型非常简单（至少在没有继承或任何东西的情况下）。 然而，这是为了示例而设计的尽可能简单的案例。 Overloading 会变得更糟。 _ 更加 _ 糟糕。
例如，通常语言不会强制用户在 _ 字面上每个程序中的每个表达式 _ 上注释类型。 这意味着通常事物的类型暂时未知并且必须被推断。 你可能必须经历一个完整的推断链来排除每种情况，而不是仅仅根据 A、B 和 C 检查 v 的已知类型并立即检测到矛盾。
更糟糕的是，函数通常有多个参数，因此猜测使用哪个 overload _ 也会 _ 影响函数中的 _ 每个其他 _ 参数应该采用什么类型。 这意味着猜测会级联，并且对于第一个参数的每个猜测，您都必须独立地检查其他参数，这反过来可能涉及更多的猜测和回溯。 同样，当类型是泛型时，检查参数的类型可能不是微不足道的，因此检查顶层类型的猜测需要递归来检查类型参数，这反过来又涉及更多的猜测。
这意味着这种猜测通常会 _ 指数级地 _ 爆炸。 对于每个顶层猜测，您都必须尝试第二个级别决策点的每种可能性，并且对于 _ 这些 _ 中的每一个，您都必须尝试第三个级别决策点的每种可能性，依此类推。
这不仅仅是一个理论问题。 在 Swift 中，即使是非常基本的表达式也会导致类型检查中的指数级爆炸。 像 let g: Double = -(1 + 2) + -(3 + 4) + 5 这样简单的东西在 Swift 3.1 中需要 20 秒 才能进行类型检查。 问题不仅仅限于 Swift。 Swift 有（或曾经有）一种特别诅咒的设计，即使是 _ 整数文字 _ 也会导致指数级爆炸，但相同的问题可能发生在任何具有 ad-hoc overloading 的语言中。 例如，这是某人在 Java 中遇到指数级类型检查。
更糟糕的是 C++，它的模板系统运行的原则是 “替换失败不是错误”，大致意思是“尝试每一种可能性，并且只有当每种选择的组合都导致失败时才报告错误”。 这意味着模板的使用通常会导致 a) 编译时间呈指数级增长，以及 b) 编译错误消息呈指数级增长。 更糟糕的是，滥用此“功能”已成为 C++ 社区中的 _ 标准做法 _（称为“模板元编程”）。 C++ 因编译速度慢和拥有 _ 大量 _ 完全难以理解的错误消息而闻名，而这是一个主要原因。
因此，确保良好的错误消息的第一步也是最重要的一步是 ** 设计您的类型系统，以便类型检查器永远不必猜测或回溯 **。
规则 2：不要急于下结论
第一条规则仅仅困扰着 _ 大多数 _ 现实世界中的编程语言。 现在是时候谈论 _ 真正 _ 有争议的事情了，几乎每种语言都犯了错误。
考虑以下 Ocaml 代码：
let _ = [1; ""]
编译此代码会导致错误消息：
File "bin/main.ml", line 1, characters 12-14:
1 | let _ = [1; ""]
^^
Error: This expression has type string but an expression was expected of type
int
此错误消息告诉我们 "" 的类型为 string，这很好，但它也声称它应该具有类型 int，这没有明显的原因，这不太好。 Ocaml 中的列表没有任何内在要求它们必须是 ints。 像 [""; ""] 这样的东西可以编译得很好。 冲突的 _ 实际 _ 原因是 Ocaml 根本没有突出显示的 1 _ 紧挨着 _ 突出显示的部分。
现在在这种情况下，示例足够小，用户可能只需通过查看错误点 _ 附近 _ 的代码就可以推断出不匹配的实际原因。 但是，随着代码变得越来越大和越来越复杂，这很快就会变得不可能。 例如，考虑以下情况：
type 'a ref = {mutable v: 'a}
let v = {v=`None}
(* Fake identity function which secretly stores the value in shared mutable state *)
let f = fun x -> (
match v.v with
| `None -> let _ = v.v <- `Some x in x
| `Some old -> let _ = v.v <- `Some x in old
)
(* assume lots of code in between here *)
(* blah blah blah *)
let _ = 1 + f 1
(* assume lots of code in between here *)
(* blah blah blah *)
let _ = 5.3 -. f 2.1
这将产生以下相当无用的错误消息：
File "bin/main.ml", line 19, characters 17-20:
19 | let _ = 5.3 -. f 2.1
^^^
Error: This expression has type float but an expression was expected of type
int
就这样，整个编译器输出。 同样，我们可以看到突出显示的表达式是一个 float，但绝对没有迹象表明 _ 为什么 _ Ocaml 希望它是一个 int。
与之前的示例不同，查看周围的代码也不会使其更加清晰。 即使查看附近调用的 f 函数的定义也没有帮助，因为 f 没有显式的类型签名。 不匹配的实际原因是代码中不同 _ 调用 _ f，而没有任何指示如何找到它。
这里的根本问题是，当 Ocaml 要求两个类型相等时，它实际上并没有跟踪它希望相等的类型。 它只是盲目地 ** 假设它碰巧看到的第一个类型是绝对真理 **，并在此假设下进行。 这样做确实使类型检查稍微快一些（由于需要跟踪更少的数据），这可能是 Ocaml 编译器以这种方式实现的原因。 然而，结果是完全无用的错误消息。
如果用户编写 [1; ""]，那么他们可能打算让它成为一个 ints 列表，并且 "" 是不正确的。 但也可能是他们打算拥有一个字符串列表，并且 1 是不正确的部分。 （或者可能，用户只是不知道 Ocaml 禁止在同一个列表中同时包含 ints 和 strings，并且只要错误消息没有解释这种限制，无论哪种方式都会感到困惑。）
那么更好的错误消息会是什么样子？ 让我们看看 PolySubML 如何处理相同的示例。 代码并不完全可以直接比较，因为 PolySubML 首先根本不强制类型相等，但在这种特殊示例中，最终结果仍然相同，因此它仍然提供了有用的比较。
这是之前相同的代码，转换为 PolySubML：
let v = {mut v=`None 0};
(* Fake identity function which secretly stores the value in shared mutable state *)
let f = fun x -> (
match v.v <- `Some x with
| `None _ -> x
| `Some old -> old
);
(* assume lots of code in between here *)
(* blah blah blah *)
let _ = 1 + f 1;
(* assume lots of code in between here *)
(* blah blah blah *)
let _ = 5.3 -. f 2.1;
这是 PolySubML 编译器的输出：
TypeError: Value is required to have type float here:
(* blah blah blah *)
let _ = 5.3 -. f 2.1;
^~~~~~~~
However, that value may have type int originating here:
(* blah blah blah *)
let _ = 1 + f 1;
^
(* assume lots of code in between here *)
Hint: To narrow down the cause of the type mismatch, consider adding an explicit type annotation here:
match v.v <- `Some x with
| `None _ -> x
| `Some (old: _) -> old
+ ++++
);
请注意 PolySubML 如何显示冲突的双方，类型为 int 的值从何处开始，然后流到需要类型 float 的位置。 不仅如此，错误消息还建议添加手动类型注释以帮助缩小错误的原因。 这将我们带到下一个规则，这是我为 PolySubML 提出的一个技术，据我所知以前从未这样做过。
规则 3：要求用户澄清意图
在我之前的语言 CubiML 中，类型错误消息显示 a) 一个值从某个类型开始的地方，然后 b) 流向需要不兼容类型的使用的地方。 对于简单的情况，这已经足以让用户理解问题。 然而，由于类型推断，从 a) 到 b) 可能存在任意长而复杂的路径，用户无法理解。 例如，在上一节中，int 流入一个函数调用，通过一个可变字段，一个匹配表达式，然后流出函数，流向同一个函数的另一个调用。
正如前面的章节中所描述的，存在一个从提供的源代码和语言的规则开始的推断链，该链导致矛盾。 然而，编译器不知道该链中的 _ 哪一部分 _ 包含问题。 用户的错误可能在该链中的任何一点。
一种方法是向用户显示导致矛盾的整个推理链。 这肯定会确保也显示了真正错误的那个部分。 然而，冗长的错误消息是无用的，因为用户将无法真正搜索冗长的输出以找到真正与他们相关的一个部分。 因此，我们需要保持错误消息相对较短，这似乎是一个不可能的矛盾。
幸运的是，还有另一种可能性 - _ 要求用户澄清 _ 以缩小其错误的位置。 不要向用户呈现整个链，而只需要求在链中的某个点提供基本事实，这将反过来排除一半并允许您逐步缩小错误的位置。
例如，查看上一节中显示的 PolySubML 错误消息的最后一部分：
Hint: To narrow down the cause of the type mismatch, consider adding an explicit type annotation here:
match v.v <- `Some x with
| `None _ -> x
| `Some (old: _) -> old
+ ++++
);
在类型错误的情况下，PolySubML 会列出冲突链中涉及的每个推断变量，然后选择一个（通常在中间附近）并建议用户为其添加显式类型注释。
假设用户添加了正确的类型注释，这会缩小问题范围。 例如，假设您有类似 int -> x -> y -> z -> float 的东西，其中类型为 int 的值流向类型为 float 的使用，在此过程中通过点 x、y 和 z。
假设我们建议用户向 y 添加类型注释。 也许用户打算让它成为一个 int，在这种情况下，我们得到 int -> x -> int -> z -> float，并且冲突缩小到 int -> z -> float 部分。 或者，也许他们打算让它成为一个 float，在这种情况下，冲突缩小到 int -> x -> float。 无论哪种方式，用户错误的位置都已缩小。
像这样建议类型注释的位置特别有效，因为这可能是用户无论如何都会做的事情。 面对他们无法弄清楚的令人困惑的类型错误，用户通常会开始向其代码添加额外的类型注释，以尝试缩小问题范围。
然而，如果用户不知道问题在哪里，他们通常也不知道在哪里添加类型注释是有用的 ， 并且会浪费大量精力而无所获。 相比之下，使用 PolySubML，编译器会明确突出显示一个位置，在该位置添加类型注释 _ 保证 _ 有助于缩小错误原因，从而实现更快、更有效的调试。
题外话：为什么还要进行类型推断？
类型推断的反对者通常会问，如果必须添加类型注释来跟踪错误，那么进行类型推断的意义何在。 首先，有一个明显的反驳，即无论使用何种语言，没有人会注释 _ 程序中的每个表达式 _，因为这根本不可行或没有用处，因此每个人都在某种程度上支持类型推断，这只是程度问题。
但另一点是，让您 5% 的时间注释 5% 的代码比要求您抢先 100% 的时间注释 100% 的代码要少得多。 尤其是使用 PolySubML，它会直接引导您找到问题，这意味着只需少量注释即可找到它。 而且，如果您真的想这样做，您可以再次删除类型注释（尽管您通常希望将它们保留下来作为文档等）。
当类型注释不足时
当类型冲突涉及一个或多个推断变量时，PolySubML 将显示冲突的端点 _ 并且 _ 如果用户不清楚，还会建议显式注释其中一个推断变量以帮助缩小冲突原因。
您可能会想，这都很好，但是在不涉及任何推断变量的类型冲突的情况下会发生什么？ 这是一个好问题，但不幸的是，我对此没有很好的答案。
好消息是，此类冲突本质上是本地化的。 例如，在 PolySubML 类型检查器中，每个函数都有一个类型化的签名。 如果用户没有为函数提供显式类型，则编译器只是隐式插入推断变量并改用它们。 这意味着任何不涉及推断变量的类型冲突也保证不会跨越任何函数边界。
同样，当没有可变 record 字段、非平凡模式匹配、多态实例化和大多数变量赋值的显式类型注释时，编译器也会插入推断变量，等等。 这意味着如果类型冲突没有通过任何推断变量，则类型冲突的范围本质上是有限的。
在没有推断变量的冲突的情况下，PolySubML 将显示冲突的端点（像往常一样）并显示在类型检查期间检测到冲突的表达式。 例如，在以下代码中：
let f = fun (x: int): int -> x + 1;
let a = 42.9;
let _ = f a;
PolySubML 的错误消息如下：
TypeError: Value is required to have type int here:
let f = fun (x: int): int -> x + 1;
^~~
let a = 42.9;
let _ = f a;
However, that value may have type float originating here:
let f = fun (x: int): int -> x + 1;
let a = 42.9;
^~~~
let _ = f a;
Note: Type mismatch was detected starting from this expression:
let f = fun (x: int): int -> x + 1;
let a = 42.9;
let _ = f a;
^
希望这些三个数据点以及冲突的受限范围足以让用户在大多数情况下理解问题。 但是，我担心在特别复杂的情况下，这可能还不够。
类型冲突中没有涉及推断变量这一事实意味着代码有效地在彼此旁边具有两个冲突类型。 但是，如果类型特别大且复杂，即使冲突类型并排，用户也可能无法确定有问题的部分。
我不确定解决此问题的好方法是什么。 与有广泛接受和理解的解决方案（即添加中间类型注释以缩小问题范围）的 _ 数据流 _ 链不同，用户无法在 _ 复杂类型签名本身内部 _ 明确阐明意图。 如果有人对这个问题有解决方案，请告诉我。 （请注意，无论您是否进行类型推断，这都是任何语言都会遇到的问题。）
规则 4：允许用户编写显式类型注释
如果您要建议用户添加显式类型注释以帮助缩小错误范围，则还需要使用户 _ 能够 _ 添加显式类型注释。
例如，考虑 _ 泛型函数 _。 泛型函数是一种对占位符类型（也称为类型变量）进行操作的函数，这些类型可以稍后替换为任何类型，特别是可以在代码中的不同点替换为多个 _ 不同 _ 类型。
在 PolySubML 中，泛型函数的一个例子是 fun (type t) (x: t): t -> x。 这是一个可以对 _ 任何 _ 类型进行操作的恒等函数。 它的类型签名没有提及特定类型，而是使用类型参数 t 定义的。 每当调用该函数时，类型参数都会被推断变量替换，每个调用站点的推断变量都不同，这个过程称为 _ 实例化 _。
这导致了问题：是否存在用于 _ 显式 _ 类型实例化的语法？ PolySubML 的设计尽可能地遵循 Ocaml 语法。 在 Ocaml 中，在实例化泛型类型时没有显式提供类型的语法。 他们可能没有看到这种需求，因为实例化的类型始终可以被推断出来。
然而，仅仅因为类型 _ 可以 _ 被推断出来并不意味着没有对显式语法的需求。 毕竟，用户可能想要显式地提供类型，以便缩小类型错误、记录类型或对代码施加额外的约束。
考虑以下示例：
let f = fun (type t) (x: t): t -> x;
let _: float = f 42;
在 f 42 代码中，f _ 可以 _ 用 t=int 实例化，在这种情况下，它将与预期的返回类型 float 冲突。 或者，可以用 t=float 实例化，在这种情况下，返回类型是正确的，但它与参数类型 int 冲突。 此代码存在冲突，但无法知道用户打算使用哪一半，哪一半是错误。 如果用户能够为 t 提供显式类型，则他们可以指示他们指的是哪一个，从而缩小错误范围。
在 PolySubML 中，如果可能，类型错误消息将建议向推断变量添加显式类型注释，这意味着用户需要一种方法来为任何类型的推断变量提供显式类型注释，包括那些由泛型函数实例化生成的变量。 这意味着我们需要用于显式实例化的语法。
由于 Ocaml 没有用于此的任何语法，因此我不得不为 PolySubML 提出我自己的语法。 在 PolySubML 中，您可以通过将类型放在表达式后面的方括号中来显式地实例化多态类型，例如 f[t=int]、f[t=float]、f[t=str -> bool] 等。
因此，上面的代码导致以下错误消息：
TypeError: Value is required to have type float here:
let f = fun (type t) (x: t): t -> x;
let _: float = f 42;
^~~~~
However, that value may have type int originating here:
let f = fun (type t) (x: t): t -> x;
let _: float = f 42;
^~
Hint: To narrow down the cause of the type mismatch, consider adding an explicit type annotation here:
let f = fun (type t) (x: t): t -> x;
let _: float = f[t=_] 42;
+++++
规则 4b：允许用户编写显式类型注释
在上一节中，我们看到您必须小心，以确保您的语言语法提供在必要时添加显式类型注释的位置。 然而，这并不是唯一可能导致用户无法添加类型注释的事情。
一个更常见的问题是，许多语言没有 _ 用于编写类型本身 _ 的语法。 例如，考虑以下 Rust 代码：
fn main() {
let x = 42;
let f: _ /* ??? */ = |y| x + y;
f(23);
}
此代码可以编译并且可以正常工作。 然而， _ 您无法添加任何可能的类型注释 _ 到 f（标记为 ??? 的部分），并且仍然可以编译代码（至少没有使用 Nightly 编译器并选择加入不稳定的功能）。
问题在于 Rust 具有 _ 在类型系统中 _ 存在的类型，但 _ 没有语法可以实际编写该类型 _。 这意味着您的代码 _ 只要推断出类型 _ 就可以工作。 然而，由于没有办法实际 _ 编写 _ 您正在使用的类型，因此一旦您需要添加显式类型注释，您就会完全卡住。
异步流在这里尤其糟糕，因为 a) 它们往往具有复杂的类型，特别是如果您链接多个流操作，并且 b) 通常无法编写涉及的任何类型。 调试使用异步流的 Rust 代码中的错误是一种令人沮丧的练习，通常包括盯着代码并进行随机调整，直到某些东西编译。
有一次，我浪费了大量时间尝试添加显式类型注释，以缩小我正在处理的某些流代码中的类型错误的原因。 我甚至尝试将其分解并添加 Boxes，以便可以使用 dyn Trait，但我 _ 仍然 _ 无法通过显式类型使其工作，并且仍然不知道原始编译错误的原因。 我最终不得不完全重写有问题的代码以完全停止使用流，因为无法调试编译错误。
但不要再发牢骚了。 这里的重点是你不应该这样做。 ** 任何可以推断的类型也必须可以显式地编写 **。
这比您想象的要困难
避免像 Rust 那样将 _ 有意 _ 不可写的类型放入您的语言是好的第一步。 然而，这本身是不够的，因为也很容易 _ 意外 _ 地拥有不可写的类型。
每个可推断的类型也必须可以显式表达的要求意味着类型检查器不能具有任何 _ 特殊能力 _，使其能够执行无法在类型语法中完成的操作。 总会有一种诱惑，即说“哦，让我们只是向类型检查器添加这个额外的分析，这将解决一个常见的痛点并允许编译更多正确的代码。” 但是，除非您 _ 也 _ 添加相应的显式类型语法（您通常不会这样做，因为这会使语言“更复杂”），否则您只是违反了此规则。
意外违规
事实上，即使您故意尝试遵循此规则，如果您不小心，也很容易违反此规则。
在 PolySubML 的设计过程中，此规则是一个主要考虑因素，我什至添加了一个额外的功能（类型联合和交集）到类型语法中，只是为了在一个特定的边缘情况下使必要的类型可表达。 即使这样，我 _ 仍然 _ 搞砸了！
在 PolySubML 的原始版本中，以下代码已编译：
let ref = {mut v: _(* ??? *) =`None 0};
let {type t; a: t; b: t->t} = {a=3; b=fun x->x+1};
ref.v <- `Some a;
match ref.v with
| `Some a -> b a
| `None _ -> 0
;
此代码没有任何实际的 _ 类型冲突 _，那么问题是什么？ 问题在于它正在推断无法编写的类型。
具体来说，无法为第一行中字段 v 编写任何注释（其中 ???）。 v 的 _ 推断 _ 类型为 ``(Some t)，其中 t 是由第 2 行的模式匹配创建的抽象类型。 然而，由于 t 仅在第 2 行 _ 定义 _，因此用户无法在第 1 行的注释中显式地编写它。编译器正在推断无法编写的类型，这正是我努力避免的！
因此，我不得不修改 PolySubML，以确保它只能推断 _ 在被推断的推断变量的点范围内 _ 的类型，以保证用户可以在他们愿意的情况下在该点显式地编写该类型。 今天在 PolySubML 中编译相同的代码会导致类型错误，从而满足规则 4。
规则 5：不要在运行时执行模型中包含静态类型推断
我不会在这里说太多，因为我已经写了一篇 关于该主题的整篇博文，但我认为我应该为了完整起见在这里提到这一点，因为这是另一个常见的设计问题，会导致类型推断以复杂和令人惊讶的方式运行，从而导致类型推断的坏名声。
结论
类型推断因令人困惑且无法调试的类型错误而闻名。 然而，没有理由必须如此。 如果您以正确的方式设计语言，即使使用强大的全局类型推断，您仍然可以获得高质量的类型错误。 这确实意味着要避免某些通常很方便的功能，但我认为从长远来看，在您的语言中拥有高质量的错误消息是更好的权衡。