Suggestion: Add more to the FAQ

[tsloughter]

Aside from dialyzer it would be useful to have comparisons to other Erlang type checking tools, particularly Gradualizer. I'm sure there are others that'd be good to provide, gradualizer is just the one I was personally curious in a comparison with :).

[ilya-klyuchnikov]

Thanks. Yes, it would be added as part of documentation soon.

[tsloughter]

Hey, any update on this? Or can you say here what the difference is with Gradualizer :)

[VLanvin]

After reading the docs and running some quick experiments, here are my preliminary conclusions about this.

I think the main difference is that eqWAlizer has two modes, strict and dynamic. Dynamic mode corresponds, in essence, to Gradualizer. Strict mode allows for stricter type-checking, by not only considering dynamic() to be equal to term(), but also by treating types differently internally, and by making sure that dynamic() can never appear during elaboration, type refinements, or type inference. While eqWAlizer is mostly developed with gradual mode in mind at the moment, we still try to keep strict mode in sync as it can sometimes provide better signal.

You can find more info about modes here.

EqWAlizer and Gradualizer also make different assumption about types. For example, eqWAlizer does not differentiate between numeric types (it consider them all equal to number()), while Gradualizer does. Gradualizer also makes different assumption about map types. For example, Gradualizer understands type #{integer() := integer()} as the type of maps that have at least one binding from an integer to an integer. In eqWAlizer, we considered such a type to be ambiguous and opted to simply interpret it as #{term() => term()} in strict mode, and #{dynamic() => dynamic()} in gradual mode.

On the topic of maps, eqWAlizer differentiates between dictionaries and shapes: shapes are special map types where the keys are all atoms that are known statically. This allows eqWAlizer to perform more precise type checking on maps in some instances.

More info about types and subtyping for maps.

Finally, eqWAlizer features stronger occurrence typing (type refinement) than Gradualizer. In particular, eqWAlizer is able to refine the type of expressions using information in arbitrary deep patterns and guards. See these snapshot tests as an example. Gradualizer only allows refinements based on failing clauses in very specific cases, as explained here.

Hope this clarifies things a bit, I'll add this info in the documentation after more experimenting.