WhatsApp / eqwalizer

A type-checker for Erlang
Apache License 2.0
506 stars 27 forks source link

Can eqWAlizer distinguish between different numeric types? #11

Closed kikofernandez closed 1 year ago

kikofernandez commented 1 year ago

Hi! I know that currently (v 0.12.12) eqWAlizer cannot distinguish between different numeric types (doc here). I was wondering if there is a technical issue with it per se or if this is something that could be worked out in the future, to catch more typing errors.

Thanks!

ilya-klyuchnikov commented 1 year ago

Sorry for the very late reply.

We decided not to support different numeric types for a combination of reasons:

  1. Simplicity of the internals of the type-checker. We did experiments with supporting the Numeric tower (https://www.ccs.neu.edu/home/stamourv/papers/numeric-tower.pdf) and while it's possible - it complicates the internals a lot.
  2. Our experiments showed that type-checking with Numeric tower would be noisy.
  3. It has never been escalated by our primary users and something that is critical or important.
  4. In general, - having different numeric types (and even ranges) seems to us as an unnecessary over-complication.
  5. Except Typed Racket (with strong typing discipline) - no other popular language has Numeric Tower in a sense of having types like positive integers, negative integers, ...
ilya-klyuchnikov commented 1 year ago

@kikofernandez

A few additional points:

So, it becomes hairy to type-check the following code:

-spec convert(pos_integer()) -> pos_integer().
convert(Min) -> round(Min / 60).