为何Erlang的Dialyzer无法检测状态差异？如何增强检查严格性？

问题描述 #

我在以下MVR代码上运行Dialyzer，test_function中除IncorrectMap外均通过检测。但我在case分支中故意返回不同的PlayersMapNew，却未被Dialyzer识别，这是为何？如何让Dialyzer对代码检查更严格，以便更易管理和跟踪状态？此外，我不确定当前的map类型检查是否符合文档规范（相关文档较为匮乏），能否对map的单个键进行正确性检查？

-module(example_module).

-export([my_function/1, state_changer/3, test_function/0]).

-type map_arg() :: #{key1 => integer(), key2 => atom()}.
-type move() :: rock | paper | scissor.
-type playersmap() :: #{players => {pid(), pid()}} | #{players => {pid(), pid()}, fst_mover => {{pid(),_}, move()}}.


-spec my_function(Map_arg :: map_arg()) -> ok.

my_function(Map) ->
    ok.

test_function() ->
    CorrectMap = #{key1 => 1, key2 => 'value'},
    IncorrectMap = #{key1 => 1, key2 => 2},
    my_function(CorrectMap),
    my_function(IncorrectMap),
    state_changer({move, rock}, {self(), tag}, #{players  => {self(), self()}, fst_mover => {{self(), tag}, scissor}}).


-spec state_changer({move, Choice :: move()}, From :: {pid(), _}, PlayersMap :: playersmap()) -> {reply, playersmap()}.
state_changer({move, Choice}, From, PlayersMap) ->        
    {CurId, _} = From,    
    {P1Id, P2Id} = maps:get(players, PlayersMap),
    case CurId of
        P1Id ->                        
            PlayersMapNew = maps:put(fst_mover, {From, Choice}, PlayersMap),                    
            {reply, PlayersMapNew};
        P2Id -> 
            PlayersMapNew = maps:put(fst_mover, {Choice, From}, PlayersMap),                    
            {reply, PlayersMapNew}
    end.

核心原因是你的playersmap()类型定义使用了开放map语法（=>），其中第一个分支#{players => {pid(), pid()}}表示：只要包含players键的map，无论是否有其他键、其他键的值类型是什么，都属于该类型。

在P2Id分支中，你将fst_mover设为{Choice, From}（类型为{move(), {pid(), _}}），虽然这不符合playersmap()第二个分支中fst_mover的类型定义{{pid(),_}, move()}，但该map仍然满足第一个分支的条件（包含players键），因此Dialyzer认为返回值符合playersmap()的联合类型，不会触发错误。

（1）使用精确map类型（Closed Maps） #

将类型定义中的=>替换为:=，强制map只能包含指定的键，且键值类型必须严格匹配。修改后的playersmap()定义：

-type playersmap() :: #{players := {pid(), pid()}} 
                    | #{players := {pid(), pid()}, fst_mover := {{pid(),_}, move()}}.

这样，当你在P2Id分支中放入类型错误的fst_mover值时，Dialyzer会立即检测到该map不属于playersmap()的任何分支，触发类型不匹配错误。

（2）启用严格警告选项 #

在项目的rebar.config中配置Dialyzer的严格警告规则，例如：

{dialyzer, [
    {warnings, [
        unmatched_returns,
        error_handling,
        race_conditions,
        underspecs,
        overspecs,
        no_undefined_callbacks
    ]}
]}.

这些选项会让Dialyzer检测未处理的返回值、错误处理遗漏、竞态条件、类型规格不完整/过度定义等问题，大幅提升检查严格性。

（3）细化类型规格 #

为函数的输入输出类型做更精确的定义，比如将state_changer的返回类型根据分支做更细致的区分（如果业务逻辑允许），或者使用-spec明确约束每个分支的返回值类型。

Erlang的类型系统支持针对单个键的严格检查，主要通过以下方式实现：

（1）精确map类型约束 #

使用:=语法指定必须存在的键及其类型，例如：

-type player_state() :: #{players := {pid(), pid()}, fst_mover => {{pid(),_}, move()}}.

这里players键是必须存在且类型严格为{pid(), pid()}，fst_mover是可选键，但如果存在则必须符合{{pid(),_}, move()}类型。

（2）结合maps:get/2与类型注解 #

在代码中通过maps:get/2获取键值时，Dialyzer会自动检查键是否存在于map类型中，同时验证值的类型。例如你代码中的{P1Id, P2Id} = maps:get(players, PlayersMap)，如果PlayersMap的类型定义中明确players键的类型，Dialyzer会检查该操作的合法性。

（3）使用map()的子类型约束 #

如果只需要检查单个键的类型，无需限制其他键，可以定义：

-type has_players() :: #{players := {pid(), pid()}}.

任何包含players键且值类型符合的map都属于该类型，其他键不受约束。

内容的提问来源于stack exchange，提问作者Piskator