Elixir v1.20 released: now a gradually typed language
101 points by munksgaard
101 points by munksgaard
This post is an occasion to advertise for long-term public-funded research. Some of the people doing the hard thinking behind this work are my colleagues (we work in the same building) in a computer science research lab in Paris (in particular Guillaume Duboc, Guiseppe Castagna). The theoretical foundations for this nice type system for a dynamic language, "set-theoretic typing", are in the works since the early 2000s; they were originally targeted at providing rich types to XML documents and program manipulating them, and it is sort of a coincidence that they are also rather good at providing principled yet effective type systems for dynamic languages.
We benefit from this work, collectively, thanks to the bright people working in public service, the academic values of sharing our work as widely as possible (decades of research, all of this accessible for free completely in the open, with open source software implementations, etc.), and the wisdom of some countries to direct some taxpayer money to long-term research.
Congratulations Elixir team!
Damn, Elixir is such a nice language.
Very exciting evolution, looking forward to trying it out.
def example(x) when not is_map_key(x, :foo) And the code above infers x is a map that does not have the :foo key, which has the type: %{..., foo: not_set()}.
Why does it infer a map ? To me, an integer for example would also satisfy not is_map_key(x, :foo) ?
Because is_map_key(map, key) checks if key is in map. It doesn't make sense to check if a key is in an integer.
Let's say: "is_map_key(x, key)" is "is_map(x) and is_not_nil(x.key)"
If "x" is an integer, it fails the "is_map(x)", thus validates "not is_map_key(x, key)".
But, as you suggest, "not is_map_key(x, key)" would be "is_map(x) and is_nil(x.key)"
The question would be, how does the type system decides that?
It’s explained in the Elixir type system paper. The function guard is not itself a type: the type is inferred from the guard. So for the guard to be correctly typed, x must be a map; then the guard refines that type to be a map not containing :foo.