Code Sync
3 HN mentions · mentioned in 3 months, 2023–2026
40:15 · 7K views · Oct 23, 2023
ElixirConf EU 2023 talk by Giuseppe Castagna and Guillaume Duboc on bringing set-theoretic types to Elixir, and the benefits such a type system could offer such as catching bugs.
Linked as the authoritative background on how Elixir's gradual set-theoretic type system works.
3 comments from Hacker News
> The hottest news in the Elixir community is that it is currently experimenting with set theoretic type / gradual typing. Some french PHD is working on it To expand on it: you can read the proposal[0] or watch the video presentation by the author[1]. It is a very similar system to Typescript, with (at the first glance) only minor differences: "any" becomes "term", primitive constants are not singleton types (so you cannot write programs with type system alone... yet), and I expect some edge cases around generics will be handled differently (especially since you cannot specify types yourself in function calls, i.e there is no myFunction<MyType1, MyType2>()). On the other side, there are some things that the proposal seems to be doing better than Typescript. It handles type assertions without the need for "function isX(maybeX): asserts maybeX is X { ... }" and since pattern matching plays important role in Elixir, I expect it will have a lot of polish around that. [0] [LINK] [1] this video
Short answer: “a type system centered on the use of set-theoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations”. Long answer, well, there are blog posts[0], the Design Principles of the Elixir Type System paper[1] and related presentations[2, 3, 4] that talk about it at length. Giuseppe Castagna’s site has many more related papers: [LINK] [0]: [LINK] [1]: [LINK] [2]: this video [3]: [LINK] [4]: [LINK]
We were 100% not expecting this to show up on HN front page. :) In any case, the title is accurate in that it is only a prototype and it was built by Guillaume to explore how Elixir idioms map to set-theoretic types. The UX and syntax do not reflect how the type system would look in Elixir itself (if we get a type system at all). You can find more context in Guillaume’s talk: this video The initial research announcement: [LINK] And the paper as a deeper, more accurate, and complete resource: [LINK]