I am using 1.20.0-rc4 and discovered a bug I introduced today. Wanted to share mostly because I want to understand the extent of how set theoretic typing will or will not address this kind of bug. The code snippet:
result = Cachex.incr(:cache, :key, 1, default: 0)
if result > 5 do
…
end
What I forgot in my haste was that the return from that Cachex function is a tuple, {:ok, integer()} not integer(). And I got no warning. Had I done something similar in a guard expression comparing a tuple to an integer IMHO would not have indicated any warning under set theoretic typing.
So a function signature like:
def x(y) when y >= 5, do: nil
where y is a type of tuple should NOT generate a type warning. It should not only because of the Elixir type heirarchy.
It seems this is a very possible common bug when dealing with libraries where Bang methods tend to return some Elixir type and non-bang functions tend to return a tuple with the second element being some Elixir type and the first element being an atom such as :ok, or :error.
I am interest in others thinking, and mostly to help me understand what can or cannot be done to help locate these errors. If all of our libraries we use day in and day out had set theoretic typing contribution to our app compilations, this seems to be something of value.
Anyway - please comment and help me reason about this.
defmodule TestTuple do
@moduledoc """
A simple module to demonstrate tuple usage in Elixir.
"""
@doc """
Takes a tuple with two elements
"""
@spec format_tuple({any(), any()}) :: String.t()
def format_tuple({_first, _second} = tuple) do
x(tuple)
end
defp x(tuple) when tuple >= 5 do
"This is the tuple: #{inspect(tuple)}"
end
defp x(tuple) do
"Tuple is less than 5: #{inspect(tuple)}"
end
end
and results are
iex [03:36 :: 1] > TestTuple.format_tuple({1,2})
“This is the tuple: {1, 2}”
No compile error or warnings.
So I would say this scenario is undetected by current set theoretic typing compilation.
I believe you need to do something to indicate the type for the compiler to catch it. e.g. Atom.to_string(x) tells the compiler that x is an atom.
You’re telling it there is a tuple. >= is not an integer only operator so it’s not going to complain about that. Maybe if you put an is_integer guard with it it might tell you that clause is unused. Dunno if that is or will be implemented.
Type specs and set-theoretic types don’t raise a warning here because any types can be compared (this comes from Erlang—I’m not sure about the reasoning behind that ). Sometimes type checks are missed before comparing data, which leads to logic errors.
Once you remove the function indirection there is a warning though - because the tuple will always result in the same comparison result. The issue seems to be with the type knowledge propagating through the callstack.
In this case, you compared a tuple like {:ok, 1} > 5, which will always return true.
Also, every atom is considered greater than every number, so if you were using a function that returned {:ok, integer() | :error} , either way, result > 5 is always going to return true.
This is one place where I hope eventually we’ll be able to use types, to show a warning that this expression is always going to return true .
Exactly my point @matt-savvy . Because there is an Elixir type heirarcy in play, it seems as though we lose some ability to detect what I consider to be a bug, because precisely it is a valid comparison.
I don’t feel like I was making myself clear here. I would hope eventually in this situation that given the subsequent function, that it would announce that subsequent function would never be reached. Even as confusing at first as that may seem.
Ideally (in my selfishness) I would like it to tell me more precisely that I was comparing disparate types, but the language type hierarchy already permits that comparison. If somehow that type hierarchy could be indicated to not be in play (comparing for example atoms to tuples to lists with greater than or less than) it would increase the value of type checking.
I do realize if I indicated the expected type of the parameters with a guard then I would be encouraging the type checking accuracy. However one of the purposes afaict of the lovely approach to gradual theoretic typing is NOT relying on code changes or type hinting. So far it seems this propagation of type knowledge has been IMHO highly (remarkably?) successful.
I think the idea is that there’s a lot of mistakes that can be caught/prevented by the type checker without any code changes or type annotations, but at a certain point, it’s going to be on us to clarify our intentions. There’s plenty of places where it makes total sense to compare numbers to atoms or atoms to tuples.
Also, I think this is a place where the type checking is still limited to your project and not its dependencies.
A basic example gets you a warning like you would expect:
def run(x) do
res = result(x)
if res > 5 do
IO.puts("hello")
end
x
end
defp result(x) when x < 10, do: {:ok, x + 1}
defp result(_), do: :error
Compiling 1 file (.ex)
warning: comparison between distinct types found:
res > 5
given types:
dynamic(:error or {:ok, float() or integer()}) > integer()
where "res" was given the type:
# type: dynamic(:error or {:ok, float() or integer()})
# from: lib/some_app.ex:3:9
res = result(x)
While Elixir can compare across all types, you are comparing across types which are always disjoint, and the result is either always true or always false
type warning found at:
│
5 │ if res > 5 do
│ ~
│
└─ lib/some_app.ex:5:12: SomeApp.run/1
With your dependency :
def run(x) do
Cachex.start_link(:my_cache)
{:ok, true} = Cachex.put(:my_cache, "my_key", 5)
res = Cachex.incr(:my_cache, "my_key")
if res > 5 do
IO.puts("larger than three")
end
x
end
@matt-savvy thanks for your time and comments - much appreciated.
Based on what I have seen so far it seems as though this may be a hole in the current type checking - especially given the “disjoint” comment in one of the warnings in your example. I say that with the highest regard for the awesome work on the type checking to date. Kudos to everyone on this effort.
). Sometimes type checks are missed before comparing data, which leads to logic errors.
