# Union vs Intersection for function types in Elixir gradual type system

I have just seen ElixirConf 2023 - José Valim - The foundations of the Elixir type system , which is very interesting.

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.

3 Likes

Hi! To be precise, for us,

`integer() -> integer()`

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.

1 Like