> At best a subset of functionality than an analogue. This kind of research is being conducted by experts in type theory outside of Elixir. If it's a problem for Elixir, it's a problem for any other language that would attempt it, and absolutely I would defer to the authority of those experts who have spent years looking at type theory.
Ironically the researcher that you're deferring to (Giuseppe Castagna) wrote a paper about the set theoretic types Elixir is hoping to implement one day, and he points to TypeScript as a practical existent example of these types. This is the same paper Elixir's creator recommends as an introduction to the research [1]. The paper is called "Programming with union, intersection, and negation types" [2]. Here's a quote from the conclusion of the paper (page 55):
"...the need of set-theoretic types naturally arises when trying to fit type-systems on dynamic languages: union and negations become necessary to capture the nature of branching and of pattern matching, intersections are often the only way to describe the polymorphic use of some functions whose definition lacks the uniformity required by parametric polymorphism. The development of languages such as Flow, TypeScript, and Typed Racket is the latest witness of this fact."
You might also want to take a look at the discussion that took place on HN about the paper when it was published [3].
[1] https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi....
[2] https://arxiv.org/pdf/2111.03354.pdf
[3] https://news.ycombinator.com/item?id=32018751
Ironically the researcher that you're deferring to (Giuseppe Castagna) wrote a paper about the set theoretic types Elixir is hoping to implement one day, and he points to TypeScript as a practical existent example of these types. This is the same paper Elixir's creator recommends as an introduction to the research [1]. The paper is called "Programming with union, intersection, and negation types" [2]. Here's a quote from the conclusion of the paper (page 55):
"...the need of set-theoretic types naturally arises when trying to fit type-systems on dynamic languages: union and negations become necessary to capture the nature of branching and of pattern matching, intersections are often the only way to describe the polymorphic use of some functions whose definition lacks the uniformity required by parametric polymorphism. The development of languages such as Flow, TypeScript, and Typed Racket is the latest witness of this fact."
You might also want to take a look at the discussion that took place on HN about the paper when it was published [3].
[1] https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi....
[2] https://arxiv.org/pdf/2111.03354.pdf
[3] https://news.ycombinator.com/item?id=32018751