Set Theoretic typing and existing Elixir type heirarchy

It’s a gotcha for sure. I always add an is_integer(x) to guards that do less/greater than checks.

def x(y) when is_integer(y) and y >= 5, do: nil

I’d not expect a typewarning here, but rather a “is always true/false” kind of warning, if indeed y is always a tuple.

Here is I believe a test case:

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.

That’s because tuple >= 5 is not only valid, but returns true.

iex(1)> tuple = {1, 2}
{1, 2}
iex(2)> tuple >= 5
true

Elixir allows comparisons between elements of different types.

See Kernel — Elixir v1.21.0-dev

TLDR; any tuple is considered to be greater than any integer.

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.