josefs / gradualizer Goto Github PK
View Code? Open in Web Editor NEWA Gradual type system for Erlang
License: MIT License
A Gradual type system for Erlang
License: MIT License
We have a reasonably good test suite with a lot of unit tests and a few test programs. It's very helpful and I use it all the time. But sadly, there are many cases that are not covered by the test suite. We can make it even more helpful! It'd be wonderful if people wanted to help out with this. It's also a very easy way to help out this project. I'm happy to assist anyone who wants to make a contribution.
Checking the following file:
-module(docsh_internal).
-export([merge/1,
kna/1]).
-export_type([t/0,
item/0,
kna/0]).
-type t() :: #{name := module(),
items := [item()],
description => none | iodata()}.
-type item() :: #{kind := function | type,
name := atom(),
arity := arity(),
description => none | iodata(),
exported => boolean(),
signature => iodata()}.
-type kna() :: {function | type, atom(), arity()}.
-define(a2b(A), atom_to_binary(A, utf8)).
-define(a2l(A), atom_to_list(A)).
-define(i2b(I), integer_to_binary(I)).
-define(il2b(IOList), iolist_to_binary(IOList)).
%%
%%' Public
%%
-spec merge([Info]) -> MergedInfo when
Info :: t(),
MergedInfo :: t().
merge([]) -> [];
merge([Info]) -> Info;
merge([Info1, Info2 | Rest]) ->
case are_disjoint(Info1, Info2) of
false -> erlang:error(not_disjoint, [Info1, Info2 | Rest]);
true ->
(module(Info1) =:= module(Info2)
orelse erlang:error(different_modules, [Info1, Info2 | Rest])),
merge([merge_two(Info1, Info2) | Rest])
end.
-spec kna(item()) -> kna().
kna(#{kind := K, name := N, arity := A}) -> {K, N, A}.
%%.
%%' Internal
%%
-spec merge_two(t(), t()) -> t().
merge_two(#{items := Items1} = Info1, #{items := Items2}) ->
ItemsByKNA = dict:to_list( docsh_lib:group_by(fun kna/1, Items1 ++ Items2) ),
NewItems = lists:map(fun merge_two_/1, ItemsByKNA),
Info1#{items := NewItems}.
-spec merge_two_({kna(), [item()]}) -> item().
merge_two_({{Kind, Name, Arity}, [Item]}) ->
#{kind := Kind, name := Name, arity := Arity} = Item,
Item;
merge_two_({{Kind, Name, Arity}, [Item1, Item2]}) ->
#{kind := Kind, name := Name, arity := Arity} = Item1,
#{kind := Kind, name := Name, arity := Arity} = Item2,
maps:merge(Item1, Item2).
are_disjoint(Info1, Info2) ->
Module = maps:get(name, Info1),
Module = maps:get(name, Info2),
#{items := Items1} = Info1,
#{items := Items2} = Info2,
Items1 -- Items2 == Items1.
module(#{name := Name}) -> Name.
%%. vim: foldmethod=marker foldmarker=%%',%%.
I've run into the following error:
$ gradualizer src/docsh_internal.erl
src/docsh_internal.erl: The empty list on line 35 does not have type #{name := module(),
items := [item()],
description => none | iodata()}
escript: exception error: no match of right hand side value
#{'Dict' =>
[{user_type,[{file,"dict.erl"},{location,100}],
dict,
[{var,100,'Key'},{var,100,'Value'}]}],
'List' =>
[{type,101,list,
[{type,101,tuple,
[{var,101,'Key'},{var,101,'Value'}]}]}]}
in function typechecker:solve_bounds/4 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1182)
in call from typechecker:bounded_type_subst/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1166)
in call from typechecker:expect_fun_type1/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1037)
in call from typechecker:expect_intersection_type/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1095)
in call from typechecker:expect_fun_type1/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1058)
in call from typechecker:expect_fun_type/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1024)
in call from typechecker:type_check_expr/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1315)
in call from typechecker:type_check_expr/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1234)
A trace on solve_bounds
gives:
8> (<0.80.0>) call typechecker:solve_bounds({tenv,#{{item,0} =>
{[],
{type,14,map,
[{type,14,map_field_exact,
[{atom,14,kind},
{type,14,union,
[{atom,14,function},{atom,14,type}]}]},
{type,15,map_field_exact,
[{atom,15,name},{type,15,atom,[]}]},
{type,16,map_field_exact,
[{atom,16,arity},{type,16,arity,[]}]},
{type,17,map_field_assoc,
[{atom,17,description},
{type,17,union,
[{atom,17,none},{type,17,iodata,[]}]}]},
{type,18,map_field_assoc,
[{atom,18,exported},{type,18,boolean,[]}]},
{type,19,map_field_assoc,
[{atom,19,signature},{type,19,iodata,[]}]}]}},
{kna,0} =>
{[],
{type,21,tuple,
[{type,21,union,[{atom,21,function},{atom,21,type}]},
{type,21,atom,[]},
{type,21,arity,[]}]}},
{t,0} =>
{[],
{type,10,map,
[{type,10,map_field_exact,
[{atom,10,name},{type,10,module,[]}]},
{type,11,map_field_exact,
[{atom,11,items},
{type,11,list,[{user_type,11,item,[]}]}]},
{type,12,map_field_assoc,
[{atom,12,description},
{type,12,union,
[{atom,12,none},{type,12,iodata,[]}]}]}]}}},
#{}},#{'Dict' =>
[{user_type,[{file,"dict.erl"},{location,100}],
dict,
[{var,100,'Key'},{var,100,'Value'}]}],
'List' =>
[{type,101,list,
[{type,101,tuple,[{var,101,'Key'},{var,101,'Value'}]}]}]},[{acyclic,'Value'},{acyclic,'Key'},{acyclic,'List'},{acyclic,'Dict'}],#{})
(<0.80.0>) exception_from {typechecker,solve_bounds,4} {error,{badmatch,#{'Dict' =>
[{user_type,[{file,"dict.erl"},{location,100}],
dict,
[{var,100,'Key'},{var,100,'Value'}]}],
'List' =>
[{type,101,list,
[{type,101,tuple,
[{var,101,'Key'},
{var,101,'Value'}]}]}]}}}
My not so educated guess is that there's no complete support for maps or a bug there. Might it be the case?
-module(plus).
-spec m(+1) -> {}.
m(+1) ->
{}.
The pattern + 1 on line 4 doesn't have the type 1
Tying in with #56, it would be nice if I could open a PR which adds this test case as a known bug. Perhaps a known_problems/should_pass
and known_problems/should_fail
?
I think we should aim for something very simple and permissive here. Perhaps all we should check is that the pattern matches against a binary string and ignore the sizes in the types, at least at first.
In the JavaScript world, Flow and TypeScript can enable type checking on a per file basis in a project setup. This allows for gradual enabling of the type checker so that there is not an overwhelming amount of errors when starting out. Without a similar solution I think it will be difficult to add gradualizer to a big code base - especially if we do a good job with type inference.
First and foremost, I think this is a really great project! I especially like the speed it works with, since that makes it ideal for in-editor instant feedback.
I'm not sure if you're interested in this kind of reports at this stage - if not, please just ignore and close the issue. I've run Gradualizer on docsh and have got some crashes:
docsh_docs_v1.erl:
error: function_clause
stacktrace: [{typechecker,handle_type_error,
[{not_exported,remote_type,
{{atom,46,docsh_format},{atom,46,t},0}}],
[{file,"src/typechecker.erl"},{line,2640}]},
{typechecker,'-type_check_forms/2-fun-0-',5,
[{file,"src/typechecker.erl"},{line,2544}]},
{lists,foldr,3,[{file,"lists.erl"},{line,1276}]},
{erl_eval,do_apply,6,[{file,"erl_eval.erl"},{line,670}]},
{erl_eval,try_clauses,8,[{file,"erl_eval.erl"},{line,904}]},
{erl_eval,exprs,5,[{file,"erl_eval.erl"},{line,122}]},
{erl_eval,eval_lc1,6,[{file,"erl_eval.erl"},{line,696}]},
{erl_eval,eval_generate,7,[{file,"erl_eval.erl"},{line,725}]}]
docsh_beam.erl:
error: function_clause
stacktrace: [{typechecker,type_check_expr,
['*environment excluded*',
{remote,79,
{record_field,79,{var,79,'B'},docsh_beam,{atom,79,name}},
{atom,79,module_info}}],
[{file,"src/typechecker.erl"},{line,898}]},
{typechecker,do_type_check_expr_in,3,
[{file,"src/typechecker.erl"},{line,1597}]},
{typechecker,type_check_expr_in,3,
[{file,"src/typechecker.erl"},{line,1398}]},
{lists,zipwith,3,[{file,"lists.erl"},{line,451}]},
{lists,zipwith,3,[{file,"lists.erl"},{line,451}]},
{typechecker,type_check_call,5,
[{file,"src/typechecker.erl"},{line,1924}]},
{typechecker,do_type_check_expr_in,3,
[{file,"src/typechecker.erl"},{line,1598}]},
{typechecker,type_check_expr_in,3,
[{file,"src/typechecker.erl"},{line,1398}]}]
docsh_syntax.erl:
error: function_clause
stacktrace: [{typechecker,do_type_check_expr_in,
['*environment excluded*',
{var,1242,'Fun'},
{'fun',64,
{function,
{atom,64,docsh_syntax},
{var,64,'AttrName'},
{integer,64,1}}}],
[{file,"src/typechecker.erl"},{line,1401}]},
{typechecker,type_check_expr_in,3,
[{file,"src/typechecker.erl"},{line,1398}]},
{typechecker,'-type_check_call_ty/4-lc$^0/1-1-',2,
[{file,"src/typechecker.erl"},{line,1242}]},
{typechecker,type_check_call_ty,4,
[{file,"src/typechecker.erl"},{line,1242}]},
{typechecker,type_check_expr,2,
[{file,"src/typechecker.erl"},{line,975}]},
{typechecker,type_check_lc,3,
[{file,"src/typechecker.erl"},{line,1343}]},
{lists,map,2,[{file,"lists.erl"},{line,1239}]},
{lists,map,2,[{file,"lists.erl"},{line,1239}]}]
You can run the checks from the gradualizer
branch of docsh with make gradualizer
.
I realise you might be aware of these - if so, I'm looking forward to all the future improvements!
typechecker:handle_type_error({type_error,bin,0,
{user_type,[{file,"test_path.erl"},{location,24}],t,[]}}) (/home/overminddl1/erlang/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 2807)
It seems binary types are not being handled by the type error path? So should be a simple fix. Although the fact that the binary is not passed in like it is for strings/charlists seems odd? Also typelib:pp_type(Ty)
does not seem to add the remote module name to the type so I just get something like t()
instead of test_path:t()
or so, and with how common t
is as a type name that's not terribly helpful, plus just seeing t
isn't really helpful either, it would be nice to get a list of types drilled down. :-)
Coming from TypeScript I was curious why they choose to absorb T in T | any
which becomes any
.
The answer is simple: performance. Is there any literature on the implications of doing it as they do vs doing it as we do?
Is there a communication channel for just general discussion? I just wanted to have this in print and easily accessible - close when my meta question(s) are resolved!
I was happily surprised when Gradualizer pointed it out that I don't have to check for undefined
if my function expects just t1/0
(BTW, I was writing production code - this is just a minimised example):
-module(test).
-export([f/1]).
-type t1() :: binary().
-spec f(t1()) -> ok | error | other.
f(T) ->
case T of
undefined -> error;
_ -> other
end.
However, it puzzled me way more when I changed the code to the following and got The pattern <<"ok">> on line 12 doesn't have the type undefined | <<_:_*8>>
error:
-module(test).
-export([f/1]).
-type t1() :: binary().
-type maybe(T) :: undefined | T.
-spec f(maybe(t1())) -> ok | error | other.
f(T) ->
case T of
undefined -> error;
<<"ok">> -> ok;
_ -> other
end.
I'm not sure if it's a known issue. It resembles #16 a bit, but that one is already closed.
Hello!
I was wondering if there would be any interest in/possibility of adding Elixir support to Gradualizer?
Semantically they are near identical languages that use the same typespecs, so I feel the same tool could be applied to both. I can think of two main differences:
Elixir has Lisp style macros. To handle this type checking could be performed after macro resolution so no knowledge of that system is required.
Elixir has protocols, which are slightly similar to Haskell's typeclasses and have no equivalent in Erlang. This could be ignored, at least to start.
I've not yet read any of the Gradualizer source- does this feature seem realistic and achiveable?
Cheers,
Louis
A function can have multiple specs, which the documentation calls overloading and whose semantics is intersection types. For instance,
-spec foo(boolean()) -> its_a_bool;
(integer()) -> its_an_int.
means that foo
has both the type boolean() -> its_a_bool
and the type integer() -> its_an_int
.
We currently handle this for function definitions and explicit calls using the fun_ty_intersection
return value from expect_fun_type
, but not for fun F/A
and fun M:F/A
expressions. To do this we'd need to be able to represent intersection types in the type language.
This proposal is only about ergonomics and nothing to do with type-checker logic.
It was inspired by erl_types
but slightly outdated by recent introduction of type/1
/type/2
helper functions.
I propose to add helper macros like ?t_any
/t_list([?t_integer])
etc, see gomoripeti@2e1b256 (this is an outdated commit but before the effort to rebase it I wanted to ask the team if it makes sense or I should just dismiss it forever)
pros:
erl_anno:new(0)
all over the placetype(tuple)
when I really mean type(tuple, any)
(equivalent with ?t_tuple
)type/1/2
functions) it can also be used to match types ignoring second anno field (and optionally ignoring fourth field too)type()
can be (and with an IDE also autocomplete can work quite nicely like ?t_<TAB>
)cons:
I've started work on integrating Gradualizer with Vim.
A Neomake maker runs the gradualizer
EScript to obtain results for a file open in the current Vim buffer. The code path is extended with per-project ebin
dirs, so that the analysis results are relatively accurate.
For now, the changes are available below - it still requires some polishing, so I'm not creating PRs yet:
One thing that popped up in Gradualizer output is that line numbers are not placed consistently - I had to add a shell script to reformat them - that's the only change on the vim-integration
branch above.
@josefs do you think this could be addressed directly in Gradualizer (likely gradualizer_cli.erl
)? A format like this would be ideal (with on line 102 being redundant, but it doesn't hurt):
src/docsh_lib.erl:102: The type beam_lib:beam/0 on line 102 is not exported
src/docsh_lib.erl:114: The tuple on line 114 does not have type docsh_beam:debug_info() | false
A minimal example is:
-module(a).
-export([p/0]).
-spec p() -> ok.
p() -> ok.
-module(test).
-export([h/0]).
-import(a, [p/0]).
-spec h() -> ok.
h() -> p().
With Gradualizer producing:
test.erl: Call to undefined function p/0 on line 8
@gomoripeti in #53 wrote:
also could run make dialyze
Im not familiar with the new method and it probably needs to be done by a repo owner but would be nice to integrate travis with github PR checks (https://blog.travis-ci.com/2018-05-07-announcing-support-for-github-checks-api-on-travis-ci-com)
Would be nice if we follow up on that.
Should Gradualizer support extended numeric types like non_neg_integer()
, pos_integer()
and others? Currently Gradualizer returns :nok
in this example (Elixir)
@spec factorial(non_neg_integer()) :: pos_integer()
def factorial(0), do: 1
def factorial(n) do
n * factorial(n - 1)
end
Error is
The operator '*' on line 7 is given a non-numeric argument of type pos_integer()
Currently the following code
-spec test() -> {atom1, atom2} | atom3.
test() ->
case f() of
{atom1, _} = X -> X;
_ -> atom3
end.
-spec f() -> {atom1, atom2} | atom4.
f() ->
{atom1, atom2}.
gives me the error
The variable 'X' on line 7 has type {atom1, atom2} | atom4 but is expected to have type {atom1, atom2} | atom3
I believe type checking the return value of a function which is spec-ed to return term()
should always pass (the same way as being spec-ed to return any()
) as every type is a subtype of term()
. (this is of course an under-specification from the side of the user)
This works fine for certain expressions where the subtype
function is used, eg:
-spec return_float() -> term().
return_float() -> 1.23.
-spec return_string() -> term().
return_string() -> "asd".
However where the check uses the expect_*_type
family of functions, type checking fails, because these helper functions don't allow term()
.
-spec return_tuple() -> term().
return_tuple() -> {1, 2}.
-spec return_list() -> term().
return_list() -> [1, 2].
-spec return_record() -> term().
return_record() -> #rec{}.
yields:
The tuple on line 48 does not have type term()
The expression [1,2] on line 51 does not have type term()
The record #rec on line 54 is expected to have type term().
I'm willing to fix this, if this is indeed a bug, however I'm not sure if the expect_*_type
functions should be extended, or rather do_type_check_expr_in
should short-circuit for term()
the same way as for any()
?
In https://github.com/josefs/Gradualizer/pull/24#issuecomment-406861255` was mentioned that type_check_expr
should not return type in any case (currently it return a type other than any if expr is fun objection, function call, expr with clauses (try, case, receive etc), record or tuple).
The general behaviour of type_check_expr
is that it calls itself on subtypes of the expr and (maybe) type-checks the returned types. If the returned type is always any then what can this function check?
On a different note even type_check_expr_in
calls type_check_expr
to infer some type (eg in case Cond of Pattern -> ...
Pattern
is checked against the inferred type of Cond
). Type checking could be more powerful if more precise type would be inferred for more expressions (eg a float literal could be inferred to be of type float()
)
But maybe the two functionalities could be split:
type_check_expr
checks the type of expression in case there is no type information available (basically same as checking against the any() type - checking a dynamic program)infer_type_of_expr
would infer the type of the expression (this would have obviously limited scope and wouldn't go beyond the boundaries of function calls)But I might misunderstand the roles of the functions (I ignored collecting constraints). What am I missing?
When I run make gradualize
to gradualize the gradualizer itself, it crashes in typechecker.erl with the following error:
The variable 'Ty1' on line 60 has type type() but is expected to have type type()
I tried to solve it but I got confused. This is how far I got.
The first type()
is defined in typechecker (the currently checked module) while the second is defined in typelib
. (This can be seen by uncommenting some commented code in typelib:pp_type/1
which checks for filename annotation in the form and adds it to the output.)
So far so good. Next, to see what these type()
expand to, I modified the exception caught in subtype/4
from nomatch
to {nomatch, T1, T2}
and the corresponding throw
and printed out what exactly mismatches when comparing two types piece by piece. Now I can see that they are both normalized/expanded to {ann_type, anno(), [af_anno() | abstract_type()]}
(where the types are local to erl_parse). There is no function clause in compat_ty
for the case when both types are ann_type, but there is a clause that matches identical types compat_ty(T, T, A, _) -> ...
which should match here. I don't understand why it doesn't match. I am confused.
What am I missing?
There are modules in OTP which have really unfortunate type specs, from the point of view of Gradualizer. Take the function hd/1
for example. It has the following spec:
hd([term()]) -> term()
In Gradualizer, the type term()
is the top of the subtyping hierarchy, which means that the code that consumes the output of hd/1
has to account for every kind of value there is! In practice it means that all uses of this function will signal a type error. That's no good! A better type would be:
hd([any()]) -> any()
One way to solve this problem is to provide our own type specs for problematic modules in OTP. We could instrument gradualizer_db
to use its own set of specs instead of these modules.
A non-exhaustive list of problematic OTP modules
Given getenv/1
from OTP's os.erl
:
-spec getenv(VarName) -> Value | false when
VarName :: string(),
Value :: string().
getenv(_) ->
erlang:nif_error(undef).
The following code:
-spec get_so_path() -> binary() | string().
get_so_path() ->
case os:getenv("EJABBERD_SO_PATH") of
false ->
case code:priv_dir(mongooseim) of
{error, _} ->
".";
Path ->
filename:join([Path, "lib"])
end;
Path ->
Path %% this is line 77
end.
Results in:
The variable 'Path' on line 77 has type Value | false but is expected to have type binary() | string()
Which seems to be incorrect, since the first clause of the case
rules out false
, therefore Path
must be a string()
. I have a hunch this might be connected with this comment on type refinements, but my understanding of the theory is vague, to say the least :)
Surprisingly, the error persists in this case:
-spec get_so_path() -> binary() | string().
get_so_path() ->
case os:getenv("APP_SO_PATH") of
false ->
"/fake/default/path";
Path ->
Path
end.
But disappears when a binary literal is provided in the false
clause:
It did disappear due to Vim not being able to parse a Gradualizer crash message.
-spec get_so_path() -> binary() | string().
get_so_path() ->
case os:getenv("APP_SO_PATH") of
false ->
<<"/fake/default/path">>;
Path ->
Path
end.
Attempting to run make escript
on RedHat linux (which is locked to make
version GNU Make 3.82
with no alternatives on the main installs), and running make escript
gives this:
╰─➤ make escript
erlang.mk:30: Please upgrade to GNU Make 4 or later: https://erlang.mk/guide/installation.html
erlang.mk:30: Please upgrade to GNU Make 4 or later: https://erlang.mk/guide/installation.html
GEN escript-zip
WARNING: No more files
gradualizer
make: *** [escript-zip] Error 1
And the supplied link is useless as it says nothing about how to workaround the issue on modern RedHat installs (which regulate what can and cannot be installed).
One of the discussions in #83 regards type assertions. A good idea that spawned out of that (thanks @zuiderkwast!) was that adding an id
-function that accepts an extra dummy parameter representing a type would allow us to implement type assertions in an efficient and general way without the need to extend the language. To exemplify:
% defined in a header file, I suppose
assert_ty(V, _) -> V.
% Inferred spec: -spec foo(any()) -> integer().
foo(A) -> assert_ty(A, {type, integer}).
-spec bar(integer() | boolean()) -> integer().
% Trust me, due to "circumstances" I'm only ever called with integers...
bar(A) -> assert_ty(A, {type, integer}).
To provide nicer syntax for type assertions @zuiderkwast suggests a parse transform:
I think it is possible to write a parse transform which allows us to write type annotations on this form: '::'(42, pos_integer()).
[...]
Example: A call to '::'([42], nonempty_list(pos_integer())) is transformed into '::'([42], {type, 0, nonempty_list, [{type, 0, pos_integer, []}]}.
Discussion points:
any()
to represent any()
does not fly. Some ideas: the internal representation of types ('::'([42], {type, 0, nonempty_list, [{type, 0, pos_integer, []}]}
), structured data that needs to be massaged (if we add some helper functions, e.g. type(T) -> {type, T}
, this might turn out OK), or as a string (which we'll have to parse) e.g. '::'(42, "pos_integer()")
.These should all fail
-spec f(ok) -> ok.
f(10 = X) -> X.
-spec g(string()) -> ok.
g($a) -> ok.
-spec h(10..20) -> ok.
h(21) -> ok.
-spec i(integer()) -> ok.
i(1.0) -> ok.
Test case:
%% -spec h(_) -> apple | banana. % Same error with or without spec
h(1.0) -> banana;
h(_) -> apple.
Error
** exception error: no function clause matching typechecker:add_any_types_pat({float,14,1.0},#{}) (src/typechecker.erl, line 2542)
in function typechecker:add_type_pat/4 (src/typechecker.erl, line 2358)
in call from typechecker:add_types_pats/4 (src/typechecker.erl, line 2348)
in call from typechecker:check_clause/4 (src/typechecker.erl, line 2300)
in call from lists:map/2 (lists.erl, line 1239)
in call from typechecker:check_clauses/4 (src/typechecker.erl, line 2286)
in call from typechecker:check_clauses_fun/3 (src/typechecker.erl, line 2256)
in call from typechecker:'-type_check_forms/2-fun-0-'/5 (src/typechecker.erl, line 2680)
Hi @josefs!
Thanks for the great presentation at EUC. After watching it, I had some questions and I thought I would reach out to you. I decided to open up an issue so other folks can jump into the discussion and contribute/learn. If this is not the proper medium or if you would prefer me to ask them elsewhere, please let me know and I will do it.
The first one is about any()
and term()
. In the presentation, you made it clear they are not the same. However, it is not clear to me what are the practical implications. Do you have an example of a typespec that would be pass with any()
or not with term()
and vice-versa?
The second question is about typing checking when calling untyped functions. Imagine you have:
-spec foo(integer(), integer()) -> integer().
foo(A, B) -> another_module:bar(A, B).
Where another_module:bar/2
is not spec'ed. Does it mean you assume another_module:bar/2
returns any()
or do you perform partial evaluation in case another_module:bar/2
calls a typed function?
Thank you!
While running gradualizer on an a mature Elixir project, I got quite a few of these:
*********************************
Report this error to Gradualizer:
** (FunctionClauseError) no function clause matching in :typechecker.handle_type_error/1
The following arguments were given to :typechecker.handle_type_error/1:
# 1
{:type_error, :map, 151, {:type, 141, :union, [{:atom, 0, nil}, {:user_type, 141, :attract_file, []}]}}
/Users/jowens/dev/snoke/deps/gradualizer/src/typechecker.erl:3327: :typechecker.handle_type_error/1
/Users/jowens/dev/snoke/deps/gradualizer/src/typechecker.erl:3228: anonymous fn/5 in :typechecker.type_check_forms/2
(stdlib) lists.erl:1276: :lists.foldr/3
lib/gradualixir.ex:37: anonymous fn/2 in Gradualixir.gradualize/2
(elixir) lib/enum.ex:3281: Enumerable.List.reduce/3
(elixir) lib/enum.ex:1968: Enum.reduce_while/3
lib/mix/tasks/gradualizer.ex:25: Mix.Tasks.Gradualizer.run/1
(mix) lib/mix/task.ex:316: Mix.Task.run_task/3
(mix) lib/mix/cli.ex:79: Mix.CLI.run_task/2
(elixir) src/elixir_compiler.erl:71: :elixir_compiler.dispatch/4
(elixir) src/elixir_compiler.erl:68: :elixir_compiler.compile/3
(elixir) src/elixir_lexical.erl:17: :elixir_lexical.run/2
(elixir) src/elixir_compiler.erl:23: :elixir_compiler.quoted/2
(elixir) lib/code.ex:767: Code.require_file/2
(elixir) lib/kernel/cli.ex:503: Kernel.CLI.wrapper/1
(elixir) lib/enum.ex:1314: Enum."-map/2-lists^map/1-0-"/2
(elixir) lib/kernel/cli.ex:68: Kernel.CLI.process_commands/1
(elixir) lib/kernel/cli.ex:26: anonymous fn/2 in Kernel.CLI.main/1
(elixir) lib/kernel/cli.ex:105: anonymous fn/3 in Kernel.CLI.exec_fun/2
I was using https://github.com/OvermindDL1/gradualixir
typechecker:handle_type_error({type_error,map,182,
{type,227,term,[]}}) (src/typechecker.erl, line 2675)
And if you check typechecker.erl
you see that a type_error,map
is returned in 2 distinct places but is not handled in the error handler.
The discussion about testing in #54 needs its own place.
What's your suggestion regarding testing? As you said, some code will fail/pass type checking depending on this option's value. Two new subdirectories?
I don't know @Zalastax. I think unit tests using code in strings, as in the typechecker_tests suite, is better than the should_fail/pass ones.
I don't agree that strings are better - they lack syntax highlighting.
Type checkers are a prime case for golden testing and I was happy to see that it's already what's being used. Golden testing is easier to reason about since every test case is completely static (less logic in test = good). We should only resort to unit tests with custom logic when it's absolutely necessary.
regarding testing I think the should_pass/fail are nice as smoke tests but a bit limited (for example you cannot test if there are 1 or more errors in a should_fail module). the typechecker_tests-style tests need less context, can reach edge cases easier, or eg can also test specific errors (when gradualizer will support returning error terms)
regarding module attributes, I think in real use the option should be per project (eg in rebar.config) and not per module - but for testing a module attribute can be a nice idea.
My two personal goals are that:
I've had quite good success with the dtslint approach to testing types but I am not sure that's the path forward.
Sorry, I couldn't figure out quickly what is wrong so just reporting it.
(I suspect something around expect_tuple_type
returning {type, 0, any, []}
instead of any
)
Type checking the below program
-spec f(tuple() | integer()) -> ok.
f({1, 2}) ->
ok.
results in the below crash
escript: exception error: no function clause matching
lists:zip([{integer,2,1},{integer,2,2}],{type,0,any,[]}) (lists.erl, line 387)
in function typechecker:add_type_pat/4 (src/typechecker.erl, line 2117)
in call from typechecker:add_types_pats/4 (src/typechecker.erl, line 2093)
in call from typechecker:check_clause/4 (src/typechecker.erl, line 2032)
in call from lists:map/2 (lists.erl, line 1239)
in call from typechecker:check_clauses/4 (src/typechecker.erl, line 2018)
in call from typechecker:type_check_function/2 (src/typechecker.erl, line 2080)
in call from typechecker:'-type_check_forms/2-fun-0-'/5 (src/typechecker.erl, line 2358)
-spec fff() -> Result when Result :: integer().
fff() -> 0.
ggg() -> -fff().
** exception error: no function clause matching typechecker:int_type_to_range({var,6,'Result'}) (../src/typechecker.erl, line 604)
in function typechecker:negate_num_type/1 (../src/typechecker.erl, line 658)
in call from typechecker:type_check_expr/2 (../src/typechecker.erl, line 1219)
in call from typechecker:do_type_check_expr_in/3 (../src/typechecker.erl, line 1599)
in call from typechecker:type_check_expr_in/3 (../src/typechecker.erl, line 1595)
in call from typechecker:check_clause/4 (../src/typechecker.erl, line 2395)
in call from lists:map/2 (lists.erl, line 1239)
in call from typechecker:check_clauses/4 (../src/typechecker.erl, line 2376)
As a test to see how it ran, I ran Gradualizer on Gradualizer itself, there are a few issues, and they do seem to be legitimate:
╰─➤ find ebin/ -name '*.beam' -exec ./gradualizer -pa ebin {} \; 127 ↵
ebin/gradualizer_db.beam: The function get_src_map on line 145 is expected to return #{module() => string()} but it returns #{module() => file:filename()}
ebin/gradualizer_db.beam: The pattern #{K := Types} on line 156 doesn't have the type #{mfa() => [type()]}
ebin/gradualizer_db.beam: The pattern #{K := TypeInfo} on line 271 doesn't have the type #{mfa() => #typeinfo{}}
ebin/gradualizer_db.beam: The pattern #{autoimport := false} on line 289 doesn't have the type opts()
ebin/gradualizer_db.beam: The pattern #{Mod := Filename} on line 308 doesn't have the type #{module() => string()}
ebin/gradualizer_db.beam: The pattern #{Mod := Filename} on line 320 doesn't have the type #{module() => string()}
ebin/gradualizer_db.beam: The variable 'Forms1' on line 343 has type {file:posix() | badarg | system_limit, file:filename()} |
file:filename() |
abstract_forms() but is expected to have type gradualizer_file_utils:abstract_forms()
escript: exception error: no match of right hand side value
{{type,0,any,[]},
#{},
{constraints,#{},#{},
{set,0,16,16,8,80,48,
{[],[],[],[],[],[],[],[],[],[],[],[],[],
[],[],[]},
{{[],[],[],[],[],[],[],[],[],[],[],[],[],
[],[],[]}}}}}
in function typechecker:type_check_expr/2 (src/typechecker.erl, line 1005)
in call from typechecker:type_check_expr/2 (src/typechecker.erl, line 906)
in call from typechecker:type_check_block_in/3 (src/typechecker.erl, line 2023)
in call from typechecker:type_check_block_in/3 (src/typechecker.erl, line 2024)
in call from typechecker:check_clause/4 (src/typechecker.erl, line 2202)
in call from lists:map/2 (lists.erl, line 1239)
in call from typechecker:check_clauses/4 (src/typechecker.erl, line 2183)
in call from typechecker:check_clauses_fun/3 (src/typechecker.erl, line 2153)
ebin/gradualizer_file_utils.beam: The tuple on line 28 does not have type parsed_file()
ebin/gradualizer_file_utils.beam: The tuple on line 37 does not have type parsed_file()
ebin/rebar_prv_gradualizer.beam: Undefined remote_type rebar_state:t/0 on line 8
ebin/rebar_prv_gradualizer.beam: Undefined remote_type rebar_state:t/0 on line 22
ebin/rebar_prv_gradualizer.beam: Undefined remote_type rebar_app_info:t/0 on line 32
ebin/rebar_prv_gradualizer.beam: Undefined remote_type rebar_app_info:t/0 on line 38
ebin/rebar_prv_gradualizer.beam: Call to undefined function rebar_dir:src_dirs/2 on line 71
ebin/typechecker.beam: The variable 'Tys' on line 366 has type [abstract_type()] |
[abstract_type()] |
[abstract_type()] |
any |
af_singleton_integer_type() |
[(Name :: af_atom()) | af_record_field_type()] |
[abstract_type()] |
[af_assoc_type()] |
any |
[af_singleton_integer_type()] |
af_function_type() |
[{type, anno(), any} | abstract_type()] |
[] |
[] |
[af_singleton_integer_type()] but is expected to have type [type()]
ebin/typechecker.beam: The tuple on line 597 does not have type int_range()
ebin/typechecker.beam: The tuple on line 615 does not have type type()
ebin/typechecker.beam: The tuple on line 781 does not have type any |
{type_error, type()} |
{fun_ty, type(), type(), constraints:constraints()} |
{fun_ty_any_args, type(), constraints:constraints()} |
{fun_ty_intersection, [type()], constraints:constraints()} |
{fun_ty_union, [any()], constraints:constraints()}
ebin/typechecker.beam: The pattern {VEnv3,Cs2} on line 2246 doesn't have the type none() | none() | none() | any()
ebin/typelib.beam: The tuple on line 52 does not have type type()
ebin/typelib.beam: The operator '++' on line 97 is expected to have a non-list argument of type module() | file:filename()
ebin/typelib.beam: The tuple on line 129 does not have type type()
And it looks like there is a crash of Gradualizer itself within all that as well.
Hello, thanks for creating Gradualizer!
I tried it out on a simple module and ran into this error:
# foo.ex
defmodule Foo do
@spec is_comment?(String.t()) :: boolean
def is_comment?("#" <> _rest), do: true
def is_comment?(_), do: false
end
iex(4)> :gradualizer.type_check_module(Foo)
The pattern <<"#",_rest@1/binary>> on line 3 doesn't have the type 'Elixir.String':t()
:nok
Looks like it hasn't resolved the type Elixir.String.t
as a synonym for binary
?
The function record_info/2
is a built-in pseudo-function. Currently, Gradualizer doesn't know about it and reports a type error. We need to add this function to the type environment.
The question is what type we should give this function. There is a whole spectrum of increasingly precise type we could give it. I'm considering whether we should try to make it as precise as possible by actually checking the arguments and return the actual fields or size, depending on how it's called.
For example, given the following record declaration:
-record(person, {name, phone, address}).
The call record_info(size, person)
would have the singleton type 3
.
I want to work on making Gradualizer a real Erlang application so I'm wondering what you have in mind.
Is it a traditional long-running OTP application you have in mind or a CLI application that starts and stops between each request?
Perhaps an implementation using the Language Server Protocol?
If module passed to &:gradualizer.type_check_module/1
function contains function calls to other modules, Gradualizer throws error Call to undefined function ...
. What is the proper way to avoid it?
I've added a milestone called Beta release which right now collects some of the issues that I'd like to see resolved before we can announce a beta. My main goal is to have Gradualizer handle all language constructs in Erlang and not crash when invoked on syntactically valid programs.
I think we should aim at being lenient for the beta release and not report a type error if there is any doubt about what choice to make. We can refine the typing later.
I'm interested in hearing what people think of this plan and if there are other things you'd like to see in a beta.
Something is wrong with Erlang version?
Trying it with OTP20 / macos
Iljas-iMac:Gradualizer timcf$ make
erlc absform.erl
erlc constraints.erl
erlc gradualizer_db.erl
erlc typechecker.erl
typechecker.erl:5: Warning: export_all flag enabled - all functions will be exported
erlc typelib.erl
erl *.beam
2018-06-04 17:27:51 application_controller: ~ts: ~ts~n
["syntax error before: ","'.'"]
"absform.beam"
{"could not start kernel pid",application_controller,"{bad_environment_value,\"absform.beam\"}"}
could not start kernel pid (application_controller) ({bad_environment_value,"absform.beam"})
Crash dump is being written to: erl_crash.dump...done
make: *** [run] Error 1
Lager is probably the most popular logging framework used in the Erlang ecosystem. However, it's API is somewhat peculiar, because calling it is done with pseudo-calls, i.e. hooks which look like regular function calls, but are actually rewritten by lager_transform
parse transformation. This results in, for example, Call to undefined function lager:debug/2 on line 204
messages.
One obvious way of solving this would be for a library using such a parse transformation to export properly typed function stubs. What's the Gradualizer team's stance on that? Do you suggest sending PRs adding suitable stubs e.g. to lager?
(this ticket was split from #23 which also contain some of the early comments)
let's see the following correct function with spec
-spec f(atom() | integer()) -> true | integer().
f(AI) ->
if is_atom(AI) -> %% Expr1
true;
true ->
AI + 1 %% Expr2
end.
AI
in Exrp2
must be the subtype of number() :: integer() | float()
as the first argument of +
AI
in Exrp2
is atom() | integer()
based on the spec which is not a subtype of integer() | float()
How could Gradualizer realise that Expr2
is only executed when type of AI
is integer()
?
if NOT is_atom(AI) => typeof(AI) == (atom() | integer()) & (not atom()) == integer()
- however this is not always possibleLet's see a more generic example
-spec f(input()) -> any().
f(A) ->
case cond(A) of
true -> true;
false -> body(A)
end.
-spec cond(input()) -> boolean().
-spec body(required()) -> any().
In this case what the type checking could do is realise that body(A)
is only executed in a subset of cases therefor type of A
in body(A)
is just a subset or subtype of input()
. In case input() & required() == none()
(the intersection of the two types is empty) then we can say that body(A)
will always fail, but otherwise we cannot know (and have to leave type checking at runtime). This method requires to be able to calculate the intersection of two types.
What is the right way to handle these kind of constructs? (if
, case
, multiple function clause)
let's see the following correct function with spec
-spec f(atom() | integer()) -> true | integer().
f(AI) ->
is_atom(AI) %% Expr1
orelse
AI + 1. %% Expr2
AI
in Exrp2
must be the subtype of number() :: integer() | float()
as the first argument of +
AI
in Exrp2
is atom() | integer()
based on the spec which is not a subtype of integer() | float()
How could Gradualizer realise that Expr2
is only executed when type of AI
is integer()
?
if NOT is_atom(AI) => typeof(AI) == (atom() | integer()) & (not atom()) == integer()
- however this is not always possibleLet's see a more generic example
-spec f(input()) -> any().
f(A) ->
cond(A)
orelse
body(A).
-spec cond(input()) -> boolean().
-spec body(required()) -> any().
In this case what the type checking could do is realise that body(A)
is only executed in a subset of cases therefor type of A
in body(A)
is just a subset or subtype of input()
. In case input() & required() == none()
(the intersection of the two types is empty) then we can say that body(A)
will always fail, but otherwise we cannot know (and have to leave type checking at runtime). This method requires to be able to calculate the intersection of two types.
What is the right way to handle these kind of constructs? (if
, case
, andalso
, orelse
, multiple function clause)
When gradualizer is run as an escript (as on travis) it crashes with the below error:
{"init terminating in do_boot",{{badmatch,{error,enotdir}},
[{gradualizer_db,import_erl_files,2,[{file,"/home/travis/build/josefs/Gradualizer/_build/default/lib/gradualizer/src/gradualizer_db.erl"},{line,333}]},
{gradualizer_db,init,1,[{file,"/home/travis/build/josefs/Gradualizer/_build/default/lib/gradualizer/src/gradualizer_db.erl"},{line,151}]}...
This can probably have something to do with code:priv_dir(gradualizer) => "/home/travis/build/josefs/Gradualizer/gradualizer/gradualizer/priv"
because it is running from an escript archive.
Currently gradualizer:type_check_file
accepts files ending in .beam
or .erl
, however it would be nice to be able to give a BEAM forms term directly (type_check_forms
?), perhaps other things like accepting an erlang string would be useful as well, however being able to pass in in-memory forms or a binary of a beam file (that may not exist on disk) would be very useful for tools built on this.
Is the public API just the gradualizer
module?
Is it fine that we use short module names like ty
?
We have a decent test suite. It's be nice to leverage this by adding CI support. I have good experience with travis-ci but I'm interested in
We also have the possibility to run dialyzer if we implement CI support. Do people think that would be a good idea? I personally think it's be good to keep Gradualizer free from dialyzer warnings, but I'm too lazy to run it frequently. However, @gomoripeti runs it every now and again and finds useful improvements.
Currently the rules for pushing types into arithmetic operator applications in type_check_arith_op_in
says (the other operator rules are similar):
subtype(R, number)
check(A, R)
check(B, R)
------------------
check(A op B, R)
This subtype constraint goes the wrong way, as shown in this example:
-spec f(integer(), integer()) -> integer() | divide_by_zero.
f(_X, 0) -> divide_by_zero;
f(X, Y) -> X div Y.
%% The operator 'div' on line 8 is given a non-integer argument of type integer() | divide_by_zero
The error message is a bit strange as well, since it's the subtype(R, number)
constraint that fails and not anything to do with the arguments.
The reason for having the subtyping this way around (I suspect) is to make this fail:
-spec g(number(), number()) -> integer().
g(X, Y) -> X + Y.
%% The variable 'X' on line 12 has type integer() | float() but is expected to have type integer()
I believe the correct rule is
S = infer(A)
T = infer(B)
U = compat_arith_type(S, T)
subtype(U, R)
--------------------
check(A op B, R)
It would be good to have an option to return errors as erlang terms (when called from Erlang, not cli).
This requires unifying and documenting the error terms, each one having the same structure (common fields in same position: eg filename, line number, expected type etc.)
Also the default formatter (used by the cli) could have a format similar to other tools, like the compiler: file-name:line-number:error-text
Currently I'm investigating ability of using of this tool to analyze Elixir-compiled BEAM bytecode.
BEAM files compiled with Elixir compiler can be decompiled back to Erlang AST/source code.
Example: this file
Can be decompiled back to
-file("/Users/timcf/HTprojects/hm-crypto/lib/hm_cryp"
"to/public_key.ex",
1).
-module('Elixir.HmCrypto.PublicKey').
-compile(no_auto_import).
-spec parse_pem(rsa_key()) -> tuple().
-export_type([rsa_key/0]).
-type rsa_key() :: binary() | tuple().
-export(['__info__'/1, parse_pem/1]).
-spec '__info__'(attributes | compile | functions |
macros | md5 | module | deprecated) -> any().
'__info__'(module) -> 'Elixir.HmCrypto.PublicKey';
'__info__'(functions) -> [{parse_pem, 1}];
'__info__'(macros) -> [];
'__info__'(attributes) ->
erlang:get_module_info('Elixir.HmCrypto.PublicKey',
attributes);
'__info__'(compile) ->
erlang:get_module_info('Elixir.HmCrypto.PublicKey',
compile);
'__info__'(md5) ->
erlang:get_module_info('Elixir.HmCrypto.PublicKey',
md5);
'__info__'(deprecated) -> [].
parse_pem(Vpem_string@1)
when erlang:is_binary(Vpem_string@1) andalso
Vpem_string@1 /= <<>> ->
[Vpem_entry@1] = public_key:pem_decode(Vpem_string@1),
public_key:pem_entry_decode(Vpem_entry@1);
parse_pem(Vpem@1) when erlang:is_tuple(Vpem@1) ->
Vpem@1.
When I'm trying to apply Gradualizer to this file, first thing I get is error
The atom 'Elixir.HmCrypto.PublicKey' on line 24 does not have type Module
I'm not expert in pure Erlang standards, but isn't this atom a valid module name? If I run erl
shell with loaded BEAM files of application - it works without any issues as module name:
Eshell V9.3.1 (abort with ^G)
1> 'Elixir.HmCrypto.PublicKey':parse_pem({hello, world}).
{hello,world}
2>
Any ideas about it?
The following code
-type t() :: #{year := integer() | nil,
price := integer() | nil,
model := 'Elixir.String':t() | nil}.
-spec 'can_buy?'('Elixir.Car':t(),
integer()) -> boolean().
'can_buy?'(#{price := Vprice@1}, Vmoney@1)
when Vprice@1 =< Vmoney@1 ->
true;
'can_buy?'(#{}, _) -> false.
currently not passing Gradualizer checks:
The pattern #{price := Vprice@1} on line 10 doesn't have the type 'Elixir.Car':t()
Is it bug or feature? I'm asking because big amount of Elixir code uses map-based types.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.