Elixir 1.17 的类型系统

前言

差不多在一年半以前，Elixir 的作者 José Valim 计划给 Elixir 引入类型系统，我已经期待了很久。随着最近 Elixir 1.17 的第一个 RC 版本发布，终于可以初步窥探其效果了。

本文将参考官方的资料并用实际代码，尝试解读引入类型系统后的一些变化。

现状

目前社区主要使用 Dialyzer 和 Typespec 注释来获得一定程度上的类型安全保障。它的作用比较有限，据我观察很多 Elixir 官方团队参与的项目都不使用 Dialyzer。当然即使如此编写 @spec 注释仍然是一个很好的习惯，因为它能起到辅助文档生成的作用。

现在类型系统被引入编译器，并且是渐进式的。这意味着它会以编译警告而不是编译失败的形式展现。所以类型系统的引入并不意味着带来显著的不兼容。更重要的，我们不再需要 Dialyzer，我们有内置的更强大的方案。

当前的局限

如上所述，目前 Elixir 使用 Erlang 的 Tyepspec，通过独立的 Dialyzer 工具找出一些明确的错误。一方面 Dialyzer 的能力有限，只对一些明确的类型冲突产生错误提示。并且这个工具的错误信息相当不友好。另一方面 Typespec 自身表达能力也有局限（下面会讲）。而 Elixir 的类型系统在编译层面能给出更友好的提示，并具有更强大的类型表现力。

假设我们有这样一个函数：

@spec negate(integer()) :: integer()
def negate(x) when is_integer(x), do: -x

传递 integer() 类型的参数，返回 integer() 类型的值。因为它十分简单，用 Typespec 描述此函数的类型是绰绰有余的。

现在，这个函数多了一个子句：

@spec negate(integer() | boolean()) :: integer() | boolean()
def negate(x) when is_integer(x), do: -x
def negate(x) when is_boolean(x), do: not x

现在这个函数的类型相当于 (integer() | boolean() -> integer() | boolean())。你可能想说，貌似我们的 Typespec 也能描述它？是的，确实可以，但不够合理。

很显然我们的 negate/1 函数，在接收到 integer() 类型的参数时只会返回 integer()，而不是 integer() or boolean()。类似的，接收到 boolean() 参数时也不会返回 integer()。准确的说，这个函数应该用两个 @spec 才能精确表达：

@spec negate(integer()) :: integer() # <- 类型一
@spec negate(boolean()) :: boolean() # <- 类型二

我们需要这样的类型规范：(integer() -> integer()) and (boolean() -> boolean())。这就是 Typespec 的局限性，很多时候它只能表达出模糊的函数类型。

语义子类型

上面提到的 (integer() -> integer()) 和 (boolean() -> boolean()) 从语义的角度，都是 (integer() | boolean() -> integer() | boolean()) 的子类型。这种子类型关系并不需要显式定义，在这个框架内可以引出一种称作集合论类型的系统。

例如，所有的数字都是 integer() 的语义子类型，所有的原子都是 atom() 的语义子类型。同时原子 :foo、:bar 各自也可以视作独立的类型，被称作单例类型（代表单个值的类型）。

集合论类型

上个章节提到的 integer() 和 atom() 都属于集合论中的并集，它们是一组值的集合。除此之外还有类型的交集和差集。实际上 (integer() -> integer()) and (boolean() -> boolean()) 就是交集的体现，它是语义上并不兼容的两个类型的集合。

假设有以下类型：

(not (false or nil) -> false)

按照集合论，此处的 not (false or nil) 的含义是除了 false 和 nil 以外的所有类型的集合。包括所有非 atom() 类型和除了 false 和 nil 以外的所有原子。这便是差集的体现。

按照集合论，类型即集合。兼容的子类型或单例类型才可以通过类型安全检查。集合论基本可以算是 Elixir 类型系统的核心理论和设计，基于集合论让类型系统的表现力更加精确和强大。

更多

本文正在更新中，当前完成度大约 55%。请等待更新。