Some thoughts on the proposed ??? (which I think I quite like).
What if the meaning of this operator was: if the type checker can reach it, it’s an error/warning and shows the condition in which it could be reached. If the type checker can’t reach it, you’re good. If the execution ever does reach it at runtime (edit: without having issued a warning), it’s because there’s a bug in the type checker.
Consider:
def some_fun(:foo), do: :ok
def some_fun(:bar), do: :ok
def some_fun(:baz), do: ???
I might write this to indicate that :baz is a todo. If the type checker can’t find a situation where :baz is passed, you’re good. But when it sees these, you start getting a warning:
# obvious
some_fun(:baz)
# maybe less obvious, but this expr has type atom() which contains :baz
some_fun(String.to_atom("anything"))
Using these semantics, you could now use ??? wherever you want to be exhaustive:
case fun() do
:foo -> :ok
:bar -> :ok
_ -> ???
end
def some_fun(:foo), do: :ok
def some_fun(:bar), do: :ok
def some_fun(_), do: ???
This implies that, when you don’t use ???, type checking can be “assertive” and assume that the return type of your case/function/etc. is narrowed to whatever you’re returning because it’ll error at runtime and be handled using existing mechanisms (OTP).
Another note: I do not think it should not be possible that a callee require that a caller handle an exception to successfully type check. E.g. a function that indicates some error type and requires that I call it in a try or something.
