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.
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/3 will fail on non-map argument (it is different from returning false). So this guard will work only for maps, all other values will fail guard.
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.
gasche | 14 hours ago
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.
lpil | 23 hours ago
Congratulations Elixir team!
ThePaulMcBride | a day ago
Damn, Elixir is such a nice language.
moltonel | a day ago
Very exciting evolution, looking forward to trying it out.
Why does it infer a map ? To me, an integer for example would also satisfy
not is_map_key(x, :foo)?hauleth | 15 hours ago
Because
is_map_key/3will fail on non-map argument (it is different from returningfalse). So this guard will work only for maps, all other values will fail guard.moltonel | 10 hours ago
Ah ok, now I remember failure in guards short-circuit, so the
notisn't evaluated, thanks.thomas0 | a day ago
Because
is_map_key(map, key)checks ifkeyis inmap. It doesn't make sense to check if akeyis in an integer.linkdd | 20 hours ago
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?
fanf | 20 hours ago
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.