Спецификации типа Эликсира и переменные параметризованного типа

Question

Я пытаюсь выяснить, как скомбинировать с параметризованными типами и переменными типа в спецификациях типа 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). 

Есть ли способ, чтобы выразить это ограничение с помощью эликсира @spec?

Answer 1

(. Я более свободно в простом 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 диализный не читает эту спецификацию в самом строгом смысле этого слова (требующем все экземпляры T быть unifiable). Это просто требует, чтобы каждый T был term().

Следовательно, никакие предупреждения не будут излучаться ни в Эрланге, ни в Эликсире.

Полный код примера в 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.