Elixir 类型规范和参数化类型变量

Elixir type specs and parameterized type variables

我想弄清楚如何在 Elixir 类型和函数规范中组合 参数化类型 类型变量 。作为一个简单的例子,假设我正在定义一个 Stack 模块:

defmodule Stack do
  @type t :: t(any)
  @type t(value) :: list(value)

  @spec new() :: Stack.t
  def new() do
    []
  end

  # What should the spec be?
  def push(stack, item) do
    [item|stack]
  end
end

使用第 3 行的参数化类型规范,我可以定义一个函数来创建一个新的堆栈,该堆栈应该只包含整数:

@spec new_int_stack() :: Stack.t(integer)
def new_int_stack(), do: Stack.new

到目前为止,还不错。现在我想确保只有整数可以被压入这个堆栈。例如,透析器应该没问题:

int_stack = new_int_stack()
Stack.push(int_stack, 42)

但是透析器应该抱怨这个:

int_stack = new_int_stack()
Stack.push(int_stack, :boom)

我不知道 push 函数的类型规范应该是什么来强制执行。在 Erlang 中,我很确定这种语法可以解决问题:

-spec push(Stack, Value) -> Stack when Stack :: Stack.t(Value).

有没有办法使用 Elixir 来表达这个约束 @spec

(我对纯 Erlang 比较流利,但代码应该很容易移植。)

如果你写一个单独的int_push/2(就像你写一个new_int_stack/0)那么你当然可以写:

-spec int_push(integer(), stack(integer())) -> stack(integer()).

这应该允许 Dialyzer 检测滥用,纯粹是因为 Item 参数被指定为 integer()

最接近通用规范的是:

-spec push(T, stack(T)) -> stack(T) when T :: term().

不幸的是,从 Erlang 18 开始,Dialyzer 并未从最严格的意义上阅读此规范(要求所有实例 T 是统一的)。它只需要每个 T 是一个 term().

因此,Erlang 或 Elixir 都不会发出警告。

Erlang 示例的完整代码:

-module(stack).

-export([new/0, new_int_stack/0, push/2, test/0]).

-type stack()  :: stack(any()).
-type stack(T) :: list(T).

-spec new() -> stack().

new() ->
  [].

-spec push(T, stack(T)) -> stack(T) when T :: term().

push(Item, Stack) ->
  [Item|Stack].

-spec new_int_stack() -> stack(integer()).

new_int_stack() ->
  new().

-spec test() -> ok.

test() ->
  A = new(),
  B = new_int_stack(),
  push(foo, B),
  ok.