在2022年，我们宣布了为Elixir添加集合理论类型的努力。在2023年6月，我们发表了一篇关于Elixir类型系统设计的获奖论文，并表示我们的工作正在从研究过渡到开发。通过Elixir v1.20，我们完成了第一个开发里程碑，即对每个Elixir程序进行类型推断和逐渐类型检查，而无需引入类型注释。这意味着Elixir逐渐能够报告死代码和验证过的错误：在运行时执行时 guaranteed 失败的类型违规。Elixir能够高效地找到现有程序中的验证错误，而不增加开发者的负担，并且虚假警报率极低。在本公告中，我们将详细说明类型系统的目标，dynamic()类型在Elixir中的含义以及它如何找到验证错误。特别是，我们的实现性能良好，在“如果T：类型收窄基准”基准测试中，Elixir通过了13个类别中的12个，这表明它能够从普通的Elixir代码中恢复精确的类型信息，我们用它来找到动态类型程序中的验证错误。类型系统得益于CNRS与Remote之间的合作。开发工作目前由Fresha和Tidewave赞助。我的Elixir中有类型？我们的目标是引入一个类型系统，其特点是：健全 - 类型系统推导和分配的类型与程序行为一致；逐渐 - Elixir的类型系统包括dynamic()类型，当变量或表达式在运行时检查时可以使用。在没有dynamic()的情况下，Elixir的类型系统表现为静态类型；开发者友好 - 类型的描述、实现和组合采用基本集合操作：并、交、非（因此它是一个集合理论类型系统），并提供明确的错误消息。将类型系统引入现有语言是一项复杂的变更。基于这个原因，我们的第一个里程碑是实现类型系统，而不引入类型注释，同时通过查找死代码和验证错误来为开发者提供价值。这是通过dynamic()类型完成的，dynamic()在Elixir中与其他逐渐类型化语言有很大不同。我们来逐步讲解dynamic()类型。许多逐渐类型系统都有any()类型，从类型系统的角度来看，通常意味着“可以做任何事情”，不会报告任何类型违规。另一方面，Elixir的逐渐类型称为dynamic()，它具有两个重要属性：兼容性和收窄。在静态类型系统中，当你有一个形状为integer()或binary()的类型，并且你调用一个函数时，该函数必须接受这两种类型。然而，由于类型系统无法精确捕捉我们所有程序的意图，这可能导致误报。例如，考虑下面的简单代码：def percentage_or_error (value) when is_integer (value) do value_or_error = if value > 1 then value else "not well" end # ... 更多代码 ... if value > 1 then value_or_error / 100 else String.upcase(value_or_error) end end 尽管value_or_error的类型是integer()或binary()，但是运算符/仅接受数字，而String.upcase仅接受二进制/字符串，上述程序仍然是有效的，并且在运行时不会抛出异常。然而，类型系统仍会报告两个违规，因为/和String.upcase所提供的类型不是接受的类型的子类型。虽然上面的程序可以更好地编写以消除所有类型违规，但类型系统始终会拒绝有效的程序，如果Elixir在现有代码库中引入了过多的误报，它将迅速侵蚀对类型系统的信任。因此，Elixir的逐渐类型系统将value_or_error变量标记为dynamic(integer()或binary())类型，这意味着在运行时类型可以是integer()或binary()。在调用带有dynamic()类型的函数时，Elixir仅在提供的类型和接受的类型不相交时才会发出类型违规。在上面的程序中，即使/仅期望数字，dynamic(integer()或binary())仍然可以是integer()，并且由于接受的类型和提供的类型没有不相交，因此没有类型违规。然而，如果我们将程序更改为：value_or_error = if value > 1 then value else "not well" end Map.fetch!(value_or_error, :some_key) 因为Map.fetch!期望一个map数据结构，而value_or_error在运行时只能是integer或binary，因此接受的类型和提供的类型是不相交的，这就变成了一个违规。这被称为兼容性属性，解释了Elixir如何仅报告验证错误。然而，仅报告验证错误并没有用，前提是我们无法在第一时间找到许多错误。我们通过确保Elixir的动态类型可以被收窄来解决这个问题。考虑这段代码：def add_a_and_b (data) do data.a + data.b end 在上面的程序中，data