I do not know much about typing system. Regarding the union vs intersection of function types, there was something I did not grasp. For me it seems more correct the combined type is a union.
integer() -> integer()
def negate(n) when is_integer(n), do: -n
boolean() -> boolean()
def negate(b) when is_boolean(b), do: not b
The negate “symbol function” I thought would look like this:
negate: (integer() -> ineteger()) or (bool() -> bool())
So when the typing verification process start walking the code, if it arrives to an expression like negate(12) then it can go to the typing structure attached to the negate function symbol, lookup the matched typing from the options, since its or then find the first one matched, and use that to continue the verification and typing inference.
a = negate(12)
b = a + "word"
# type error
How would the type walkthrough check would work? What intersection would mean?
I don’t know how the elixir typesystem decides what “constitutes a type”
But if you take it to mean a “type is a subset of values that might not constitute a crash when passed as a value to any given function” it makes sense. If you search for “covariance” vs “contravariance” you will get a technical explanation (see paragraph 4 of: Covariance and contravariance (computer science) - Wikipedia)
But think of it this way:
integer() → integer() is all functions guaranteed to not crash when you pass an integer and returns an integer.
boolean() → boolean() is all functions guaranteed to not crash when you pass an boolean and returns a boolean.
if you did a union of those, then a function that doesn’t crash when you pass a boolean, but DOES crash when you pass an integer, is part of the union.
You really do want to type specify intersection because we have a stronger guarantee (the set of functions it’s a member of is smaller than either of the two descriptions). This is a function that doesn’t crash when you pass integer AND doesn’t crash when you pass a boolean. The AND relationship is captured by the intersection operator.
is functions that, when given an integer, are guaranteed – if they don’t crash – to return an integer (and not something else).
The intuition still holds though: a function that returns integers when given integers, and integers when given booleans has type integer() -> integer(). So it would be part of the union.
About crashes: typechecking does prevent them – if you annotate all your functions and avoid using dynamic(). If you do though, then crashes may happen but the guarantee remains that result of the function will be of the right type.
Also @elpd , when typing the application negate(12), we look at the type of its argument, and then at the each of the arrows in the intersection. Then, for each arrow, if the type of the argument can appear in the input type of the arrow, we add its return type to a union that is going to be the type of the application. In this case, only integer(). T
But if you give something that may be an integer or a boolean to negate, both arrows will be selected and the application will have type integer() or boolean(). This is how the walkthrough is done.
