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 各自也可以视作独立的类型,被称作单例类型(代表单个值的类型)。

类型系统的最终设计仅决定让每一个 atom() 具单例类型,而 integer() 是不可分割的。所以数字不可作为单例类型。

集合论类型

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

假设有以下类型:

(not (false or nil) -> false)

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

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

更多

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

作者头像 一点点入门知识 打赏作者
本文由作者按照 CC BY 4.0 进行授权
分享:

相关文章