Why Erlang Dialyzer cannot find type error in the following code? -


free_vars_in_dterm({var, v}) -> {var, v}; cannot type check, however, dialyzer says ok. $ dialyzer *erl checking whether plt ~/.dialyzer_plt up-to-date... yes proceeding analysis... done in 0m0.66s done (passed successfully)

code below:

-module(formulas).  -type formulas() :: {predicate(), [dterm()]}                   | {'~', formulas()}                   | {'&', formulas(), formulas()}                   | {'|', formulas(), formulas()}                   | {'->', formulas(), formulas()}                   | {'<->', formulas(), formulas()}                   | {'exist', variable(), formulas()}                   | {'any', variable(), formulas()}.  -type dterm() :: constant()                | variable()                | {func(), [dterm()]}.  -type constant() :: {const, atom()}                   | {const, integer()}.  -type variable() :: {var, atom()}.  -type func() :: {function,                  function_name::atom(),                  arity::integer()}.  -type predicate() :: {predicate,                       predicate_name::atom(),                       arity::integer()}.   -include_lib("eunit/include/eunit.hrl").  -export([is_ground/1, free_vars/1, is_sentence/1]).  -spec is_ground(formulas()) -> boolean(). is_ground({_, {var, _}, _}) -> false; is_ground({{predicate, _, _}, terms}) ->     lists:all(fun is_ground_term/1, terms); is_ground(formulas) ->     ts = tuple_size(formulas),     lists:all(fun is_ground/1, [element(i, formulas)                                 || <- lists:seq(2, ts)]).  -spec is_ground_term(dterm()) -> boolean(). is_ground_term({const, _}) -> true; is_ground_term({var, _}) -> false; is_ground_term({{function, _, _}, terms}) ->     lists:all(fun is_ground_term/1, terms).   -spec is_sentence(formulas()) -> boolean(). is_sentence(formulas) ->     sets:size(free_vars(formulas)) =:= 0.  -spec free_vars(formulas()) -> sets:set(variable()). free_vars({{predicate, _, _}, dterms}) ->     join_sets([free_vars_in_dterm(dterm)                || dterm <- dterms]); free_vars({_qualify, {var, v}, formulas}) ->     sets:del_element({var, v}, free_vars(formulas)); free_vars(compound_formulas) ->     tp_size = tuple_size(compound_formulas),     join_sets([free_vars(element(i, compound_formulas))                || <- lists:seq(2, tp_size)]).  -spec free_vars_in_dterm(dterm()) -> sets:set(variable()). free_vars_in_dterm({const, _}) -> sets:new(); free_vars_in_dterm({var, v}) -> {var, v}; free_vars_in_dterm({{function, _, _}, dterms}) ->     join_sets([free_vars_in_dterm(dterm)                || dterm <- dterms]).  -spec join_sets([sets:set(t)]) -> sets:set(t). join_sets(set_list) ->     lists:foldl(fun (t, acc) -> sets:union(t, acc) end,                 sets:new(),                 set_list).

first short answer, using dialyzer's maxims :

  1. dialyzer never wrong. (recited erlang programmers)
  2. dialyzer never promised find errors in code. (not famous)

maxim number 2 (admittedly not satisfying) "standard" answer "why dialyzer didn't catch error" question.

more explanatory answer:

dialyzer's analysis return values of functions doing over-approximations. result, value included in types should considered "maybe returned" value. has unfortunate side-effect values going returned (such {var, v} tuple) considered "maybe returned". dialyzer must guarantee maxim 1 (never wrong), in cases unexpected value "may returned" not give warning, unless none of specified values can returned. last part checked @ level of entire function, , since in example of clauses indeed return sets, no warnings generated.


Comments

Post a Comment

Popular posts from this blog

javascript - Clear button on addentry page doesn't work -

this addentry blog page have made scratch , there underlying problems code particularly clear button supposed clear text entered when button clicked on doesn't work have saved html file problem. also 1 other problem submit button works doesn't pass of text index file have written php , reason whenever click on submit button redirects me index page without posting entry have made. <!doctype html> <html> <head> <script> function message() { alert("clear form?"); } </script> <style> body {background-color: beige;} h1 {color: black;} p {color: black;} textarea { width: 50%; height: 150px; padding: 12px 20px; box-sizing: border-box; border: 2px solid #ccc; border-radius: 4px; background-color: white; font-size: 16px; resize: none; } div { padding-left: 20px; } </style> </head> <meta charset="utf-8"> <link rel="stylesheet" href=".
Read more

c# - Selenium Authentication Popup preventing driver close or quit -

i have selenium automated task setup login website retrieve information. it's basic in automation. logging in , clicking 2 links. running issue proving problem. the site in question uses authentication required popup not javascript popup rather regular windows auth popup. have read isn't handled out of box selenium. i using " http://username:password@url.com " site every , site has issues on end prompt me again username/password randomly. have enter username/password twice in row when navigating there hand. since task loops continuously few hours picking needed info figured use webdriverwait verify element present on page. if authentication popup appears, element isn't present. no need care run, start over. the problem having when authentication popup displayed , hit timeout limit want close driver/browser window can start task on again. however, driver.close() , driver.quit() not doing anything. browser remains open , unloaded page still there login p
Read more

tensorflow when input_data MNIST_data , zlib.error: Error -3 while decompressing: invalid block type -

i'm geting started tensorflow,followed tutorials,but cannot download mnist data. import tensorflow tf tensorflow.examples.tutorials.mnist import input_data mnist=input_data.read_data_sets("mnist_data/",one_hot=true) print("download done!") error information: extracting mnist_data/train-images-idx3-ubyte.gz traceback (most recent call last): file "/home/sj/program/tesorflow_try.py", line 6, in <module> mnist=input_data.read_data_sets("mnist_data/",one_hot=true) file "/usr/local/lib/python2.7/dist-packages/tensorflow/contrib/learn/python/learn/datasets/mnist.py", line 213, in read_data_sets train_images = extract_images(f) file "/usr/local/lib/python2.7/dist-packages/tensorflow/contrib/learn/python/learn/datasets/mnist.py", line 60, in extract_images buf = bytestream.read(rows * cols * num_images) file "/usr/lib/python2.7/gzip.py", line 268, in read self._read(readsize) file
Read more