| > wrote a paper about the set theoretic types Elixir is hoping to implement one day The point is, if a solution already exists, it's implementation details would simply be imitated and no further research would be required. The SOTA in set-theoretic types is not sufficient to capture typing for guards, which last I heard was a focus of Castagna's research specifically for Elixir, though the sophisticated typing of Elixir may also present other significant challenges. Again, type narrowing isn't related to pattern matching on guards. As far as I'm aware, pattern matching on function signatures is impossible for Javascript as it doesn't even permit function overloading - though Typescript could do name-mangling like C++ does to get around this. Guards allow you to overload functions based on the shape of the data, and guards can be quite complex when chained together (e.g., 'and', 'or'). But to refer back to the stated project goals, its aims are more ambitious than the SOTA: > - The Elixir team wants to go beyond type annotations and make type signatures a direct part of the language in a way to add new idioms and expressive power to the engineering teams that opt-in. This should open new perspectives in the theory of typing and the application of bi-directional typing. > - The language and runtime of Elixir have a distinct focus on fault-tolerance, concurrency, and distribution, which can lead to interesting typing considerations and modelling https://www.irif.fr/~gc/stageElixir.en.html |
Imitating ideas from one language to improve another is a form of research, and can be fairly difficult.
> As far as I'm aware, pattern matching on function signatures is impossible for Javascript as it doesn't even permit function overloading
There's no syntactical support for function overloading in JS, but it's fairly trivial to accomplish the same semantics using normal control flow (i.e. conditionals). This is why type narrowing (which uses control flow analysis), is relevant here. The paper I referred to above actually points this out. On page 6 under the section labeled "FUNCTION OVERLOADING", the author wrote:
"However, intersection types let us express ad-hoc polymorphism (i.e., function overloading) if coupled with some mechanism that allows functions to test the type of their arguments."
The author then goes on to describe this technique in more detail on the very next page:
"OCCURRENCE TYPING: Occurrence typing or flow typing [59, 46, 17] is a typing technique pioneered by Typed Racket that uses the information provided by a type test to specialize the type of some variables in the branches of a conditional...This method of refining types according to conditionals is important in type systems for dynamic languages and in those that enforce null safety: some examples include Ceylon [38], Dart [27], Flow, Kotlin [37], Typed Racket, TypeScript, and Whiley [47]."
> But to refer back to the stated project goals:
Thank you for linking to the list of project goals. The second bullet point under the list of goals says:
"To capture some programming patterns used in Elixir programming one needs to resort to the techniques of gradual typing, parametric polymorphism, and occurrence typing, three tools whose theoretical aspects have been already studied for semantic subtyping".
TS of course exhibits gradual typing and parametric polymorphism (generics), but did you notice the mention of occurrence typing? The same form of typing I referred to above, and which the author explicitly mentions exists in TypeScript (amongst others).
I honestly don't have the time to devote to this conversation any longer. I will most likely allow you to have the final word, because this discussion could carry on ad infinitum and is incredibly unproductive. As Paul Graham once said this might be taken as a tacit admission of failure [1], but I have things to do.
[1] https://news.ycombinator.com/item?id=34043420#:~:text=when%2....