我已经根据this教程创建了以下代码段。最后两行(feed_squid(FeederRP)feed_red_panda(FeederSquid))显然违反了已定义的约束,但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).

最佳答案

最大限度地减少了示例,我有以下两个版本:

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).

Dialyzer对其可以捕获的版本的警告是:
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() -> bamboofun() -> none()的父类(super class)型(将崩溃的闭包,如果未在feed_squid/1中调用,则该闭包仍然是有效参数)。推断出类型之后,Dialyzer无法知道是否在函数内实际调用了传递的闭包。

如果使用了-Woverspecs选项,Dialyzer仍会发出警告:
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(它们从未 promise 过会发现所有错误),那就更好了。

警告:深部零件如下!

在第一种情况下报告错误但在第二种情况下报告错误的原因与模块局部优化的进度有关。最初,函数feed_squid/1可以成功键入(fun() -> any()) -> any()。在第一种情况下,首先仅使用feed_squid/1对函数FeederRP进行完善,并且肯定会返回bamboo,立即篡改规范并停止对main/0的进一步分析。在第二步中,首先将仅使用feed_squid/1完善函数FeederSquid,并且肯定会返回sperm_whale,然后同时使用FeederSquidFeederRP进行完善,然后返回sperm_whalebamboo。然后,使用FeederRP调用时,成功键入的期望返回值是sperm_whalebamboo。然后,该规范 promise 它将是sperm_whale,并且Dialyzer接受它。另一方面,该参数应为fun() -> bamboo | sperm_whale success-typing-wise,它为fun() -> bamboo,因此仅保留fun() -> bamboo即可。根据规范(fun() -> sperm_whale)进行检查时,Dialyzer假定该参数可以为fun() -> none()。如果您从不在feed_squid/1中调用传递的函数(Dialyzer的类型系统不保留此信息),并且您在规范中保证始终将返回sperm_whale,那么一切都很好!

可以“修复”的是类型系统可以扩展为在调用中实际使用作为参数传递的闭包时发出的警告,并在“幸存”类型推断的某些部分的唯一方法是警告的情况下发出警告成为fun(...) -> none()

10-06 13:51