Почему Dialyzer не находит этот код неверным?

Question

Я создал фрагмент ниже на основе этого урока. Последние две строки (feed_squid(FeederRP) а также feed_red_panda(FeederSquid)) явно нарушают определенные ограничения, но Dialyzer находит их в порядке. Это довольно обидно, потому что это именно тот тип ошибок, который я хочу уловить с помощью инструмента, выполняющего статический анализ.

В уроке есть объяснение:

Прежде чем вызвать функции с неправильным типом фидера, они сначала должны быть вызваны с правильным видом. Начиная с R15B01, Dialyzer не обнаружит ошибку с этим кодом. Наблюдаемое поведение состоит в том, что как только вызов данной функции будет выполнен в теле функции, Dialyzer будет игнорировать последующие ошибки в той же единице кода.

В чем причина такого поведения? Я понимаю, что философия успешной типизации заключается в том, чтобы "никогда не плакать, волк", но в текущем сценарии Dialyzer явно игнорирует намеренно определенные спецификации функций (после того, как он видит, что функции были вызваны правильно ранее). Я понимаю, что код не приводит к сбою во время выполнения. Могу ли я как-то заставить Dialyzer всегда серьезно относиться к спецификациям моей функции? Если нет, есть ли инструмент, который может это сделать?

-module(zoo).
-export([main/0]).

-type red_panda() :: bamboo | birds | eggs | berries.
-type squid() :: sperm_whale.
-type food(A) :: fun(() -> A).

-spec feeder(red_panda) -> food(red_panda());
            (squid) -> food(squid()).
feeder(red_panda) ->
    fun() ->
            element(random:uniform(4), {bamboo, birds, eggs, berries})
    end;
feeder(squid) ->
    fun() -> sperm_whale end.

-spec feed_red_panda(food(red_panda())) -> red_panda().
feed_red_panda(Generator) ->
    Food = Generator(),
    io:format("feeding ~p to the red panda~n", [Food]),
    Food.

-spec feed_squid(food(squid())) -> squid().
feed_squid(Generator) ->
    Food = Generator(),
    io:format("throwing ~p in the squid's aquarium~n", [Food]),
    Food.

main() ->
    %% Random seeding
    <<A:32, B:32, C:32>> = crypto:rand_bytes(12),
    random:seed(A, B, C),
    %% The zoo buys a feeder for both the red panda and squid
    FeederRP = feeder(red_panda),
    FeederSquid = feeder(squid),
    %% Time to feed them!
    feed_squid(FeederSquid),
    feed_red_panda(FeederRP),
    %% This should not be right!
    feed_squid(FeederRP),
    feed_red_panda(FeederSquid).

Answer 1

Немного сворачивая пример, у меня есть две версии:

Первый, который Dialyzer может поймать:

-module(zoo).
-export([main/0]).

-type red_panda_food() :: bamboo.
-type squid_food()     :: sperm_whale.

-spec feed_squid(fun(() -> squid_food())) -> squid_food().
feed_squid(Generator) -> Generator().

main() ->
    %% The zoo buys a feeder for both the red panda and squid
    FeederRP = fun() -> bamboo end,
    FeederSquid = fun() -> sperm_whale end,
    %% CRITICAL POINT %%
    %% This should not be right!
    feed_squid(FeederRP),
    %% Time to feed them!
    feed_squid(FeederSquid)

Тогда тот без предупреждений:

    [...]
    %% CRITICAL POINT %%
    %% Time to feed them!
    feed_squid(FeederSquid)
    %% This should not be right!
    feed_squid(FeederRP).

Диализатор предупреждает о версии, которую он может поймать:

zoo.erl:7: The contract zoo:feed_squid(fun(() -> squid_food())) -> squid_food() cannot be right because the inferred return for feed_squid(FeederRP::fun(() -> 'bamboo')) on line 15 is 'bamboo'
zoo.erl:10: Function main/0 has no local return

... и это случай, когда вы предпочитаете доверять собственному суждению против более жесткой спецификации пользователя.

Для версии, которую он не ловит, Dialyzer предполагает, что feed_squid/1 тип аргумента fun() -> bamboo это супертип fun() -> none() (закрытие, которое приведет к сбою, которое, если не вызывается в течение feed_squid/1, по-прежнему является действительным аргументом). После того, как типы были выведены, Dialyzer не может знать, действительно ли в функции вызывается переданное закрытие или нет.

Диализатор по-прежнему выдает предупреждение, если опция -Woverspecs используется:

zoo.erl:7: Type specification zoo:feed_squid(fun(() -> squid_food())) -> squid_food() is a subtype of the success typing: zoo:feed_squid(fun(() -> 'bamboo' | 'sperm_whale')) -> 'bamboo' | 'sperm_whale'

... предупреждение о том, что ничто не мешает этой функции управлять другим устройством подачи или любым другим устройством подачи! Если этот код проверяет ожидаемый ввод / вывод замыкания, а не является общим, то я вполне уверен, что Dialyzer поймает злоупотребление. С моей точки зрения, гораздо лучше, если ваш реальный код проверяет ошибочный ввод, а не полагается на спецификации типов и Dialyzer (который никогда не обещал найти все ошибки).

