elpd
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?
Most Liked
ityonemo
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: Type variance - 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.
gldubc
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.
Popular in Discussions
Other popular topics
Chat & Discussions>Discussions
Latest on Elixir Forum
Sponsor Spotlight
Supporting innovation across the BEAM ecosystem.
Categories:
Sub Categories:
Forums
Popular Tags
- #ecto
- #liveview
- #troubleshooting
- #learning-elixir
- #deployment
- #library
- #erlang
- #testing
- #genserver
- #mix
- #absinthe
- #remote-other
- #otp
- #plug
- #how-to-question
- #macros
- #postgres
- #channels
- #elixirconf
- #exunit
- #discussion
- #code-sync
- #javascript
- #podcasts
- #onsite
- #dialyzer
- #docker
- #authentication
- #umbrella
- #full-time-contract
- #podcasts-by-brainlid
- #ecto-query
- #elixir-ls
- #phoenix_html
- #iex
- #blog-post
- #graphql
- #genstage
- #ai
- #websockets
- #supervisor
- #elixirconf-us
- #advent-of-code
- #distillery
- #processes
- #api
- #forms
- #metaprogramming
- #security
- #hex
Our Sponsors
Build Elixir applications with speed and confidence.
Supporting innovation across the BEAM ecosystem.
We build reliable cloud platforms for business-critical systems.
Catch errors, track performance, monitor hosts and more.
Error tracking, logs, uptime, and Just Enough APM. Built for developers.
Practical resources that improve the lives of professional developers.
Develop your skills with books, videos, and courses.
Enabling companies to succeed by building software people love.
The team behind Membrane, Popcorn, LiveDebugger. Available for hire.
Courses that'll move you from confusion to "Aha, now I get it!"