Typing violation warning when comparing atoms

Questions / Help
, ,
1

Why comparing atoms gives typing violation warning?

consider:

defmodule MyModule do
  def test do
    :a < :b
  end
end

mix compile my_module.ex

gives a warning:

Compiling 1 file (.ex)
    warning: comparison between incompatible types found:

        :a < :b

    While Elixir can compare across all types, you are comparing across types which are always distinct, and the result is either always true or always false

    typing violation found at:
    │
  3 │     :a < :b
    │        ~
    │
    └─ my_module.ex:3:8: MyModule.test/0
1 Like
2

What’s the result you expected? What are you trying to do?

1 Like
3

Because :a and :b are not considered to be of type atom() but respectively as type :a and :b.

4 Likes
4

And as mentioned in the warning the result of the comparison is static as well.

2 Likes
5

Since the < operator is inlined with :erlang.</2, I expected the compiler to resolve its typing to a parametric polymorphic definition, something akin to (a, a) -> boolean() when a: term(). I didn’t expect singleton types.

I gave a simplified example to illustrate the problem, which I encountered when implementing client-server consistency tests in Hologram. Basically, I test whether manually transpiled Erlang functions behave exactly the same as their server counterparts.

6

If the typesystem has distinct types, why would it fall back to less specific types? This would be different if you would have variables here, but you hardcoded values for the comparison.

7

@antoine-duchenet @LostKobrakai Guys, considering your previous answers, does this mean that Erlang functions are not treated as “atomic” functions for the type system and they don’t have hardcoded typings? Or maybe the underlying Erlang functions’ abstract code (or bytecode) is analysed as well in the process to determine the typings?

8

Not sure I get what you’re asking for, but I don’t think there’s much to it.

With 1.17 warnings where implemented to warn when comparisons are made between different types of data – mostly to warn for the common footgun of comparing structs like DateTime, which would use structural comparison not semantic one. That’s the source of the warning.

The reason for getting the warning if both sides are atoms comes from the fact that the new typesystem implementation considers atom() a divisable type, which includes all possible individual atoms. So :a and :b are distinct types based on the typesystem, but both are part of atom(). The wording sounds a bit unfortunate here though given it’s a bit ambiguous what type of “type” the error refers to.

2 Likes
9

He’s probably asking about BIFs and such.

1 Like
10

BIFs are a runtime/implementation concern though. The compiler (and the typesystem) generally don’t care about any of that.

11

So your functions that call them would never be type-checked by Dialyzer whether they pass the right types of arguments to BIFs, is that what you’re saying?

12

No. I’m saying that a function being implemented as a BIF or not doesn’t matter. Anything happing at compile time happens way before there’s any difference between those.

13

This should be marked as the solution.

1 Like
14

I’m not sure if I understand your question correctly, but functions applications (Foo.bar(baz) or :foo.bar(baz)) are not typed yet, this will come with future releases.

Standard library functions from Elixir and Erlang will be typed then.