ВНИМАНИЕ: ГЛУБОКАЯ ЭЗОТЕРНАЯ ЧАСТЬ СЛЕДУЕТ!

Причина, по которой ошибка сообщается в первом случае, но не во втором, связана с прогрессом локального уточнения модуля. Изначально функция feed_squid/1 имеет успех набрав (fun() -> any()) -> any(), В первом случае функция feed_squid/1 сначала будет уточнено только с FeederRP и обязательно вернусь bamboo немедленно опровергнуть спецификацию и прекратить дальнейший анализ main/0, Во втором, функция feed_squid/1 сначала будет уточнено только с FeederSquid и обязательно вернусь sperm_whale затем уточняется обоими FeederSquid а также FeederRP и вернуться sperm_whale ИЛИ ЖЕ bamboo, Когда тогда позвонил с FeederRP ожидаемое возвращаемое значение при успешном наборе sperm_whale ИЛИ ЖЕ bamboo, Спецификация тогда обещает, что это будет sperm_whale и Dialyzer принимает это. С другой стороны, аргумент должен быть fun() -> bamboo | sperm_whale с точки зрения успеха, это fun() -> bamboo так что остается только с fun() -> bamboo, Когда это проверено по спецификации (fun() -> sperm_whale Диализатор предполагает, что аргумент может быть fun() -> none(), Если вы никогда не вызываете переданную функцию в течение feed_squid/1 (то, что система типов Dialyzer не хранит в качестве информации), и вы обещаете в спецификации, что вы всегда будете возвращать sperm_whale, Все отлично!

То, что может быть "исправлено", так это то, что система типов может быть расширена, чтобы отмечать, когда замыкание, которое передается в качестве аргумента, фактически используется в вызове, и предупреждать в случаях, когда единственным способом "выжить" некоторая часть вывода типа является быть fun(...) -> none(),

Answer 2

(Обратите внимание, я немного размышляю здесь. Я не читал код диализатора подробно).

"Нормальная" полноценная проверка типов имеет то преимущество, что проверка типов решаема. Мы можем спросить "Правильно ли напечатана эта программа" и получить ответ "Да" или "Нет" в ответ на завершение проверки типов. Не так для диализатора. По сути, дело в том, чтобы решить проблему остановки. Следствием этого является то, что будут программы, которые явно ошибочны, но все же проскальзывают через ручки диализатора.

Впрочем, это не один из таких случаев:)

Проблема двоякая. Тип успеха говорит: "Если эта функция завершается нормально, каков ее тип?". В приведенном выше нашем feed_red_panda/1 функция завершается для любого совпадения аргумента fun (() -> A) для произвольного типа A, Мы могли бы позвонить feed_red_panda(fun erlang:now/0) и это тоже должно работать. Таким образом, наши два вызова функции в main/0 не вызывает проблемы. Они оба заканчиваются.

Вторая часть проблемы - "Ты нарушил спецификацию?". Обратите внимание, что часто спецификации не используются в диализаторе как факт. Он выводит сами типы и использует шаблоны вывода вместо вашей спецификации. Всякий раз, когда вызывается функция, она аннотируется параметрами. В нашем случае это будет аннотировано двумя типами генераторов: food(red_panda()), food(squid()), Затем выполняется локальный анализ функции на основе этих аннотаций, чтобы выяснить, нарушили ли вы спецификацию. Поскольку в аннотациях присутствуют правильные параметры, мы должны предположить, что функция используется правильно в некоторой части кода. То, что он также вызывается с помощью кальмаров, может быть артефактом кода, который никогда не вызывается из-за других обстоятельств. Поскольку мы являемся локальными по функциям, мы не знаем и не вызываем сомнений у программиста.

Если вы измените код, чтобы сделать неправильный вызов только с генератором squid, то мы обнаружим несоответствие спецификации. Потому что мы знаем, что единственно возможный вызов сайта нарушает спецификацию. Если вы перенесете неправильный вызов в другую функцию, он также не будет найден. Потому что аннотация все еще на функции, а не на сайте вызова.

Можно представить себе будущий вариант диализатора, который учитывает тот факт, что каждый колл-сайт может обрабатываться индивидуально. Поскольку диализатор также со временем меняется, возможно, он сможет справиться с этой ситуацией в будущем. Но в настоящее время это одна из ошибок, которая проскользнет.

Главное, заметить, что диализатор нельзя использовать как "средство проверки правильности набора". Вы не можете использовать его для навязывания структуры в ваших программах. Вы должны сделать это самостоятельно. Если вам нужна дополнительная статическая проверка, возможно, можно было бы написать средство проверки типов для Erlang и запустить его на частях вашей базы кода. Но вы столкнетесь с проблемами при обновлении и распространении кода, с которыми нелегко справиться.