elpd
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?
Where Next?
Trending in Discussions
Other Trending Topics
Latest on Elixir Forum
Sponsor Spotlight
Enabling companies to succeed by building software people love.
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
- #elixirconf
- #channels
- #exunit
- #discussion
- #code-sync
- #javascript
- #podcasts
- #onsite
- #dialyzer
- #docker
- #authentication
- #umbrella
- #full-time-contract
- #podcasts-by-brainlid
- #ecto-query
- #elixir-ls
- #blog-post
- #ai
- #elixirconf-us
- #phoenix_html
- #iex
- #graphql
- #genstage
- #websockets
- #supervisor
- #advent-of-code
- #distillery
- #processes
- #api
- #forms
- #hex
- #security
- #metaprogramming
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.
Producing high quality Elixir screencasts since 2017.
The deployment platform built for Elixir: PaaS ease, VPS control.
The team behind Membrane, Popcorn, LiveDebugger. Available for hire.
Courses that'll move you from confusion to "Aha, now I get it!"
Showing Posts 1 to 2- Show Best Posts
- Show All (oldest first)
- Show All (newest first)
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, onlyinteger(). TBut if you give something that may be an integer or a boolean to
negate, both arrows will be selected and the application will have typeinteger() or boolean(). This is how the walkthrough is done.