Comparison to Dialyzer

Gradualizer and Dialyzer have similar goal: to use static analysis to prevent bugs early. But they go about it differently and have different pros and cons. We like to think of them as complementary tools and we outline their respective strengths and weaknesses below:

Principles

Dialyzer is not a typesystem. It's a discrepancy analyzer which aims to prove the presence of runtime crashes. It avoids false positives.

Gradualizer is a more conventional type system. It aims to prove the absence of type based crashes (although the story is a little more nuanced because of gradual types).

Type specs

Dialyzer introduced the type specs which are part of the erlang syntax. However, there is no need to write any specs in order to benefit from Dialyzer, it will infer information about functions without them. Dialyzer doesn't check the correctness of the specs by default. There are the flags -Wunderspec and -Woverspec to check the specs against analysis results, however, these checks are unfortunately unsound. When type specs are provided they are combined with the analysis result (technically, the spec and the analysis result is intersected). This means that the analysis can be made more precise using specs but it is also possible to create very strange errors if specs are faulty.

Gradualyzer depends intimately on type specs. It uses the type specs introduced by Dialyzer. Without any specs, Gradualizer doesn't do any static checking, you get the same experience as just using standard erlang. When type specs are added the code is checked against these specs. (Though you will get static checking when calling functions in OTP because they have specs). Gradualizer doesn't do any type inference by default, though it has the flag --infer which does local type inference of expressions.

Examples

Here are some concrete examples of differences between Dialyzer and Gradualizer.

Checking type specs

A type spec which says that the function returns the empty tuple, but it can also return true.

-spec pattern_test(integer()) -> {}.
pattern_test(1) ->
	true;
pattern_test(X) ->
	{}.

• Dialyzer will not detect the error in the above program
  • Using the flag -Woverspecs will detect it though.
• Gradualizer detects the error

Handling Unions

-spec tuple_union() -> {undefined, binary()}
			| {integer(), undefined}.
tuple_union() ->
	{undefined, undefined}.

• Dialyzer approximates a union of tuples as a tuple of unions.
  • In this case it means that it approximates the return type as {undefined | integer(), binary() | undefined}
  • The result is that Dialyzer fails to catch the error
• Gradualizer detects the error

Flow Sensitivity

-export([foo/0]).
foo() -> bar(apa).

-spec bar(apa | bepa) -> true | false.
bar(apa)  -> true;
bar(bepa) -> false.

• Dialyzer can figure out that the clause bar(bepa) will never be called.
  • With -Wunderspecs, Dialyzer will also complain that bar/1 will never return false.
• Gradualizer cannot do any of that.

Restrictions on the Nesting Depth of Types

Dialyzer will only go so far when trying to detect errors in nested types.

-spec depth4() -> {1,{2,{3,4}}}.
depth4() -> {1,{2,{3,5}}}.
-spec depth5() -> {1,{2,{3,{4,5}}}}.
depth5() -> {1,{2,{3,{4,6}}}}.

• Dialyzer will detect the error in depth4/0 but not depth5/0
• Gradualyzer will detect both
• In fairness, this is rarely a problem in practice